|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2022yoneda-pseudocode.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2022yoneda-pseudocode.tex" :end))
% (defun C () (interactive) (find-LATEXSH "lualatex 2022yoneda-pseudocode.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2022yoneda-pseudocode.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2022yoneda-pseudocode.pdf"))
% (defun e () (interactive) (find-LATEX "2022yoneda-pseudocode.tex"))
% (defun u () (interactive) (find-latex-upload-links "2022yoneda-pseudocode"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2022yoneda-pseudocode.pdf"))
% (code-eec-LATEX "2022yoneda-pseudocode")
% (find-pdf-page "~/LATEX/2022yoneda-pseudocode.pdf")
% (find-sh0 "cp -v ~/LATEX/2022yoneda-pseudocode.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2022yoneda-pseudocode.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2022yoneda-pseudocode.pdf
% file:///tmp/2022yoneda-pseudocode.pdf
% file:///tmp/pen/2022yoneda-pseudocode.pdf
% http://angg.twu.net/LATEX/2022yoneda-pseudocode.pdf
% (find-LATEX "2019.mk")
% (find-lualatex-links "2022yoneda-pseudocode" "yps")
\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}
%
% (find-dn6 "preamble6.lua" "preamble0")
%\usepackage{proof} % For derivation trees ("%:" lines)
\input diagxy % For 2D diagrams ("%D" lines)
%\xyoption{curve} % For the ".curve=" feature in 2D diagrams
%
\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")
%
%\usepackage[backend=biber,
% style=alphabetic]{biblatex} % (find-es "tex" "biber")
%\addbibresource{catsem-slides.bib} % (find-LATEX "catsem-slides.bib")
%
% (find-es "tex" "geometry")
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
\def\respcomp{\mathsf{respcomp}}
\def\respids {\mathsf{respids}}
\def\sqcond {\mathsf{sqcond}}
\def\Te {T_\eta}
\def\Tez{(T_\eta)_0}
\def\eTe{\eta_{T_\eta}}
\def\TeT{T_{\eta_T}}
%L forths["<."] = function () pusharrow("<.") end
%D diagram Y0-main-names
%D 2Dx 100 +40
%D 2D 100 A1
%D 2D |
%D 2D +25 A2 - A3
%D 2D | |
%D 2D +25 A4 - A5
%D 2D | |
%D 2D +25 A6 - A7
%D 2D | |
%D 2D +25 A8 - A9
%D 2D
%D 2D +15 B0 - B1
%D 2D
%D 2D +20 C0 - C1
%D 2D
%D ren A1 ==> A
%D ren A2 A3 ==> C RC
%D ren A4 A5 ==> D RD
%D ren A6 A7 ==> E RE
%D ren A8 A9 ==> F RF
%D ren B0 B1 ==> \catB \catA
%D ren C0 C1 ==> \catB(C,-) \catA(A,R-)
%D
%D (( A1 A3 -> .plabel= r η
%D A2 A3 |->
%D A2 A4 -> .plabel= l f
%D A3 A5 -> .plabel= r Rf
%D A2 A5 harrownodes nil 20 nil |->
%D A4 A5 |->
%D A4 A6 -> .plabel= l g
%D A5 A7 -> .plabel= r Rg
%D A4 A7 harrownodes nil 20 nil |->
%D A6 A7 |->
%D A6 A8 -> .plabel= l h
%D A7 A9 -> .plabel= r Rh
%D A6 A9 harrownodes nil 20 nil |->
%D A8 A9 |->
%D
%D A2 A6 -> .slide= -15pt .plabel= l k
%D A1 A5 -> .slide= 20pt .plabel= r ℓ
%D A1 A7 -> .slide= 35pt .plabel= r m
%D
%D B0 B1 -> .plabel= a R
%D
%D C0 C1 -> .plabel= a T
%D # C0 C1 <. .plabel= b T^{-1} .slide= -5pt
%D ))
%D enddiagram
\pu
\def\ColorOpt#1{{\color{brown} #1}}
\def\opt#1{\ColorOpt{\{} #1 \ColorOpt{\}}}
\def\s{\;\;\;\;\;\;\;}
%\sa{B(C,-).identity}{
% \begin{array}{ll}
% \catB(C,-).\text{identity} & \text{is:} \\ [5pt]
% %
% ∀D. \; \catB(C,-)._1 \; (\catB.\id \; \opt{D}) \\
% \s = \Set.\id \; \opt{\catB(C,-)._0 \; D}, & \text{that is:} \\[5pt]
% %
% ∀D. \; \catB(C,\id_D) \\
% \s = λf.\, \id_D ∘_\catB f \\
% \s = λf.\, f \\
% \s = \id_{\catB(C,D)} \\
% \end{array}
% }
%\sa{A(A,R-).identity}{
% \begin{array}{ll}
% \catA(A,R-).\text{identity} & \text{is:} \\ [5pt]
% %
% ∀D. \; \catA(A,R-)._1 \; (\catB.\id \; \opt{D}) \\
% \s = \Set.\id \; \opt{\catA(A,R-)._0 \; D}, & \text{that is:} \\[5pt]
% %
% ∀D. \; \catA(A,R(\id_D)) \\
% \s = λℓ.\, \id_{RD} ∘_\catA ℓ \\
% \s = λℓ.\, ℓ \\
% \s = \id_{\catA(C,D)} \\
% \end{array}
% }
\sa{Y0 constructions}{
\begin{array}{rcl}
\catA &\text{is}& \text{a small category} \\
\catB &\text{is}& \text{a small category} \\
R &:& \catB \to \catA \\
A &∈& \catA \\
C &∈& \catB \\[5pt]
%
B(C,-) &:& \catB \to \Set \\
B(C,-)_0 &=& λD.\,\catB(C,D) \\
B(C,-)_1 &=& λg.\,λf.\,g∘f \\[5pt]
%
A(A,R-) &:& \catB \to \Set \\
A(A,R-)_0 &=& λD.\,\catA(A,RD) \\
A(A,R-)_1 &=& λg.\,λℓ.\,Rg∘ℓ \\[5pt]
%
η &:& A \to RC \\
T &:& B(C,-) \to A(A,R-) \\[5pt]
% %
% η_T &=& T(C)(\id_C) \\
% \Tez &=& λD. \, λf.\, Rf∘η \\
%
(T_0↦η) &=& λT_0.\,T_0(C)(\id_C) \\
(η↦T_0) &=& λη.\,λD. \, λf.\, Rf∘η \\
\end{array}
}
\sa{respids B(C,-)}{
\begin{array}{ll}
\respids_{\catB(C,-)} \quad \text{is:} \\ [5pt]
%
∀D. \; \catB(C,\id_D) \\
\s = λf.\, \id_D ∘_\catB f \\
\s = λf.\, f \\
\s = \id_{\catB(C,D)} \\
\end{array}
}
\sa{respids A(A,R-)}{
\begin{array}{ll}
\respids_{\catA(A,R-)} \quad \text{is:} \\ [5pt]
%
∀D. \; \catA(A,R(\id_D)) \\
\s = λℓ.\, \id_{RD} ∘_\catA ℓ \\
\s = λℓ.\, ℓ \\
\s = \id_{\catA(C,D)} \\
\end{array}
}
\sa{respcomp B(C,-)}{
\begin{array}{ll}
\respcomp_{\catB(C,-)} \quad \text{is:} \\ [5pt]
%
∀D,E,F,g,h. \\
\s \catB(C,h) ∘_\Set \catB(C,g) \\
\s = (λk.\,h ∘_\catB k) ∘_\Set (λf.g ∘_\catB f) \\
\s = λf.\,h ∘_\catB (g ∘_\catB f) \\
\s = λf.\,(h ∘_\catB g) ∘_\catB f \\
\s = \catB(C,h ∘_\catB g) \\
\end{array}
}
\sa{respcomp A(A,R-)}{
\begin{array}{ll}
\respcomp_{\catA(A,R-)} \quad \text{is:} \\ [5pt]
%
∀D,E,F,g,h. \\
\s \catA(A,Rh) ∘_\Set \catA(A,Rg) \\
\s = (λk.\,h ∘_\catB k) ∘_\Set (λf.g ∘_\catB f) \\
\s = λf.\,h ∘_\catB (g ∘_\catB f) \\
\s = λf.\,(h ∘_\catB g) ∘_\catB f \\
\s = \catA(A,h ∘_\catB g) \\
\end{array}
}
$$\pu
\diag{Y0-main-names}
\qquad
\ga{Y0 constructions}
$$
$$\ga{respids B(C,-)}
\qquad
\ga{respids A(A,R-)}
$$
$$\ga{respcomp B(C,-)}
\qquad
\ga{respcomp A(A,R-)}
$$
\newpage
\sa{sqcond Te}{
\begin{array}{ll}
\sqcond_{\Te} \quad \text{is:} \\ [5pt]
%
∀D,E,g. \\
\s \Tez(E) ∘_\Set \catB(C,g) \\
\s = (λk.\,Rk ∘_\catA η) ∘_\Set (λf.\,g ∘_\catB f) \\
\s = (λf.\,R(g ∘_\catB f) ∘_\catA η) \\
\s = (λf.\,Rg ∘_\catA (Rf ∘_\catA η)) \\
\s = (λℓ.\,Rg∘ℓ) ∘_\Set (λf.\,Rf∘η) \\
\s = \catA(A,Rg) ∘_\Set \Tez(D) \\
\end{array}
}
\sa{eTe = e}{
\begin{array}{ll}
(\eTe = η) \quad \text{is:} \\ [5pt]
%
(T_0→η) ((η↦T_0) (η)) \\
= (T_0→η) ((λη.\,λD. \, λf.\, Rf∘η) (η)) \\
= (T_0→η) (λD. \, λf.\, Rf∘η) \\
= (λT_0.\,T_0(C)(\id_C)) (λD. \, λf.\, Rf∘η) \\
= (λD. \, λf.\, Rf∘η) (C) (\id_C) \\
= R \id_C ∘ η \\
= \id_{RC} ∘η \\
= η \\
\end{array}
}
$$\diag{Y0-main-names}
\qquad
\ga{Y0 constructions}
$$
$$\ga{sqcond Te}
\qquad
\ga{eTe = e}
$$
\newpage
\sa{(TeT)_0 = T_0}{
\begin{array}{ll}
((\TeT)_0 = T_0) \quad \text{is:} \\ [5pt]
%
(η↦T_0) ((T_0→η) (T_0)) \\
= (η↦T_0) ((λT_0.\,T_0(C)(\id_C)) (T_0)) \\
= (η↦T_0) (T_0(C)(\id_C)) \\
= (λη.\,λD. \, λf.\, Rf∘η) (T_0(C)(\id_C)) \\
= λD. \, λf. \, Rf∘(T_0(C)(\id_C)) \\
= λD. \, λf. \, T_0(D)(f) \\
= T_0 \\
\end{array}
}
$$\diag{Y0-main-names}
\qquad
\ga{Y0 constructions}
$$
$$\ga{(TeT)_0 = T_0}
$$
\newpage
{\bf Lemma: $Rf∘TC(\id_C) = TD(f)$.}
{\bf Formal proof:} if we apply $\sqcond_T$ to $f:D→C$ we get:
%
$$∀D.\,∀f.\,∀γ.\,Rf∘TC(γ) = TD(f∘γ)$$
and if we specialize $γ:=\id_C$ above and simplify a bit we get:
%
$$∀D.\,∀f.\,Rf∘TC(\id_C) = TD(f)$$
%D diagram lemma-diag-1
%D 2Dx 100 +40
%D 2D 100 A1
%D 2D |
%D 2D +20 A2 - A3
%D 2D | |
%D 2D +20 A4 - A5
%D 2D | |
%D 2D +20 A6 - A7
%D 2D
%D 2D +15 B0 - B1
%D 2D
%D 2D +20 C0 - C1
%D 2D
%D ren A1 ==> A
%D ren A2 A3 ==> C RC
%D ren A4 A5 ==> C RC
%D ren A6 A7 ==> D RD
%D ren B0 B1 ==> \catB \catA
%D ren C0 C1 ==> \catB(C,-) \catA(A,R-)
%D
%D (( A1 A3 -> # .plabel= r η
%D A2 A3 |->
%D A2 A4 -> .plabel= l \id_C
%D A3 A5 -> .plabel= r R\id_C
%D A2 A5 harrownodes nil 20 nil |->
%D A4 A5 |->
%D A4 A6 -> .plabel= l f
%D A5 A7 -> .plabel= r Rf
%D A4 A7 harrownodes nil 20 nil |->
%D A6 A7 |->
%D
%D # A2 A6 -> .slide= -15pt .plabel= l k
%D A1 A5 -> .slide= 30pt .plabel= r T(C)(\id_C)
%D A1 A7 -> .slide= 80pt .plabel= r \sm{T(D)(f∘\id_C)\\=T(D)(f)}
%D
%D B0 B1 -> .plabel= a R
%D
%D C0 C1 -> .plabel= a T
%D # C0 C1 <. .plabel= b T^{-1} .slide= -5pt
%D ))
%D enddiagram
%D diagram Y0-NT-3
%D 2Dx 100 +25 +40 +30 +35 +30 +35
%D 2D 100 A0 B0 - B1 D0 |-> D1 E0 |-> E1
%D 2D +17 | | | | D3' | E3'
%D 2D +8 A1 B2 - B3 D2 |-> D3 E2 |-> E3
%D 2D
%D 2D +15 C0 - C1
%D 2D
%D ren A0 A1 ==> C D
%D ren B0 B1 B2 B3 ==> \catB(C,C) \catA(A,RC) \catB(C,D) \catA(A,RD)
%D ren C0 C1 ==> \catB(C,-) \catA(A,R-)
%D # ren D0 D1 D3' ==> \id_C TC(\id_C) Rf∘(TC(\id_C))
%D # ren D2 D2' D3 ==> f∘\id_C f TD(f)
%D
%D ren D0 D1 D3' ==> γ TC(γ) Rf∘TC(γ)
%D ren D2 D3 ==> f∘γ TD(f∘γ)
%D ren E0 E1 E3' ==> \id_C TC(\id_C) Rf∘TC(\id_C)
%D ren E2 E3 ==> f TD(f)
%D
%D (( A0 A1 -> .plabel= l f
%D B0 B1 -> .plabel= a TC
%D B0 B2 -> .plabel= l \catB(C,f)
%D B1 B3 -> .plabel= r \catA(A,Rf)
%D B2 B3 -> .plabel= a TD
%D C0 C1 -> .plabel= a T
%D D0 D1 |-> D1 D3' |->
%D D0 D2 |-> D2 D3 |->
%D E0 E1 |-> E1 E3' |->
%D E0 E2 |-> E2 E3 |->
%D ))
%D enddiagram
\pu
{\bf Diagrams:}
%
$$\diag{Y0-NT-3}
$$
$$\diag{lemma-diag-1}
$$
% (favp 31 "basic-example-bij")
% (fava "basic-example-bij")
% (fava "basic-example-bij" "Y0-NT-3")
% identity : ∀ {A} → D [ F₁ (C.id {A}) ≈ D.id ]
% homomorphism : ∀ {X Y Z} {f : C [ X , Y ]} {g : C [ Y , Z ]} →
% D [ F₁ (C [ g ∘ f ]) ≈ D [ F₁ g ∘ F₁ f ] ]
% %L dofile "edrxtikz.lua" -- (find-LATEX "edrxtikz.lua")
% %L dofile "edrxpict.lua" -- (find-LATEX "edrxpict.lua")
% \pu
%\printbibliography
\GenericWarning{Success:}{Success!!!} % Used by `M-x cv'
\end{document}
% __ __ _
% | \/ | __ _| | _____
% | |\/| |/ _` | |/ / _ \
% | | | | (_| | < __/
% |_| |_|\__,_|_|\_\___|
%
% <make>
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2022yoneda-pseudocode veryclean
make -f 2019.mk STEM=2022yoneda-pseudocode pdf
% Local Variables:
% coding: utf-8-unix
% ee-tla: "yps"
% End: