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

