Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2022missing-changes-1.tex") % (defun c () (interactive) (find-LATEXsh "lualatex -record 2022missing-changes-1.tex" :end)) % (defun C () (interactive) (find-LATEXSH "lualatex 2022missing-changes-1.tex" "Success!!!")) % (defun D () (interactive) (find-pdf-page "~/LATEX/2022missing-changes-1.pdf")) % (defun d () (interactive) (find-pdftools-page "~/LATEX/2022missing-changes-1.pdf")) % (defun e () (interactive) (find-LATEX "2022missing-changes-1.tex")) % (defun u () (interactive) (find-latex-upload-links "2022missing-changes-1")) % (defun v () (interactive) (find-2a '(e) '(d))) % (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g)) % (defun d0 () (interactive) (find-ebuffer "2022missing-changes-1.pdf")) % (code-eec-LATEX "2022missing-changes-1") % (find-pdf-page "~/LATEX/2022missing-changes-1.pdf") % (find-sh0 "cp -v ~/LATEX/2022missing-changes-1.pdf /tmp/") % (find-sh0 "cp -v ~/LATEX/2022missing-changes-1.pdf /tmp/pen/") % file:///home/edrx/LATEX/2022missing-changes-1.pdf % file:///tmp/2022missing-changes-1.pdf % file:///tmp/pen/2022missing-changes-1.pdf % http://angg.twu.net/LATEX/2022missing-changes-1.pdf % (find-LATEX "2019.mk") % (find-lualatex-links "2022missing-changes-1" "mc1") % % https://mail.google.com/mail/u/0/#inbox/FMfcgzGrbcCBSvFGDTZDDLwRCTdsFJGW \documentclass[oneside,12pt]{article} \usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref") \usepackage{amsmath} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{pict2e} \usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor") %\usepackage{colorweb} % (find-es "tex" "colorweb") %\usepackage{tikz} % \usepackage{edrx21} % (find-LATEX "edrx21.sty") \input edrxaccents.tex % (find-LATEX "edrxaccents.tex") \input edrx21chars.tex % (find-LATEX "edrx21chars.tex") %\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex") %\input edrxgac2.tex % (find-LATEX "edrxgac2.tex") %\input 2017planar-has-defs.tex % (find-LATEX "2017planar-has-defs.tex") % % (find-es "tex" "geometry") \begin{document} \def\ref#1{\standout{ref:#1}} \def\acontext{\ang{\textsf{context}}} \def\aexpr {\ang{\textsf{expr}}} Lines 304--309: Current version: \begin{quotation} It can also be noticed that most typings that could be inferred from the diagram can be omitted. The diagram above can be formalized as: ``in a context where $(\catA, \catB, R, A, B, η)$ are as in the diagram above, $(B,η)$ can be said to be a universal arrow from $A$ to % $R$ when $∀(B',g).∃!f.(Rf∘η=g)$''. This looked too loaded to be used % in public, but it was practical for private notes --- and I could even % omit the ``$Rf∘η=g$'', as everything commutes by default. In sec.\ref{omitting-types} wa way to formalize this method for omitting and reconstructing types will be presented, and in sec.\ref{indefinite-articles} a second way to define universalness will be discussed as well. \end{quotation} Corrected version: \begin{quotation} It can also be noticed that most typings that can be inferred from the diagram can be omitted. The diagram above can be formalized as: ``in a context where $(\catA, \catB, R, A, B, η)$ are typed as in the diagram above, $(B,η)$ can be said to be a universal arrow from $A$ to $R$ when $∀(B',g).∃!f.(Rf∘η=g)$''. And as by default everything commutes (see the convention (CC)), the $(Rf∘η=g)$ can also be omitted. In sec.\ref{omitting-types} a way to formalize this method for omitting and reconstructing types will be presented, and in sec.\ref{indefinite-articles} a second way to define universalness will be discussed as well. \end{quotation} \bsk Line 521: Current version: \begin{quotation} The comprehension $\setofst{ \aexpr }{ \acontext }$ to $\setofsc{ \acontext }{ \aexpr }$ are rewritten for clarity, \end{quotation} Corrected version: \begin{quotation} The comprehension $\setofst{ \aexpr }{ \acontext }$ was rewritten as $\setofsc{ \acontext }{ \aexpr }$ for clarity, \end{quotation} \GenericWarning{Success:}{Success!!!} % Used by `M-x cv' \end{document} % Local Variables: % coding: utf-8-unix % ee-tla: "mc1" % End: