|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2020jacobs.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020jacobs.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2020jacobs.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020jacobs.pdf"))
% (defun e () (interactive) (find-LATEX "2020jacobs.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020jacobs"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-pdf-page "~/LATEX/2020jacobs.pdf")
% (find-sh0 "cp -v ~/LATEX/2020jacobs.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2020jacobs.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2020jacobs.pdf
% file:///tmp/2020jacobs.pdf
% file:///tmp/pen/2020jacobs.pdf
% http://angg.twu.net/LATEX/2020jacobs.pdf
% (find-LATEX "2019.mk")
% «.4.8._quo-types-cat» (to "4.8._quo-types-cat")
% «.10.4.2._compr-cats» (to "10.4.2._compr-cats")
%
% «.ccw1» (to "ccw1")
% «.ccw1-bij» (to "ccw1-bij")
% «.ccw1-bigbij» (to "ccw1-bigbij")
% «.ccw1-three-rules» (to "ccw1-three-rules")
% «.ccompc-prodI-and-prodE» (to "ccompc-prodI-and-prodE")
% «.ccompc-sumI» (to "ccompc-sumI")
% «.ccompc-sumE+» (to "ccompc-sumE+")
\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{edrx15} % (find-LATEX "edrx15.sty")
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex % (find-LATEX "edrxgac2.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")
%L addabbrevs("|-", "⊢")
%L addabbrevs("|->", "↦")
% (find-dednat6 "dednat6/block.lua" "TexLines")
\directlua{tf:processuntil(texlines:nlines())}
\def\Eq{\text{Eq}}
\def\dom{\text{dom}}
\def\cod{\text{cod}}
\def\psmdown#1#2{\psm{#1 \\ \dnto \\ #2}}
\def\ov{\overline}
\def\s{\dncdisplay}
\def\dncdisplay[#1|#2]{\begin{pmatrix} #2 \\ #1 \end{pmatrix}}
{\setlength{\parindent}{0em}
\footnotesize
Notes on Bart Jacobs's book
"Categorical Logic and Type Theory" (Elsevier, 1999).
\url{http://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html}
\url{http://www.math.mcgill.ca/rags/jacobs.html}
\ssk
These notes are at:
\url{http://angg.twu.net/LATEX/2020jacobs.pdf}
\ssk
See:
\url{http://angg.twu.net/LATEX/2020favorite-conventions.pdf}
\url{http://angg.twu.net/math-b.html\#favorite-conventions}
I wrote these notes mostly to test if the conventions above
are good enough.
}
% «4.8._quo-types-cat» (to ".4.8._quo-types-cat")
% (find-books "__cats/__cats.el" "jacobs")
% (find-jacobspage (+ 19 290) "4.8. Quotient types, categorically")
% (find-jacobspage (+ 19 291) "is mapped to the composite")
\section*{4.8. Quotient types, categorically}
(Page 291):
\ssk
A morphism $u:I→J$ in $\bbB$ is mapped to the composite
%
$$\Eq(I) = \Eq_I⊤(I)
\diagxyto/->/<250>
(u{×}u)^*\Eq_J⊤(J)
\diagxyto/->/<250>
\Eq_J⊤(J) = \Eq(J)
$$
%
where the first part of this map is obtained by transposing the
following composite across the adjunction $\Eq_I ⊣ δ(I)^*$:
%
$$⊤(I) ≅ u^*⊤(J)
\diagxyto/->/<250>^{u^*η_J}
u^*δ(J)^*\Eq_J⊤(J) ≅ δ(I)^*(u{×}u)^*\Eq_J⊤(J)
$$
Here is a diagram that explains that construction. Two morphisms in
the construction above are morphisms in $\bbE$ that are not-vertical;
I drew them as `$\diagxyto/-->/<250>$'s.
%D diagram Eq(u)-Jacobs
%D 2Dx 100 +70 +75 +70
%D 2D 100 B0 <==> B0' <============= B1
%D 2D -\\ - -\\
%D 2D | \\ | | \\
%D 2D v \\ v v \\
%D 2D +20 B2 <\\> B2' <============= B3 \\
%D 2D /\ \/ /\ \/
%D 2D +15 \\ B4 \\ B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +20 B6 <===================== B7
%D 2D
%D 2D +15 A0 |---------------------> A1
%D 2D |-> |->
%D 2D +35 A2 |--------------------> A3
%D 2D
%D ((
%D B0 .tex= ⊤(I) B0' .tex= u^*⊤(J) B1 .tex= ⊤(J)
%D B2 .tex= δ(I)^*(u{×}u)^*\Eq_J⊤(J) B3 .tex= δ^*(J)\Eq_J⊤(J)
%D B2' .tex= u^*δ(J)^*\Eq_J⊤(J)
%D B4 .tex= \Eq_I⊤(I) B5 .tex= \Eq_J⊤(J)
%D B6 .tex= (u{×}u)^*\Eq_J⊤(J) B7 .tex= \Eq_J⊤(J)
%D B0 B0' <-> B0' B1 <-|
%D B0 B2 -> B0' B2' -> .plabel= l u^*η_J B1 B3 -> .plabel= l η_J
%D B2 B2' <-> B2' B3 <-|
%D B0 B4 |-> B1 B5 |->
%D B2 B6 <-| B3 B7 <-|
%D B6 B7 <-| B5 B7 -> .plabel= r \id
%D B4 B6 ->
%D B0 B2' harrownodes nil 20 nil <-|
%D B0' B2' midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D
%D B4 B5 --> .plabel= b \Eq(u)
%D B6 B7 --> sl^^
%D ))
%D (( A0 .tex= I A1 .tex= J
%D A2 .tex= I{×}I A3 .tex= J{×}J
%D A0 A1 -> .plabel= b u
%D A0 A2 -> .plabel= l δ(I)
%D A1 A3 -> .plabel= r δ(J)
%D A2 A3 -> .plabel= b u{×}u
%D A0 relplace 27 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\pu
\scalebox{0.9}{$
\diag{Eq(u)-Jacobs}
$}
$$
\newpage
% ____ _
% / ___|___ _ __ ___ _ __ _ __ ___ __ _| |_ ___
% | | / _ \| '_ ` _ \| '_ \| '__| / __/ _` | __/ __|
% | |__| (_) | | | | | | |_) | | | (_| (_| | |_\__ \
% \____\___/|_| |_| |_| .__/|_| \___\__,_|\__|___/
% |_|
%
% «10.4.2._compr-cats» (to ".10.4.2._compr-cats")
% (jacp 2 "10.4.2._compr-cats")
% (jac "10.4.2._compr-cats")
\section*{10.4.2. Comprehension categories}
% (find-books "__cats/__cats.el" "jacobs")
% (find-jacobspage (+ 19 613) "10.4.2. Definition. A comprehension category")
% (find-jacobspage (+ 19 614) "(ii) the simple comprehension category")
%D diagram ??
%D 2Dx 100 +25 +25 +50 +25 +25
%D 2D 100 A0 B0
%D 2D / | / |
%D 2D +25 A1 | B1 |
%D 2D / \ | / \ |
%D 2D +25 A2 A3 B2 ---- B3
%D 2D
%D ren A0 A1 A2 A3 ==> \bbE \bbB^→ \bbB \bbB
%D ren B0 B1 B2 B3 ==> \ov{B}≡\psmdown{A×B}{A} \psmdown{A×B}{A} A×B A
%D
%D (( A0 A1 -> .plabel= m \Pts
%D A1 A2 -> .plabel= m \dom
%D A1 A3 -> .plabel= m \cod
%D A0 A3 -> .plabel= r p:=\cod∘\Pts
%D A0 A2 -> .slide= -15pt .plabel= l \{-\}:=\dom∘\Pts
%D
%D B0 B1 |->
%D B1 B2 |->
%D B1 B3 |->
%D B0 B3 |->
%D B2 B3 -> .plabel= a π_{\ov{B}}
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
%D diagram ??
%D 2Dx 100 +30 +30 +30 +30 +30 +30
%D 2D 100 A1 B1
%D 2D
%D 2D +30 A2 A3 A5 B2 B3 B5
%D 2D
%D 2D +30 A6 A7 B6 B7
%D 2D
%D 2D +30 C1 D1
%D 2D
%D 2D +30 C2 C3 C5 D2 D3 D5
%D 2D
%D 2D +30 C6 C7 D6 D7
%D 2D
%D ren A1 A2 A3 A5 A6 A7 ==> X \{X\} pX Y \{Y\} pY
%D ren B1 B2 B3 ==> \ov{B}≡\psmdown{A×B}{A} A×B A
%D ren B5 B6 B7 ==> \ov{D}≡\psmdown{C×D}{C} C×D C
%D ren D1 D2 D3 ==> \ov{AC}≡\psmdown{A×C}{A} A×C A
%D ren D5 D6 D7 ==> \ov{BC}≡\psmdown{B×C}{B} B×C B
%D
%D (( A1 A2 |->
%D A1 A3 |->
%D A2 A3 -> .plabel= a π_X
%D A5 A6 |->
%D A5 A7 |->
%D A6 A7 -> .plabel= a π_Y
%D
%D A1 A5 -> .plabel= a f
%D A2 A6 -> .plabel= l \{f\}
%D A3 A7 -> .PLABEL= ^<>(0.15) pf
%D ))
%D (( B1 B2 |->
%D B1 B3 |->
%D B2 B3 -> .plabel= a π_{\ov{B}}
%D B5 B6 |->
%D B5 B7 |->
%D B6 B7 -> .plabel= a π_{\ov{D}}
%D
%D B1 B5 ->
%D B2 B6 ->
%D B3 B7 ->
%D ))
%D (( D1 D2 |->
%D D1 D3 |->
%D D2 D3 -> .plabel= a π_{\ov{B}}
%D D5 D6 |->
%D D5 D7 |->
%D D6 D7 -> .plabel= a π_{\ov{D}}
%D
%D D1 D5 -> .PLABEL= ^<>(0.7) (◻)\;f
%D D2 D6 -> .plabel= l \{f\}
%D D3 D7 -> .PLABEL= _<>(0.15) pf
%D
%D D2 relplace 16 7 \pbsymbol{7}
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
\newpage
From this point on all the diagrams are from notes that I wrote in
2008, using almost only the ``downcased notation'' from
\cite[sec.3]{IDARCT}... {\sl TODO:} create diagrams similar to these
using the notation from Jacobs! See \cite{FavC}, section 2,
conventions (COT) and (CNSh).
% (find-angg ".emacs" "idarct-preprint")
% (find-idarctpage 3 "3. Downcased Types")
% (find-idarcttext 3 "3. Downcased Types")
% (favp 8 "the-conventions")
% (fav "the-conventions")
\bsk
% --------------------
% «ccw1» (to ".ccw1")
% (s "Comprehension categories with unit" "ccw1")
\myslide {Comprehension categories with unit} {ccw1}
\def\EtoBto{\mathbb{E} \to \mathbb{B}^\to}
% (find-jacobspage (+ 19 616) "10.4.7." "comprehension category with unit")
Jacobs, 10.4.7 (p.616):
A fibration $p: \mathbb{E} \to \mathbb{B}$ with a
terminal object functor $1: \mathbb{B} \to \mathbb{E}$
(where we know by lemma 1.8.8 that $p \dashv 1$ and that $\eta_I = \id$)
is {\sl comprehension category with unit} if 1 has a right adjoint.
We call this right adjoint $\{-\}$.
%D diagram ccwu-adjs-dnc
%D 2Dx 100 +30 +30
%D 2D 100 a0 |---> a1 |---> a2
%D 2D || ^ /\ ^ ||
%D 2D || | || | ||
%D 2D \/ v || v \/
%D 2D +30 a3 |---> a4 |---> a5
%D 2D
%D (( a0 .tex= \s[a|b] a1 .tex= \s[c|*] a2 .tex= \s[d|e]
%D a3 .tex= a a4 .tex= c a5 .tex= d,e
%D @ 0 @ 1 |-> @ 1 @ 2 |->
%D @ 0 @ 3 => .plabel= l p
%D @ 1 @ 4 <= .plabel= r 1
%D @ 2 @ 5 => .plabel= r \{-\}
%D @ 0 @ 4 varrownodes nil 20 nil <->
%D @ 1 @ 5 varrownodes nil 20 nil <->
%D @ 3 @ 4 |-> @ 4 @ 5 |->
%D ))
%D enddiagram
%D
$$\diag{ccwu-adjs-dnc}$$
\msk
Jacobs, 10.4.7 (p.616):
Definition of the functor $\EtoBto$:
its action on objects is $X \mto pε_X$.
%D diagram ccwu-p
%D 2Dx 100 +30 +30 +40 +30 +30
%D 2D 100 a0 |------------> a2 b0 |------------> b2
%D 2D /\ ^ // || /\ ^ // ||
%D 2D || | // || || | // ||
%D 2D || - \/ \/ || - \/ \/
%D 2D +30 a3 |---> a4 |---> a5 b3 |---> b4 |---> b5
%D 2D
%D (( a0 .tex= 1\{X\} a2 .tex= X
%D a3 .tex= \{X\} a4 .tex= \{X\} a5 .tex= pX
%D a0 a2 -> .plabel= a ε_X
%D a3 a4 -> .plabel= b \id
%D a4 a5 -> .plabel= b pε_X
%D a0 a3 <-| a2 a4 |-> a2 a5 |->
%D a0 a4 varrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= \s[d,e|*] b2 .tex= \s[d|e]
%D b3 .tex= d,e b4 .tex= d,e b5 .tex= d
%D b0 b2 |-> b3 b4 |-> b4 b5 |->
%D b0 b3 <= b2 b4 => b2 b5 =>
%D b0 b4 varrownodes nil 20 nil <-|
%D ))
%D enddiagram
$$\diag{ccwu-p}$$
% (fooi "|->" "->" "<-|" "<-" "=>" "|->" "<=" "<-|")
% (fooi "|->" "=>" "<-|" "<=" "->" "|->" "<-" "<-|")
\msk
% (find-dn4exfile "eedemo2.tex")
%D diagram ccwu-pb
%D 2Dx 100 +30 +5 +15 +15 +15 +30
%D 2D 100 a0
%D 2D /\/
%D 2D || \
%D 2D || v
%D 2D +25 a1 |--> a2 a3
%D 2D - - ||/
%D 2D \ \ || \
%D 2D v v\/ \
%D 2D +25 a4 |---> a5 \
%D 2D - - v
%D 2D +25 a6 |-> a7 |------------------> a8
%D 2D /\ /\ \ // ||
%D 2D || || \ // ||
%D 2D || || v \/ \/
%D 2D +25 a9 |-> a10 |---------> a11 |-> a12
%D 2D
%D (( a0 .tex= 1I
%D a1 .tex= \{1I\} a2 .tex= I a3 .tex= X
%D a4 .tex= \{X\} a5 .tex= pX
%D a6 .tex= 1I a7 .tex= 1\{Y\} a8 .tex= Y
%D a9 .tex= I a10 .tex= \{Y\} a11 .tex= \{Y\} a12 .tex= pY
%D a0 a1 |-> a0 a2 <-|
%D a3 a4 |-> a3 a5 |->
%D a6 a9 <-| a7 a10 <-| a8 a11 |-> a8 a12 |->
%D a1 a2 -> sl_ .plabel= b π_{1I}
%D a1 a2 <- sl^ .plabel= a \eta_I
%D a1 a4 -> .plabel= l \{g\}
%D a2 a4 -> .plabel= m g^\vee
%D a0 a3 -> .plabel= a g
%D a2 a5 -> .plabel= m u
%D a4 a5 -> .plabel= b π_X
%D a3 a8 -> .PLABEL= ^(0.33) f
%D a4 a11 -> .PLABEL= ^(0.33) \{f\}
%D a5 a12 -> .PLABEL= ^(0.33) pf
%D a6 a7 -> .plabel= b 1v
%D a7 a8 -> .PLABEL= _(0.5) ε_Y
%D a9 a10 -> .plabel= b v
%D a10 a11 -> .plabel= b \id
%D a11 a12 -> .plabel= b π_Y
%D ))
%D enddiagram
%D diagram ccwu-pb-dnc
%D 2Dx 100 +30 -15 +15 +15 +15 +30
%D 2D 100 a0
%D 2D /\/
%D 2D || \
%D 2D || v
%D 2D +25 a1 |--> a2 a3
%D 2D - - ||/
%D 2D \ \ || \
%D 2D v v\/ \
%D 2D +25 a4 |---> a5 \
%D 2D - - v
%D 2D +25 a6 |-> a7 |------------------> a8
%D 2D /\ /\ \ // ||
%D 2D || || \ // ||
%D 2D || || v \/ \/
%D 2D +25 a9 |-> a10 |---------> a11 |-> a12
%D 2D
%D (( a0 .tex= \s[i|*]
%D a1 .tex= i,* a2 .tex= i a3 .tex= \s[a|b]
%D a4 .tex= a,b a5 .tex= a
%D a6 .tex= \s[i|*] a7 .tex= \s[c,d|*] a8 .tex= \s[c|d]
%D a9 .tex= i a10 .tex= c,d a11 .tex= c,d a12 .tex= c
%D a0 a2 <= a0 a1 =>
%D a3 a4 => a3 a5 =>
%D a6 a9 <= a7 a10 <= a8 a11 => a8 a12 =>
%D a0 a3 |->
%D a1 a2 <-> a1 a4 |-> a2 a4 |->
%D a2 a5 |-> a3 a8 |-> .plabel= a {◻} a4 a5 |->
%D a4 a11 |-> a5 a12 |->
%D a6 a7 |-> a7 a8 |->
%D a9 a10 |-> a10 a11 |-> a11 a12 |->
%D ))
%D enddiagram
The functor $\EtoBto$ is a comprehension category, i.e.,
it takes cartesian morphisms to pullback squares.
We want to check that the image of a cartesian morphism is a pullback.
Given two maps $i \mto a$ and $i \mto c,d$ such that
$a \mto c$ is well-defined, we need to construct a
mediating map $i \mto a,b$.
%
$$\diag{ccwu-pb}
\qquad
\diag{ccwu-pb-dnc}
$$
\newpage
% --------------------
% «ccw1-bij» (to ".ccw1-bij")
% (s "Comprehension categories with unit: a bijection" "ccw1-bij")
\myslide {Comprehension categories with unit: a bijection} {ccw1-bij}
Jacobs, 10.4.9 (i):
In a CCw1, pack a morphism $u: I \to J$ in the base category,
and an object $Y$ over $J$. Then the vertical morphisms $1I \to u^*Y$
are in bijection with morphisms from $u$ to $π_Y$ in $\mathbb{B}/J$.
%D diagram 1049
%D 2Dx 100 +30 +30 +30 +30 +30
%D 2D 100 a0 |-> a1 b0 |-> b1
%D 2D /\ || / /\ || /
%D 2D || || \ || || \
%D 2D || \/ v || \/ v
%D 2D +30 a2 |-> a3 a4 b2 |-> b3 b4
%D 2D / / || / / ||
%D 2D \ \ || \ \ ||
%D 2D v v \/ v v \/
%D 2D +30 a5 |-> a6 b5 |-> b6
%D 2D
%D (( a0 .tex= 1I a1 .tex= u^*Y
%D a2 .tex= I a3 .tex= I a4 .tex= Y
%D a5 .tex= \{Y\} a6 .tex= J
%D a0 a1 ->
%D a0 a2 <-| a0 a4 -> a1 a3 |-> a1 a4 -> sl^^ .plabel= a {◻} a1 a4 <-|
%D a2 a3 -> .plabel= b \id a2 a5 -> a3 a6 -> .PLABEL= ^(0.3) u a4 a5 |-> a4 a6 |->
%D a5 a6 -> .plabel= b π_Y
%D ))
%D (( b0 .tex= \s[a,b|*] b1 .tex= \s[a,b|c]
%D b2 .tex= a,b b3 .tex= a,b b4 .tex= \s[a|c]
%D b5 .tex= a,c b6 .tex= a
%D b0 b1 |->
%D b0 b2 <= b0 b4 |-> b1 b3 => b1 b4 |-> sl^ .plabel= a {◻} b1 b4 <= sl_
%D b2 b3 |-> b2 b5 |-> b3 b6 |-> b4 b5 => b4 b6 =>
%D b5 b6 |->
%D ))
%D enddiagram
%D
$$\diag{1049}$$
\newpage
% --------------------
% «ccw1-bigbij» (to ".ccw1-bigbij")
% (s "Comprehension categories with unit: big bijection" "ccw1-bigbij")
\myslide {Comprehension categories with unit: big bijection} {ccw1-bigbij}
Jacobs, 10.4.9 (ii):
% \widemtos
%D diagram 10.4.9-ii
%D 2Dx 100 +15 +45 +40 +45 +15 +45
%D 2D
%D 2D 100 a0 <-> a1 <========= a2
%D 2D - - - -
%D 2D | / / |
%D 2D v v v v
%D 2D +30 a3 ==== =====> a4 <-> a5
%D 2D /\ / \
%D 2D \\ \\
%D 2D \\ \\
%D 2D +20 a6 ============== => a7
%D 2D
%D 2D +15 a8
%D 2D / \
%D 2D \\
%D 2D \\
%D 2D +20 b0 |--- ------------> b1 a9
%D 2D -- - -
%D 2D | \ | \
%D 2D | v | v
%D 2D +20 | b2 |------------- -> b3
%D 2D v |- > v |- >
%D 2D +20 b4 b5
%D 2D
%D (( a0 .tex= 1L a1 .tex= (Qu^*A)^*1I a2 .tex= 1I
%D a3 .tex= u'^*X a4 .tex= \prod_{u^*A}u'^*X a5 .tex= u^*\prod_{A}X
%D a6 .tex= X a7 .tex= \prod_{A}X
%D a8 .tex= u^*A a9 .tex= A
%D b0 .tex= L b1 .tex= I
%D b2 .tex= J b3 .tex= K
%D b4 .tex= \{X\} b5 .tex= \{\prod_{A}X\}
%D a0 a1 <-> a1 a2 <-|
%D a0 a3 -> a1 a3 -> a2 a4 -> a2 a5 ->
%D a3 a4 |-> a4 a5 <->
%D a3 a6 <-| a5 a7 <-|
%D a6 a7 |->
%D a8 a9 <-|
%D b0 b1 -> .plabel= a Qu^*A
%D b0 b2 -> .PLABEL= ^(0.6) u'=QA^*u b1 b3 -> .plabel= r u
%D b2 b3 -> .plabel= a QA
%D b0 b4 -> b4 b2 -> .plabel= r π_X b1 b5 -> b5 b3 -> .plabel= r π_{\prod_{A}X}
%D ))
%D enddiagram
%D
$$\diag{10.4.9-ii}$$
\bsk
$a,c; b \vdash d$
$a; b \vdash c \mto d$
%D diagram 10.4.9-ii-dnc
%D 2Dx 100 +15 +45 +40 +45 +15 +45
%D 2D
%D 2D 100 a0 <-> a1 <========= a2
%D 2D - - - -
%D 2D | / / |
%D 2D v v v v
%D 2D +30 a3 ==== =====> a4 <-> a5
%D 2D /\ / \
%D 2D \\ \\
%D 2D \\ \\
%D 2D +20 a6 ============== => a7
%D 2D
%D 2D +15 a8
%D 2D / \
%D 2D \\
%D 2D \\
%D 2D +20 b0 |--- ------------> b1 a9
%D 2D -- - -
%D 2D | \ | \
%D 2D | v | v
%D 2D +20 | b2 |------------- -> b3
%D 2D v |- > v |- >
%D 2D +20 b4 b5
%D 2D
%D (( a0 .tex= \s[a,b,c|*] a1 .tex= \s[a,b,c|*] a2 .tex= \s[a,b|*]
%D a3 .tex= \s[a,b,c|d] a4 .tex= \s[a,b|{c|->d}] a5 .tex= \s[a,b|{c|->d}]
%D a6 .tex= \s[a,c|d] a7 .tex= \s[a|{c|->d}]
%D a8 .tex= \s[a,b|c] a9 .tex= \s[a|c]
%D b0 .tex= a,b,c b1 .tex= a,b
%D b2 .tex= a,c b3 .tex= a
%D b4 .tex= a,c,d b5 .tex= a,(c|->d)
%D a0 a1 <-> a1 a2 <=
%D a0 a3 |-> .plabel= l a,b,c|-d
%D a1 a3 |-> a2 a4 |->
%D a2 a5 |-> .plabel= r a,b|-c|->d
%D a3 a4 => a4 a5 <->
%D a3 a6 <= a5 a7 <=
%D a6 a7 =>
%D a8 a9 <=
%D b0 b1 |->
%D b0 b2 |-> b1 b3 |->
%D b2 b3 |->
%D b0 b4 |-> b4 b2 |-> b1 b5 |-> b5 b3 |->
%D ))
%D enddiagram
%D
$$\diag{10.4.9-ii-dnc}$$
\newpage
% --------------------
% «ccw1-three-rules» (to ".ccw1-three-rules")
% (s "Comprehension categories with unit: three rules" "ccw1-three-rules")
\myslide {Comprehension categories with unit: three rules} {ccw1-three-rules}
Jacobs, 10.3.3:
% (find-dn4file "diagxy.tex" "\\newdir")
% \newdir^{ (}{{ }*!/-.5em/@^{(}}%
\newdir^{) }{{ }*!/.5em/@^{)}}%
%D diagram sumI
%D 2Dx 100 +30 +30
%D 2D 100 a0 /
%D 2D // || /\ \
%D 2D // || \\ v
%D 2D \/ \/ \\
%D 2D +30 a2 |--> a3 a1
%D 2D / / // ||
%D 2D \ // ||
%D 2D v \/ v \/
%D 2D +30 a4 |--> a5
%D 2D
%D (( a0 .tex= \s[a,b|c] a1 .tex= \s[a|b,c]
%D a2 .tex= a,b,c a3 .tex= a,b
%D a4 .tex= a,(b,c) a5 .tex= a
%D @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{◻}
%D @ 0 @ 2 => @ 0 @ 3 => @ 1 @ 4 => @ 1 @ 5 =>
%D @ 2 @ 3 |-> @ 2 @ 4 |-> @ 3 @ 5 |-> @ 4 @ 5 |->
%D ))
%D enddiagram
%D diagram sumE+
%D 2Dx 100 +30 +15 +30
%D 2D 100 a0 |------> a1
%D 2D / /
%D 2D \ \
%D 2D v v
%D 2D +30 a2 |------> a3
%D 2D
%D (( a0 .tex= a,b,c,d a1 .tex= a,b,c
%D a2 .tex= a,(b,c),d a3 .tex= a,(b,c)
%D @ 0 @ 1 |-> sl_ @ 0 @ 1 <-' sl^
%D @ 0 @ 2 <-> @ 1 @ 3 <->
%D @ 2 @ 3 |-> sl_ @ 2 @ 3 <-' sl^
%D @ 0 relplace 15 7 \pbsymbol{7}
%D ))
%D enddiagram
%D diagram sumE-
%D 2Dx 100 +30 +40 +35
%D 2D 100 {a,b,c} |----------\
%D 2D - |-> v
%D 2D +20 | a,b,c,d |--> a,(b,c),d |--> a,d
%D 2D \ - _| - _| -
%D 2D \ | | |
%D 2D v v v v
%D 2D +30 a,b,c |----> a,(b,c) |----> a
%D 2D
%D (( {a,b,c} # 0
%D a,b,c,d a,(b,c),d a,d # 1 2 3
%D a,b,c a,(b,c) a # 4 5 6
%D @ 0 @ 4 |-> @ 0 @ 1 |-> @ 0 @ 2 |->
%D @ 1 @ 2 |-> @ 2 @ 3 |->
%D @ 1 @ 4 |-> @ 2 @ 5 |-> @ 3 @ 6 |->
%D @ 4 @ 5 |-> @ 5 @ 6 |->
%D @ 1 relplace 5 5 \pbsymbol{7} @ 2 relplace 5 5 \pbsymbol{7}
%D ))
%D enddiagram
%:
%: a,b|-C
%: ------------Σ𝐫I
%: a;b,c|-(b,c)
%:
%: ^sumI
%:
%:
%: a|-D a,b,c|-d
%: --------------Σ𝐫E^-
%: a,(b,c)|-d
%:
%: ^sumE-
%:
%:
%: a,(b,c)|-D a,b,c|-d
%: ---------------------Σ𝐫E^+
%: a,(b,c)|-d
%:
%: ^sumE+
%:
The categorical interpretation of
the rules for dependent sums:
$$\begin{array}{cc}
\cded{sumI} & \cdiag{sumI} \\ \\
\cded{sumE+} & \cdiag{sumE+} \\ \\
\cded{sumE-} & \cdiag{sumE-} \\
\end{array}
$$
(Oops, the diagram for $Σ𝐫E^-$ is wrong)
\newpage
% --------------------
% «ccompc-prodI-and-prodE» (to ".ccompc-prodI-and-prodE")
% (s "Interpreting $Π𝐫I$ and $Π𝐫E$ in a CCompC" "ccompc-prodI-and-prodE")
\myslide {Interpreting $Π𝐫I$ and $Π𝐫E$ in a CCompC} {ccompc-prodI-and-prodE}
(Jacobs, 10.5.3)
% std->dnc: (fooi ">->" "`->" "|->" "=>" "<-|" "<=" "->" "|->" "<-" "<-|")
% dnc->std: (fooi "`->" ">->" "|->" "->" "<-|" "<-" "=>" "|->" "<=" "<-|")
%D diagram 1053-prodI
%D 2Dx 100 +30 +40 +35
%D 2D 100 a0 <== a1 b0 <== b1
%D 2D - - - -
%D 2D | |-> | | |-> |
%D 2D v v v v
%D 2D +30 a2 ==> a3 b2 ==> b3
%D 2D
%D 2D +25 a4 b4
%D 2D //|| //||
%D 2D // || // ||
%D 2D \/ \/ \/ \/
%D 2D +25 a5 |-> a6 b5 |-> b6
%D 2D
%D (( a0 .tex= 1\{X\} a1 .tex= 1I a2 .tex= Y a3 .tex= Π_XY
%D a4 .tex= X a5 .tex= \{X\} a6 .tex= I
%D a0 a1 <-|
%D a0 a2 -> .plabel= l f
%D a1 a3 -> .plabel= r λ_Xf
%D a2 a3 |->
%D a0 a3 harrownodes nil 20 nil ->
%D a4 a5 |-> a4 a6 |-> a5 a6 -> .plabel= b π_X
%D ))
%D (( b0 .tex= \s[a,b|*] b1 .tex= \s[a|*]
%D b2 .tex= \s[a,b|c] b3 .tex= \s[a|b{|->c}]
%D b4 .tex= \s[a|b] b5 .tex= a,b b6 .tex= a
%D b0 b1 <=
%D b0 b2 |-> .plabel= l a,b|-c
%D b1 b3 |-> .plabel= r a|-(b|->c)
%D b2 b3 =>
%D b0 b3 harrownodes nil 20 nil |->
%D b4 b5 => b4 b6 => b5 b6 |->
%D ))
%D enddiagram
%D
$$\defΣ{\coprod}
\defΠ{\prod}
\diag{1053-prodI}
$$
%D diagram 1053-prodE
%D 2Dx 100 +35 +35 +35 +35 +35
%D 2D 100 a0 <== a1 <== a2 c0 <== c1 <== c2
%D 2D - - - - - -
%D 2D | <-| | <-| | | <-| | <-| |
%D 2D v v v v v v
%D 2D +30 a3 <== a4 ==> a5 c3 <== c4 ==> c5
%D 2D
%D 2D +25 b0 |--------> b2 d0 |--------> d2
%D 2D /\ // || /\ // ||
%D 2D || // || || // ||
%D 2D || \/ || || \/ ||
%D 2D +25 b3 |-> b4 |-> b5 d3 |-> d4 |-> d5
%D 2D
%D (( a0 .tex= 1I a1 .tex= π_X^*1I a2 .tex= 1I
%D a3 .tex= h^{\vee*}Y a4 .tex= Y a5 .tex= Π_XY
%D b0 .tex= 1I b2 .tex= X
%D b3 .tex= I b4 .tex= \{X\} b5 .tex= I
%D a0 a1 <-| a1 a2 <-|
%D a0 a3 -> .plabel= l gh
%D a1 a4 -> .plabel= m g^\wedge
%D a2 a5 -> .plabel= r g
%D a0 a4 harrownodes nil 20 nil <-|
%D a1 a5 harrownodes nil 20 nil <-|
%D a3 a4 <-| a4 a5 |->
%D b0 b2 -> .plabel= a h
%D b0 b3 <-| b2 b4 |-> b2 b5 |->
%D b0 b4 varrownodes nil 17 nil |->
%D b3 b4 >-> .plabel= b h^\vee b4 b5 -> .plabel= b π_X
%D ))
%D (( c0 .tex= \s[a|*] c1 .tex= \s[a,b|*] c2 .tex= \s[a|*]
%D c3 .tex= \s[a|c] c4 .tex= \s[a,b|c] c5 .tex= \s[a|b{|->}c]
%D d0 .tex= \s[a|*] d2 .tex= \s[a|b]
%D d3 .tex= a d4 .tex= a,b d5 .tex= a
%D c0 c1 <= c1 c2 <=
%D c0 c3 |-> .plabel= l a|-c
%D c1 c4 |->
%D c2 c5 |-> .plabel= r a|-(b|->c)
%D c0 c4 harrownodes nil 20 nil <-|
%D c1 c5 harrownodes nil 20 nil <-|
%D c3 c4 <= c4 c5 =>
%D d0 d2 |-> .plabel= a a|-b
%D d0 d3 <= d2 d4 => d2 d5 =>
%D d0 d4 varrownodes nil 17 nil |->
%D d3 d4 `-> d4 d5 |->
%D ))
%D enddiagram
%D
$$\diag{1053-prodE}$$
In the top left vertex of the diagram for $Π𝐫E$ we have
omitted an iso to keep the diagram shorter: $1I \cong h^{\vee*}π_X^*1I$.
\newpage
% --------------------
% «ccompc-sumI» (to ".ccompc-sumI")
% (s "Interpreting $Σ𝐫I$ in a CCompC" "ccompc-sumI")
\myslide {Interpreting $Σ𝐫I$ in a CCompC} {ccompc-sumI}
(Jacobs, 10.5.3)
%D diagram 1053-sumI
%D 2Dx 100 +35 +35 +35 +35 +35
%D 2D 100 a* c*
%D 2D - -
%D 2D | |
%D 2D v v
%D 2D +30 a0 <== a1 ==> a2 c0 <== c1 ==> c2
%D 2D - - - - - -
%D 2D | <-| | <-| | | <-| | <-| |
%D 2D v v v v v v
%D 2D +30 a3 <== a4 <== a5 c3 <== c4 <== c5
%D 2D
%D 2D +25 b0 |--------> b2 d0 |--------> d2
%D 2D /\ // || /\ // ||
%D 2D || // || || // ||
%D 2D || \/ || || \/ ||
%D 2D +25 b3 |-> b4 |-> b5 d3 |-> d4 |-> d5
%D 2D
%D (( a* .tex= 1I
%D a0 .tex= f^{\vee*}X a1 .tex= Y a2 .tex= Σ_XY
%D a3 .tex= Σ_XY a4 .tex= π_X^*Σ_XY a5 .tex= Σ_XY
%D b0 .tex= 1I b2 .tex= X
%D b3 .tex= I b4 .tex= \{X\} b5 .tex= I
%D a* a0 -> .plabel= r g
%D a* a3 -> .slide= -15pt .PLABEL= _(0.25) \ang{f,g}
%D a0 a1 <-| a1 a2 |->
%D a0 a3 ->
%D a1 a4 ->
%D a2 a5 -> .plabel= r \id
%D a0 a4 harrownodes nil 20 nil <-
%D a1 a5 harrownodes nil 20 nil <-
%D a3 a4 <-| a4 a5 <-|
%D b0 b2 -> .plabel= a f
%D b0 b3 <-| b2 b4 |-> b2 b5 |->
%D b0 b4 varrownodes nil 17 nil ->
%D b3 b4 >-> .plabel= b f^\vee b4 b5 -> .plabel= b π_X
%D ))
%D (( c* .tex= \s[a|*]
%D c0 .tex= \s[a|c] c1 .tex= \s[a,b|c] c2 .tex= \s[a|b,c]
%D c3 .tex= \s[a|b,c] c4 .tex= \s[a,b|b,c] c5 .tex= \s[a|b,c]
%D d0 .tex= \s[a|*] d2 .tex= \s[a|b]
%D d3 .tex= a d4 .tex= a,b d5 .tex= a
%D c* c0 |-> .plabel= r a|-c
%D c* c3 |-> .slide= -12.5pt .PLABEL= _(0.25) a|-(b,c)
%D c0 c1 <= c1 c2 =>
%D c0 c3 |->
%D c1 c4 |->
%D c2 c5 |->
%D c0 c4 harrownodes nil 20 nil <-|
%D c1 c5 harrownodes nil 20 nil <-|
%D c3 c4 <= c4 c5 <=
%D d0 d2 |-> .plabel= a a|-b
%D d0 d3 <= d2 d4 => d2 d5 =>
%D d0 d4 varrownodes nil 17 nil |->
%D d3 d4 `-> d4 d5 |->
%D ))
%D enddiagram
%D
$$\diag{1053-sumI}$$
\newpage
% --------------------
% «ccompc-sumE+» (to ".ccompc-sumE+")
% (s "Interpreting $Σ𝐫E^+$ in a CCompC" "ccompc-sumE+")
\myslide {Interpreting $Σ𝐫E^+$ in a CCompC} {ccompc-sumE+}
(Jacobs, 10.5.3)
%D diagram 1053-strongsumI-dnc
%D 2Dx 100 +25 +25 +25 +25 +25 +25 +25 +50
%D 2D
%D 2D 100 a0 |----------> a2 a3 a4
%D 2D /\ // || // || // ||
%D 2D || // || // || // ||
%D 2D || \/ \/ \/ \/ \/ \/
%D 2D +25 b0 |--> b1 |--> b2 |--> b3 |--> b4
%D 2D
%D 2D +40 c0 |----------> c2 c3
%D 2D /\ // || // ||
%D 2D || // || // ||
%D 2D || \/ \/ \/ \/
%D 2D +25 d0 |--> d1 |--> d2 |--> d3
%D 2D
%D (( a0 .tex= \s[a,b,c|*] a2 .tex= \s[a,b,c|d] a3 .tex= \s[a,b|c] a4 .tex= \s[a|b]
%D b0 .tex= a,b,c b1 .tex= a,b,c,d b2 .tex= a,b,c b3 .tex= a,b b4 .tex= a
%D c0 .tex= \s[a,(b,c)|*] c2 .tex= \s[a,(b,c)|d] c3 .tex= \s[a|b,c]
%D d0 .tex= a,(b,c) d1 .tex= a,(b,c),d d2 .tex= a,(b,c) d3 .tex= a
%D a0 a2 |-> .plabel= a a,b,c|-d
%D a0 b0 <= a2 b1 => a2 b2 => a3 b2 => a3 b3 => a4 b3 => a4 b4 =>
%D b0 b1 |-> b1 b2 |-> b2 b3 |-> b3 b4 |->
%D c0 c2 |-> .plabel= a a,(b,c)|-d
%D c0 d0 <= c2 d1 => c2 d2 => c3 d2 => c3 d3 =>
%D d0 d1 |-> d1 d2 |-> d2 d3 |->
%D b0 d0 <-> b1 d1 <-> b2 d2 <-> b3 d3 |->
%D a0 c0 <= sl_ a0 c0 |-> sl^ .PLABEL= ^(0.72) {◻}
%D a2 c2 <= sl_ a2 c2 |-> sl^ .PLABEL= ^(0.72) {◻}
%D a3 c3 => sl_ a3 c3 |-> sl^ .PLABEL= ^(0.72) {𝐫{co}◻}
%D b0 relplace 13 7 \pbsymbol{7}
%D b1 relplace 13 7 \pbsymbol{7}
%D b2 relplace 13 7 \pbsymbol{7}
%D ))
%D enddiagram
%D
$$\diag{1053-strongsumI-dnc}$$
%D diagram 1053-strongsumI
%D 2Dx 100 +25 +25 +25 +25 +25 +25 +25 +25
%D 2D
%D 2D 100 a0 |----------> a2 a3 a4
%D 2D /\ // || // || // ||
%D 2D || // || // || // ||
%D 2D || \/ \/ \/ \/ \/ \/
%D 2D +25 b0 |--> b1 |--> b2 |--> b3 |--> b4
%D 2D
%D 2D +40 c0 |----------> c2 c3
%D 2D /\ // || // ||
%D 2D || // || // ||
%D 2D || \/ \/ \/ \/
%D 2D +25 d0 |--> d1 |--> d2 |--> d3
%D 2D
%D (( a0 .tex= 1\{Y\} a2 .tex= \kk^*Z a3 .tex= Y a4 .tex= X
%D b0 .tex= \{Y\} b1 .tex= \{\kk^*Z\} b2 .tex= \{Y\} b3 .tex= \{X\} b4 .tex= I
%D c0 .tex= 1\{Σ_XY\} c2 .tex= Z c3 .tex= Σ_XY
%D d0 .tex= \{Σ_XY\} d1 .tex= \{Z\} d2 .tex= \{Σ_XY\} d3 .tex= I
%D a0 a2 -> .plabel= a h
%D a0 b0 <-| a2 b1 |-> a2 b2 |-> a3 b2 |-> a3 b3 |-> a4 b3 |-> a4 b4 |->
%D b0 b1 -> .PLABEL= ^(0.6) h^\vee
%D b1 b2 -> .plabel= a π_{\kk^*Z}
%D b2 b3 -> .plabel= a π_Y
%D b3 b4 -> .plabel= a π_X
%D c0 c2 -> .plabel= a (\kk^{-1};\overline{h})^\wedge
%D c0 d0 <-| c2 d1 |-> c2 d2 |-> c3 d2 |-> c3 d3 |->
%D d0 d1 -> .plabel= b \kk^{-1};\overline{h}
%D d1 d2 -> .plabel= b π_Z
%D d2 d3 -> .plabel= b π_{\{Σ_XY\}}
%D b0 d0 <-> .plabel= a \kk
%D b1 d1 <->
%D b2 d2 <-> .plabel= a \kk
%D b3 d3 -> .plabel= a π_X
%D a0 c0 <-| sl_ a0 c0 -> sl^ .PLABEL= ^(0.72) 1\kk
%D a2 c2 <-| sl_ a2 c2 -> sl^ .PLABEL= ^(0.72) {◻}
%D a3 c3 |-> sl_ a3 c3 -> sl^ .PLABEL= ^(0.72) {𝐫{co}◻}
%D b0 relplace 13 7 \pbsymbol{7}
%D b1 relplace 13 7 \pbsymbol{7}
%D b2 relplace 13 7 \pbsymbol{7}
%D ))
%D enddiagram
%D
$$\defΣ{\coprod}
\diag{1053-strongsumI}
$$
\printbibliography
\end{document}
% __ __ _
% | \/ | __ _| | _____
% | |\/| |/ _` | |/ / _ \
% | | | | (_| | < __/
% |_| |_|\__,_|_|\_\___|
%
% <make>
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2020jacobs veryclean
make -f 2019.mk STEM=2020jacobs pdf
% Local Variables:
% coding: utf-8-unix
% ee-tla: "jac"
% End: