% (find-LATEX "2008comprcat-utf8.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2008comprcat-utf8.tex" :end))
% (defun d () (interactive) (find-pdf-page      "~/LATEX/2008comprcat-utf8.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2008comprcat-utf8.pdf"))
% (defun e () (interactive) (find-LATEX "2008comprcat-utf8.tex"))
% (defun u () (interactive) (find-latex-upload-links "2008comprcat-utf8"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-pdf-page   "~/LATEX/2008comprcat-utf8.pdf")
% (find-sh0 "cp -v  ~/LATEX/2008comprcat-utf8.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2008comprcat-utf8.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2008comprcat-utf8.pdf
%               file:///tmp/2008comprcat-utf8.pdf
%           file:///tmp/pen/2008comprcat-utf8.pdf
% http://angg.twu.net/LATEX/2008comprcat-utf8.pdf
% (find-LATEX "2019.mk")

\documentclass[oneside]{book}
\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")
%
% (find-es "tex" "geometry")
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

% %L dofile "edrxtikz.lua"  -- (find-LATEX "edrxtikz.lua")
% %L dofile "edrxpict.lua"  -- (find-LATEX "edrxpict.lua")
% \pu

% (find-dednat6 "dednat6/block.lua" "TexLines")
\directlua{tf:processuntil(texlines:nlines())}


% %:\s[\dncdisplay[
\def\s{\dncdisplay}
\def\dncdisplay[#1|#2]{\begin{pmatrix} #2 \\ #1 \end{pmatrix}}



% «.dtt-exchange»		(to "dtt-exchange")
% «.dtt-unpack»			(to "dtt-unpack")
% «.dtt-structural-rules»	(to "dtt-structural-rules")
% «.dtt-type-rules»		(to "dtt-type-rules")
% «.dtt-alt-sum-rules»		(to "dtt-alt-sum-rules")
% «.dtt-alt-equality»		(to "dtt-alt-equality")

% «.dtt-adjunctions»		(to "dtt-adjunctions")
% «.dtt-conversions»		(to "dtt-conversions")
% «.rules-dtt»			(to "rules-dtt")

% «.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+")

% «.dtt-unpack-2»		(to "dtt-unpack-2")


% «.elisp»			(to "elisp")



Index of the slides:
\msk
% To update the list of slides uncomment this line:
%\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")
\tocline {DTT: the exchange rule} {2}
\tocline {DTT: the ``unpack'' rule} {3}
\tocline {DTT: structural rules} {4}
\tocline {DTT: type rules} {5}
\tocline {DTT: alternate rules for strong sum} {6}
\tocline {DTT: Alternate rules for strong equality} {7}
\tocline {Adjunction diagrams} {8}
\tocline {Conversions} {9}
\tocline {Comprehension categories with unit} {10}
\tocline {Comprehension categories with unit: a bijection} {11}
\tocline {Comprehension categories with unit: big bijection} {12}
\tocline {Comprehension categories with unit: three rules} {13}
\tocline {Interpreting $\Pi$I and $\Pi$E in a CCompC} {14}
\tocline {Interpreting $\Sigma$I in a CCompC} {15}
\tocline {Interpreting $\Sigma \mathrm{E}^+$ in a CCompC} {16}
\tocline {The ``unpack'' rule (2)} {17}
\tocline {Rules for DTT} {18}

\newpage


%
% (eedn4-51-bounded)
% (find-diagxypage 23)
% (find-dn4 "dednat41.lua" "lplacement")
% (find-dn4file "experimental.lua")
% (find-LATEXfile "diagxy.tex")
% (find-LATEXfile "diagxy.tex" "\\def\\domorphism")

% (eedn4-51-bounded)
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% (find-LATEXfile "2008topos-str.tex")

% --------------------
% «dtt-exchange»  (to ".dtt-exchange")
% (s "DTT: the exchange rule" "dtt-exchange")
\myslide {DTT: the exchange rule} {dtt-exchange}

\def▁{\underline}
\def\unpackasin#1#2#3{\text{unpack $#1$ as $\ang{#2}$ in $#3$}}
\def\unpackin#1#2{\text{unpack $#1$ in $#2$}}
\def\withvia#1#2#3{\text{$#1$ with $#2$ via $#3$}}
\def\wvia#1#2{\text{with $#1$ via $#2$}}
\def\via#1#2{\text{$#1$ via $#2$}}
\def\eqdef{\overset{\text{def}}{=}}
\def\eqeta{\overset{\eta}{=}}
\def\eqbeta{\overset{\beta}{=}}
\def\Type{𝐬{Type}}
\def\Eq{𝐫{Eq}}

In Jacobs (10.1) the exchange rule for DTT is stated like this:

%:  \GG,x:σ,y:τ,\DD|-M:ρ
%:  --------------------
%:  \GG,y:τ,x:σ,\DD|-M:ρ
%:  
%:  ^exchange-jacobs
%:  
$$\ded{exchange-jacobs}$$

with a side-condition: ``$x$ is not free in $τ$''.

\msk

Let's translate this:

%:  \vec{a}⠆\vec{A},b⠆B_{\vec{a}},c⠆C_{\vec{a}},\vec{d}⠆\vec{D}_{\vec{a}bc}|-e_{\vec{a}bc\vec{d}}⠆E_{\vec{a}bc\vec{d}}
%:  -----------------------------------------------------------------------------------------------------
%:  \vec{a}⠆\vec{A},c⠆C_{\vec{a}},b⠆B_{\vec{a}},\vec{d}⠆\vec{D}_{\vec{a}bc}|-e_{\vec{a}bc\vec{d}}⠆E_{\vec{a}bc\vec{d}}
%:
%:  ^exchange-abcde-big
%:
$$\ded{exchange-abcde-big}$$

Note that if we had used $c:C_{\vec{a}b}$ instead of $c:C_{\vec{a}}$

the bottom judgment would have made no sense.

\msk

Let's make this shorter.

We can hide the annotations that indicate dependencies,

the types, and the ``vector'' marks:

%:  \vec{a}⠆\vec{A},b⠆B,c⠆C,\vec{d}⠆\vec{D}|-e⠆E
%:  ------------------------------------
%:  \vec{a}⠆\vec{A},c⠆C,b⠆B,\vec{d}⠆\vec{D}|-e⠆E
%:
%:  ^exchange-abcde-tv
%:
%:  \vec{a},b,c,\vec{d}|-e
%:  ----------------------
%:  \vec{a},c,b,\vec{d}|-e
%:
%:  ^exchange-abcde-v
%:
%:  a,b,c,d|-e
%:  ----------
%:  a,c,b,d|-e
%:
%:  ^exchange-abcde
%:
$$\ded{exchange-abcde-tv} \qquad \ded{exchange-abcde-v} \qquad \ded{exchange-abcde}$$

It is this last form that we will use.

\bsk
\bsk

{\bf Exercise:} rewrite the first translation with 
%
$$\begin{array}{rcl}
  (\vec{a}⠆\vec{A}) & := & (a_1⠆A_1[\,],\ldots,a_n⠆A_n[a_1,...,a_{n-1}]) \\
  (\vec{d}⠆\vec{D}_{\vec{a}bc}) & := & (d_1⠆D_1[a_1,...,a_{n},b,c],\ldots, \\
  				  &    & \phantom{(}d_m⠆D_m[a_1,...,a_{n},b,c,d_1,...,d_{m-1}]) \\
  \end{array}
$$

and check that the rule becomes unbearably big.

\newpage
% --------------------
% «dtt-unpack»  (to ".dtt-unpack")
% (s "DTT: the ``unpack'' rule" "dtt-unpack")
\myslide {DTT: the ``unpack'' rule} {dtt-unpack}

In Jacobs (10.1, but after 10.1.2) the strong

sum-elimination rule is stated as this:
%:
%:  \GG,z:Σx:σ.τ|-ρ:\Type   \GG,x:σ,y:τ|-Q:ρ[\ang{x,y}/z]
%:  -----------------------------------------------------(𝐫{strong})
%:      \GG,z:Σx:σ.τ|-(\unpackasin{z}{x,y}{Q}):ρ
%:
%:      ^unpack-ren-1
%:
$$\ded{unpack-ren-1}$$

In an ``unpack'' term like
%
$$\unpackasin{P}{x,y}{Q}$$

the ``unpack'' binds two variables in $Q$, $x$ and $y$,

at the same time, and sets their values to the components

of the (dependent) pair $P$.

\msk

In the presence of $π$ and $π'$ we can {\sl define}:
%
$$(\unpackasin{P}{x,y}{Q}) := Q[x:=πP,y:=π'P].$$

Let's change the ``unpack'' notation one step at a time:

$$\begin{array}{rl}
         & \unpackasin{P}{x,y}{Q} \\
  \funto & \unpackin{P=:x,y}{Q} \\
  \funto & Q[x,y:=P] \\
  \end{array}
$$

\msk

Now let's rewrite the rule:

%:  \GG,z:Σx:σ.τ|-ρ:\Type   \GG,x:σ,y:τ|-Q:ρ[z:=\ang{x,y}]
%:  -----------------------------------------------------
%:      \GG,z:Σx:σ.τ|-Q[x,y:=z]:ρ
%:
%:      ^unpack-ren-2
%:
%:  \vec{a}⠆\vec{A},p⠆(Σb⠆B.C)|-D⠆\Type   \vec{a}⠆\vec{A},b⠆B,c⠆C|-d⠆D[p:=\ang{b,c}]
%:  -----------------------------------------------------
%:      \vec{a}⠆\vec{A},p⠆(Σb⠆B.C)|-d[b,c:=p]⠆D
%:
%:      ^unpack-ren-3
%:
%:  \vec{a}⠆\vec{A},(b,c)⠆(Σb⠆B.C)|-D⠆\Type   \vec{a}⠆\vec{A},b⠆B,c⠆C|-d⠆D[(b,c):=\ang{b,c}]
%:  -----------------------------------------------------
%:      \vec{a}⠆\vec{A},(b,c)⠆(Σb⠆B.C)|-d[b,c:=(b,c)]⠆D
%:
%:      ^unpack-ren-4
%:
%:  \vec{a},(b,c)|-D   \vec{a},b,c|-d
%:  ---------------------------------
%:      \vec{a},(b,c)|-d[b,c:=(b,c)]
%:
%:      ^unpack-ren-5
%:
%:  a,(b,c)|-D   a,b,c|-d
%:  --------------------------Σ𝐫E^+
%:      a,(b,c)|-d[b,c:=(b,c)]
%:
%:      ^unpack-ren-6
%:
%:  a,(b,c)|-D   a,b,c|-d
%:  ---------------------Σ𝐫E^+
%:      a,(b,c)|-d
%:
%:      ^unpack-ren-7
%:

$$\ded{unpack-ren-2}$$
$$\ded{unpack-ren-3}$$
$$\ded{unpack-ren-4}$$

$$\ded{unpack-ren-5}$$

$$\ded{unpack-ren-6}$$

$$\ded{unpack-ren-7}$$

We will use the two last forms.


\newpage
% --------------------
% «dtt-structural-rules»  (to ".dtt-structural-rules")
% (s "DTT: structural rules" "dtt-structural-rules")
\myslide {DTT: structural rules} {dtt-structural-rules}

%:                  a|-b  a|-B=B'
%:  Conversion:     -------------𝐫{conv}
%:                      a|-b'
%:  
%:                      ^10.1-conv
%:  
%:                   a|-B
%:  Projection:     ------𝐫{v}
%:                  a,b|-b
%:  
%:                  ^10.1-var
%:  
%:                  a,b,b',c|-D            a,b,b',c|-d
%:  Contraction:    -----------𝐫{contr}    -----------𝐫{contr}
%:                   a,b,c|-D               a,b,c|-d  
%:  
%:                   ^10.1-Contr            ^10.1-contr
%:  
%:                  a|-b  a,b,c|-D     a|-b  a,b,c|-d
%:  Substitution:   --------------𝐫s   --------------𝐫s
%:                      a,c|-D            a,c|-d     
%:  
%:                      ^10.1-Subst       ^10.1-subst
%:  
%:                  a|-B  a|-C        a|-B  a|-c
%:  Weakening:      ----------𝐫w      ----------𝐫w
%:                    a,b|-C            a,b|-c  
%:  
%:                    ^10.1-Weak        ^10.1-weak
%:  
%:                  a,b,c,d|-E         a,b,c,d|-e
%:  Exchange:       ----------𝐫{exch}  ----------𝐫{exch}
%:                  a,c,b,d|-E         a,c,b,d|-e
%:  
%:                  ^10.1-Exch         ^10.1-exch

These ones are used very often:

$$\begin{array}{lcc}
  \text{Variable:}     & \cded{10.1-var}    \\ \\
  \text{Substitution:} & \cded{10.1-Subst} & \cded{10.1-subst}   \\ \\
  \text{Weakeking:}    & \cded{10.1-Weak}  & \cded{10.1-weak}    \\ \\
  \end{array}
$$

These ones not so much:

$$\begin{array}{lcc}
  \text{Conversion:}   & \cded{10.1-conv}   \\ \\
  \text{Contraction:}  & \cded{10.1-Contr} & \cded{10.1-contr}   \\ \\
  \text{Exchange:}     & \cded{10.1-Exch}  & \cded{10.1-exch}    \\ \\
  \end{array}
$$

Note: ``Variable'' is called ``Projection'' at [Jacobs].


\newpage
% --------------------
% «dtt-type-rules»  (to ".dtt-type-rules")
% (s "DTT: type rules" "dtt-type-rules")
\myslide {DTT: type rules} {dtt-type-rules}

We have four different type-formers:

singleton, (dependent) products, (dependent) sums, and equality.

For each one of them we have a type-building rule, an introduction

rule, and elimination rules.

\msk

There are several options for elimination rules

for dependent sums and equality.

\msk

In a system with ``weak sums'' the rule is $Σ𝐫E^-$.

In a system with ``strong sums'' the rule is $Σ𝐫E^+$,

or, equivalently, $π+π'$.

\msk

In a system with ``weak equality'' the rule is $𝐫{EqE}^-$.

In a system with ``strong equality'' the rule is $𝐫{EqE}^+$,

or, equivalently, ee+ur (``externalization of equality''

plus ``uniqueness of reflexivity'').

%:  
%:                  Type:             Intro:          Elim:
%:  
%:                                                    a|-*' 
%:  Singleton:       ---1              ---1𝐫I        -------1𝐫E
%:                   |-1               |-*           a|-*'=*
%:  
%:                   ^10.1-1           ^10.1-1I      ^10.1-1E
%:  
%:                 a,b|-C             a,b|-c       a|-b  a|-b|->c
%:  DepProds:     ---------Π         --------Π𝐫I   --------------Π𝐫E
%:                a|-Πb:B.C          a|-b|->c          a|-c
%:  
%:                ^10.1-prod         ^10.1-prodI       ^10.1-prodE
%:  
%:                 a,b|-C          a|-B  a,b|-C
%:  DepSums:      ---------Σ       ------------Σ𝐫I       (see below)
%:                a|-Σb:B.C        a,b,c|-(b,c)
%:  
%:                ^10.1-sum         ^10.1-sumI
%:  
%:                  a|-B                  a|-B
%:  Equality:   ----------------𝐫{Eq}   ----------𝐫{EqI}  (see below)
%:              a,b,b'|-𝐫W[b=b']        a,b|-(b=b)
%:  
%:                ^10.1-eq              ^10.1-eqI
  
\def\twol#1#2{\begin{array}[m]{ll}\text{#1} \\ \text{#2}\end{array}}
\def\twol#1#2{\text{#2}}

$$\begin{array}{lccc}
  \text{Singleton:} & \cded{10.1-1}     & \cded{10.1-1I}    & \cded{10.1-1E}    \\ \\ 
  \twol{Dependent}
       {Products:}  & \cded{10.1-prod}  & \cded{10.1-prodI} & \cded{10.1-prodE} \\ \\ 
  \twol{Dependent}
       {Sums:}      & \cded{10.1-sum}   & \cded{10.1-sumI}  & \text{(See below)}  \\ \\                 
  \text{Equality:}  & \cded{10.1-eq}    & \cded{10.1-eqI}   & \text{(See below)}  \\ \\                 
  \end{array}
$$


%:  Elimination rules:
%:                   DepSums:                  Equality:
%:  
%:                a|-D  a,b,c|-d            a,b,b',c|-D  a,b,c|-d
%:  Weak:         --------------Σ𝐫E^-       ---------------------𝐫{EqE}^-
%:                  a,(b,c)|-d               a,b,b',(b=b'),c|-d  
%:  
%:                  ^10.1-sumE-              ^10.1-eqE-
%:  
%:              a,(b,c)|-D  a,b,c|-d        a,b,b',(b=b')|-C  a,b|-c
%:  Strong:     --------------------Σ𝐫E^+   ------------------------𝐫{EqE}^+
%:                  a,(b,c)|-d               a,b,b',(b=b')|-c
%:  
%:                  ^10.1-sumE+              ^10.1-eqE+
%:  
%:               a|-b,c    a|-b,c       a|-(b=b')          a|-(b=b)'   
%:  AltStrong:   ------π   ------π'     ---------𝐫{ee}   ---------------𝐫{ur}
%:                a|-b      a|-c         a|-b=b'         a|-(b=b)'=(b=b)
%:
%:                ^10.1-pi  ^10.1-pi'    ^10.1-ee        ^10.1-ur

$$\begin{array}{ccc}
  \ded{10.1-sumE-} & & \ded{10.1-eqE-} \\ \\
  \ded{10.1-sumE+} & & \ded{10.1-eqE+} \\ \\
  \ded{10.1-pi} \qquad \ded{10.1-pi'} & & \ded{10.1-ee} \quad\;\; \ded{10.1-ur} \\ \\
  \end{array}
$$





\newpage
%
% (eedn4-51-bounded)

% --------------------
% «dtt-alt-sum-rules»  (to ".dtt-alt-sum-rules")
% (s "DTT: alternate rules for strong sum" "dtt-alt-sum-rules")
\myslide {DTT: alternate rules for strong sum} {dtt-alt-sum-rules}


Jacobs, 10.1.3 (i):

The rules $π$ and  $π'$ can be defined from $ΣE^+$:
%:
%:                          a,b|-C                       a|-B
%:                          -------Σ                    ------𝐫v
%:                          a|-Σb.C   a|-B      a,b|-C  a,b|-b
%:                          --------------𝐫w    --------------𝐫w
%:                            a,(b,c)|-B          a,b,c|-b
%:                            ----------------------------ΣE^+
%:  a|-(b,c)        a|-(b,c)            a,(b,c)|-b
%:  --------π       ------------------------------𝐫s
%:    a|-b     :=                a|-b
%:
%:    ^strongsum1                ^strongsum2
%:
%:
%:                                   a,b|-C
%:                                 ==========
%:                                 a,(b,c)|-b   a,b|-C        a,b|-C
%:                                 -------------------𝐫s     --------𝐫v
%:                                     a,(b,c)|-C            a,b,c|-c
%:                                     ------------------------------ΣE^+
%:  a|-(b,c)            a|-(b,c)                   a,(b,c)|-c
%:  --------π'          -------------------------------------𝐫s
%:    a|-c       :=                     a|-c
%:
%:    ^strongsum3                       ^strongsum4
%:
$$\ded{strongsum1} \quad := \quad \ded{strongsum2}$$
$$\ded{strongsum3} \quad := \quad \ded{strongsum4}$$

\bsk
\bsk

The rule $ΣE^+$ can be defined from $π$ and  $π'$:
%:
%:                                                                a,b|-C                 
%:                                                                -------Σ               
%:                                                    a,b|-C      a|-Σb.C   a,b,c|-d     
%:                                                  ==========π   ------------------𝐫{w} 
%:                                    a,b|-C        a,(b,c)|-b    a,(b,c),b,c|-d         
%:                                   ==========π'   -----------------------------𝐫s
%:  a,(b,c)|-D    a,b,c|-d           a,(b,c)|-c       a,(b,c),c|-d                       
%:  ----------------------ΣE^+       ------------------------------𝐫s              
%:         a,(b,c)|-d           :=           a,(b,c)|-d                                      
%:
%:         ^strongsum5                       ^strongsum6
%:
$$
\begin{array}{l}
  \ded{strongsum5} \quad  \\
  \quad := \quad \ded{strongsum6}
\end{array}
$$


\newpage
% --------------------
% «dtt-alt-equality»  (to ".dtt-alt-equality")
% (s "DTT: alternate rules for strong equality" "dtt-alt-equality")
\myslide {DTT: Alternate rules for strong equality} {dtt-alt-equality}


The $Σ𝐫E^+$ rule is equivalent to the two rules ee and ur,

that say that from ``witnesses of equality'' we can prove

external equality - i.e., that some terms are equal.

This equivalence $Σ𝐫E^+ \iff (𝐫{ee},𝐫{ur})$ is of a different

nature from the ones that we have seen before -

this one uses $\bb/\ee/{:=}$ and lives intrinsically in the

(P+T) structure - it cannot be restricted to the T-part

(i.e., to the syntactical world).


$$\begin{array}{rcl}
  a,b,b',e & \vdash & b \\
           & \eqeta & \withvia{b[b':=b, e:=r]}{b=b'}{e} \\
           &    =   & \withvia{b'[b':=b, e:=r]}{b=b'}{e} \\
           & \eqeta & b' \\
  \end{array}
$$

$$\begin{array}{rcl}
  a,b,b',e & \vdash & e \\
           & \eqeta & \withvia{e[b':=b, e:=r]}{b=b'}{e} \\
           &    =   & \withvia{r[b':=b, e:=r]}{b=b'}{e} \\
           & \eqeta & r \\
  \end{array}
$$

\newpage
% --------------------
% «dtt-adjunctions»  (to ".dtt-adjunctions")
% (s "Adjunction diagrams" "dtt-adjunctions")
\myslide {Adjunction diagrams} {dtt-adjunctions}

%D diagram Hyperdoctrine-foo
%D 2Dx     100        +45   +85        +40
%D 2D 100  eq0 =====> eq1   aw0 =====> aw1
%D 2D       -          -     -          -    
%D 2D       |   <-->   |     |   <-->   |    
%D 2D       v          v     v          v    
%D 2D +40  eq2 <===== eq3   aw2 <===== aw3
%D 2D                        -          - 
%D 2D                        |   <-->   | 
%D 2D                        v          v 
%D 2D +40                   aw4 =====> aw5
%D 2D                                        
%D 2D +20  eq4 |----> eq5   aw6 |----> aw7   
%D
%D (( eq0 .tex= \s[a,b|c]          eq1 .tex= \s[a,b,b'|(b{=}b'),c]
%D    eq2 .tex= \s[a,b|d]          eq3 .tex= \s[a,b,b'|d]
%D    @ 0 @ 1 => sl_  @ 0 @ 1 |-> sl^ .plabel= a \co{◻}
%D    @ 2 @ 3 <= sl_  @ 2 @ 3 |-> sl^ .plabel= a {◻}
%D   # @ 0 @ 2 |-> @ 1 @ 3 |-> @ 0 @ 3 harrownodes nil 20 nil <->
%D    @ 0 @ 2 |-> .PLABEL= _(0.43) a,b;c|-d
%D    @ 1 @ 3 |-> .PLABEL= ^(0.43) a,b,b';e,c|-d[\via{b=b'}{e}]
%D    @ 0 @ 2 |-> .PLABEL= _(0.57) a,b;c|-d[b':=b,e:=r]
%D    @ 1 @ 3 |-> .PLABEL= ^(0.57) a,b,b';e,c|-d
%D    @ 0 @ 3 harrownodes nil 20 nil |-> sl^
%D    @ 0 @ 3 harrownodes nil 20 nil <-| sl_
%D ))
%D (( eq4 .tex= a,b      eq5 .tex= a,b,b'
%D    @ 0 @ 1 |->
%D ))
%D (( aw0 .tex= \s[a,b|c]   aw1 .tex= \s[a|b,c]
%D    aw2 .tex= \s[a,b|d]   aw3 .tex= \s[a|d]
%D    aw4 .tex= \s[a,b|e]   aw5 .tex= \s[a|{b|->e}]
%D    @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{◻}
%D    @ 2 @ 3 <= sl_ @ 2 @ 3 |-> sl^ .plabel= a {◻}
%D    @ 4 @ 5 => 
%D    @ 0 @ 2 |-> .PLABEL= _(0.43) a,b;c|-d
%D    @ 1 @ 3 |-> .PLABEL= ^(0.43)   a;p|-d[b,c:=p]
%D    @ 0 @ 2 |-> .PLABEL= _(0.57) a,b;c|-d[p:=\ang{b,c}]
%D    @ 1 @ 3 |-> .PLABEL= ^(0.57)   a;p|-d
%D    @ 0 @ 3 harrownodes nil 20 nil |-> sl^
%D    @ 0 @ 3 harrownodes nil 20 nil <-| sl_
%D    @ 2 @ 4 |-> .PLABEL= _(0.43) a,b;d|-fb
%D    @ 3 @ 5 |-> .PLABEL= ^(0.43)   a;d|-f
%D    @ 2 @ 4 |-> .PLABEL= _(0.57) a,b;d|-e
%D    @ 3 @ 5 |-> .PLABEL= ^(0.57)   a;d|-λb.e
%D    @ 2 @ 5 harrownodes nil 20 nil <-| sl^
%D    @ 2 @ 5 harrownodes nil 20 nil |-> sl_
%D ))
%D (( aw6 .tex= a,b              aw7 .tex= a
%D    @ 0 @ 1 |->
%D ))
%D enddiagram

$$\def\s{\dncdisplay}
  \diag{Hyperdoctrine-foo}
$$

\bsk
\bsk

%D diagram beta-and-eta-for-sums
%D 2Dx     100        +40
%D 2D 100  aw0 =====> aw1   
%D 2D       -          -    
%D 2D       |   <-->   |    
%D 2D       v          v    
%D 2D +40  aw2 <===== aw3   
%D 2D                       
%D 2D +30  bw0 =====> bw1   
%D 2D       -          -    
%D 2D       |   <-->   |    
%D 2D       v          v    
%D 2D +40  bw2 <===== bw3   
%D 2D
%D (( aw0 .tex= \s[a,b|c]   aw1 .tex= \s[a|b,c]
%D    aw2 .tex= \s[a,b|d]   aw3 .tex= \s[a|d]
%D    @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{◻}
%D    @ 2 @ 3 <= sl_ @ 2 @ 3 |-> sl^ .plabel= a {◻}
%D    @ 0 @ 2 |-> .PLABEL= _(0.43) a,b;c|-d
%D    @ 0 @ 2 |-> .PLABEL= _(0.57) a,b;c|-d[b,c:=p][p:=\ang{b,c}]
%D    @ 1 @ 3 |-> .PLABEL= ^(0.43) a;p|-d[b,c:=p]
%D    @ 1 @ 3 |-> .PLABEL= ^(0.57) a;p|-d[b,c:=p]
%D    @ 0 @ 3 harrownodes nil 20 nil |-> sl^
%D    @ 0 @ 3 harrownodes nil 20 nil <-| sl_
%D ))
%D (( bw0 .tex= \s[a,b|c]   bw1 .tex= \s[a|b,c]
%D    bw2 .tex= \s[a,b|d]   bw3 .tex= \s[a|d]
%D    @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{◻}
%D    @ 2 @ 3 <= sl_ @ 2 @ 3 |-> sl^ .plabel= a {◻}
%D    @ 0 @ 2 |-> .PLABEL= _(0.43) a,b;c|-d[p:=\ang{b,c}]
%D    @ 1 @ 3 |-> .PLABEL= ^(0.43) a;p|-d[p:=\ang{b,c}][b,c:=p]
%D    @ 0 @ 2 |-> .PLABEL= _(0.57) a,b;c|-d[p:=\ang{b,c}]
%D    @ 1 @ 3 |-> .PLABEL= ^(0.57) a;p|-d
%D    @ 0 @ 3 harrownodes nil 20 nil |-> sl^
%D    @ 0 @ 3 harrownodes nil 20 nil <-| sl_
%D ))
%D enddiagram

$\def\s{\dncdisplay}
 \diag{beta-and-eta-for-sums}
$






  %
% (eedn4a-bounded)
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")

\newpage
% --------------------
% «ccw1-conversions»  (to ".ccw1-conversions")
% (s "Conversions" "ccw1-conversions")
\myslide {Conversions} {ccw1-conversions}


Conventions:

$\bb$-conversions first, then $\eta$-conversions.

Underlined names are terms.

$▁{(b{=}b)}$ is the reflexivity term.

$\begin{array}{rcl}
  (λb.▁c)▁b &=& ▁c[▁b=:b] \\
     λb.▁fb &=& ▁f         \\
 \unpackasin{\ang{▁b,▁c}}{b,c}{▁d} &=& ▁d[▁b=:b,▁c=:c] \\
 \unpackasin{▁{(b,c)}}{b,c}{▁d[\ang{b,c}=:(b,c)]} &=& ▁d[▁{(b,c)}=:(b,c)] \\
 \withvia {▁d} {b=b} {▁{(b{=}b)}} &=& ▁d \\
 \withvia {▁d[b=:b',▁{(b{=}b)}=:(b{=}b)']} {b'=b} {(b{=}b)'} &=& ▁d \\
 \end{array}
$

\bsk

$$\begin{array}{rcccl}
           a & \vdash & f & \eqbeta & λb.fb                         \\
         a,b & \vdash & e & \eqeta  & (λb.e)b                       \\
       a,b,c & \vdash & d & = & d[b,c:=\ang{b,c}]             \\
         a,p & \vdash & d & = & d[p:=\ang{b,c}][b,c:=p]             \\
       a,b,c & \vdash & d & = & d[\wvia{b=b}{r}]              \\
  a,b,b',e,c & \vdash & d & = & d[b':=b,e:=r][\wvia{b'=b}{e}] \\
  \end{array}
$$

% (find-LATEXfile "edrx08.sty")

%:  \GG,x:σ,x':σ,\DD|-ρ:\Type   \GG,x:σ,\DD[x/x']|-Q:ρ[x/x']
%:  --------------------------------------------------------(𝐫{weak})
%:  \GG,x:σ,x':σ,z:\Eq_σ(x,x'),\DD|-(\withvia{Q}{x'=x}{z}):ρ
%:
%:  ^Jacobs-587.2
%:
%:  a,b,b',c|-D   a,b,c[b=:b']|-d:D[b=:b']
%:  ----------------------------------------------(𝐫{weak})
%:  a,b,b',(b=b'),c|-(\withvia{d}{b'=b}{(b=b')}):D
%:
%:  ^Jacobs-587.2-my
%:
$$\ded{Jacobs-587.2}$$
$$\ded{Jacobs-587.2-my}$$



%

\newpage
% --------------------
% «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))
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}
$$



\newpage
% --------------------
% «dtt-unpack-2»  (to ".dtt-unpack-2")
% (s "The ``unpack'' rule (2)" "dtt-unpack-2")
\myslide {The ``unpack'' rule (2)} {dtt-unpack-2}

In 10.1.2 Jacobs defines (for $P:σ×τ$):

$\begin{array}{rcl}
  πP & \eqdef & \unpackasin{P}{x,y}{x} \\
 π'P & \eqdef & \unpackasin{P}{x,y}{y} \\
 \end{array}
$

i.e.,

$\begin{array}{rcl}
  πP & := & x[x,y:=P] \\
 π'P & := & y[x,y:=P] \\
 \end{array}
$

\bsk

\newpage
% --------------------
% «rules-dtt»  (to ".rules-dtt")
% (s "Rules for DTT" "rules-dtt")
\myslide {Rules for DTT} {rules-dtt}

%%
%% (eedn4a-bounded)

{%\ttchars
\footnotesize
\begin{verbatim}
                a|-b  a|-B=B'
Conversion:     -------------
                    a|-b'

                 a|-B
Projection:     ------
                a,b|-b

                a,b,b',c|-D       a,b,b',c|-d
Contraction:    -----------       -----------
                 a,b,c|-D          a,b,c|-d  

                a|-b  a,b,c|-D    a|-b  a,b,c|-d
Substitution:   --------------    --------------
                    a,c|-D           a,c|-d     

                a|-B  a|-C        a|-B  a|-c
Weakening:      ----------        ----------
                  a,b|-C            a,b|-c  

                a,b,c,d|-E        a,b,c,d|-e
Exchange:       ----------        ----------
                a,c,b,d|-E        a,c,b,d|-e

                Type:             Intro:          Elim:

                                                  a|-*' 
Singleton:       ---               ---           -------
                 |-1               |-*           a|-*'=*

               a,b|-C             a,b|-c      a|-b  a|-b|->c
DepProds:     ---------          --------     --------------
              a|-Πb:B.C          a|-b|->c         a|-c

               a,b|-C          a|-B  a,b|-C
DepSums:      ---------        ------------     (see below)
              a|-Σb:B.C        a,b,c|-(b,c)

                a|-B               a|-B
Equality:   ---------------     ----------      (see below)
            a,b,b'|-W[b=b']     a,b|-(b=b)

Elimination rules:
                 DepSums:                  Equality:

              a|-D  a,b,c|-d          a,b,b',c|-D  a,b,c|-d
Weak:         --------------          ---------------------
                a,(b,c)|-d              a,b,b',(b=b'),c|-d  

            a,(b,c)|-D  a,b,c|-d     a,b,b',(b=b')|-C  a,b|-c
Strong:     --------------------     ------------------------
                 a,(b,c)|-d             a,b,b',(b=b')|-c

             a|-b,c    a|-b,c       a|-(b=b')      a|-(b=b)'   
AltStrong:   ------    ------       ---------   ---------------
              a|-b      a|-c         a|-b=b'    a|-(b=b)'=(b=b)
\end{verbatim}
}








\end{document}

%  __  __       _        
% |  \/  | __ _| | _____ 
% | |\/| |/ _` | |/ / _ \
% | |  | | (_| |   <  __/
% |_|  |_|\__,_|_|\_\___|
%                        
% <make>

 (eepitch-shell)
 (eepitch-kill)
 (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2008comprcat-utf8 veryclean
make -f 2019.mk STEM=2008comprcat-utf8 pdf

 (eepitch-shell)
 (eepitch-kill)
 (eepitch-shell)
cp -v ~/LATEX/2008comprcat.tex /tmp/o
~/LUA/texcatcodes.lua -trans /tmp/o /tmp/o2

# (find-LATEXfile "2008hyp-utf8.tex")
# (find-LATEXfile "2008comprcat.tex")
# (find-fline "~/LUA/texcatcodes.lua")
# (find-fline "/tmp/o2")

% Local Variables:
% coding: utf-8-unix
% ee-tla: "NONE"
% End:

