|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2022on-the-missing-agda.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2022on-the-missing-agda.tex" :end))
% (defun C () (interactive) (find-LATEXSH "lualatex 2022on-the-missing-agda.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2022on-the-missing-agda.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2022on-the-missing-agda.pdf"))
% (defun e () (interactive) (find-LATEX "2022on-the-missing-agda.tex"))
% (defun u () (interactive) (find-latex-upload-links "2022on-the-missing-agda"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2022on-the-missing-agda.pdf"))
% (code-eec-LATEX "2022on-the-missing-agda")
% (find-pdf-page "~/LATEX/2022on-the-missing-agda.pdf")
% (find-sh0 "cp -v ~/LATEX/2022on-the-missing-agda.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2022on-the-missing-agda.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2022on-the-missing-agda.pdf
% file:///tmp/2022on-the-missing-agda.pdf
% file:///tmp/pen/2022on-the-missing-agda.pdf
% http://angg.twu.net/LATEX/2022on-the-missing-agda.pdf
% (find-LATEX "2019.mk")
% (find-lualatex-links "2022on-the-missing-agda" "mia")
% «.defs» (to "defs")
% «.title» (to "title")
% «.Y0-functors» (to "Y0-functors")
% «.eTe=ee» (to "eTe=ee")
% «.TeT=TT» (to "TeT=TT")
% «.lemma» (to "lemma")
\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")
% «defs» (to ".defs")
\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}}
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% «title» (to ".title")
{\bf On the missing diagrams}
{\bf in Category Theory:}
{\bf Agda code}
\bsk
\bsk
This file will be a complement to:
% (misp 36 "basic-example-as-skel")
% (misa "basic-example-as-skel")
\url{http://angg.twu.net/LATEX/2022on-the-missing.pdf}
It will contain diagrams, pseudocode and Agda code.
At this moment it is mostly a stub, with just the
diagrams and a bit of pseudocode.
\msk
See:
% (find-dired-re "~/LATEX/" "2022.*.pdf")
\url{http://angg.twu.net/LATEX/2022Cats3.pdf}
\url{http://angg.twu.net/LATEX/2022Cats6.pdf}
\url{http://angg.twu.net/AGDA/2022HuC2.agda.html}
\url{http://angg.twu.net/AGDA/2022HuC3.agda.html}
\newpage
% __ _____ __ _
% \ \ / / _ \ _ / _|_ _ _ __ ___| |_ ___ _ __ ___
% \ V / | | (_) | |_| | | | '_ \ / __| __/ _ \| '__/ __|
% | || |_| |_ | _| |_| | | | | (__| || (_) | | \__ \
% |_| \___/(_) |_| \__,_|_| |_|\___|\__\___/|_| |___/
%
% «Y0-functors» (to ".Y0-functors")
% (miap 2 "Y0-functors")
% (miaa "Y0-functors")
{\bf The functors $\catB(C,-)$ and $\catA(A,R-)$}\
%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{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
% _____
% __|_ _|__ _____ ___ ___
% / _ \| |/ _ \ |_____| / _ \/ _ \
% | __/| | __/ |_____| | __/ __/
% \___||_|\___| \___|\___|
%
% «eTe=ee» (to ".eTe=ee")
% (miap 3 "eTe=ee")
% (miaa "eTe=ee")
{\bf $\sqcond_{\Te}$ and $(η↦T↦η)=\id$}
\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
% _____ _____ _____ _____
% |_ _|_|_ _| _____ |_ _|_ _|
% | |/ _ \| | |_____| | | | |
% | | __/| | |_____| | | | |
% |_|\___||_| |_| |_|
%
% «TeT=TT» (to ".TeT=TT")
% (miap 3 "TeT=TT")
% (miaa "TeT=TT")
\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
% _
% | | ___ _ __ ___ _ __ ___ __ _
% | | / _ \ '_ ` _ \| '_ ` _ \ / _` |
% | |__| __/ | | | | | | | | | | (_| |
% |_____\___|_| |_| |_|_| |_| |_|\__,_|
%
% «lemma» (to ".lemma")
% (miap 5 "lemma")
% (miaa "lemma")
{\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")
%\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=2022on-the-missing-agda veryclean
make -f 2019.mk STEM=2022on-the-missing-agda pdf
% Local Variables:
% coding: utf-8-unix
% ee-tla: "mia"
% End: