|
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: