|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2008comprcat.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008comprcat.tex && latex 2008comprcat.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008comprcat.tex && pdflatex 2008comprcat.tex"))
% (eev "cd ~/LATEX/ && Scp 2008comprcat.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2008comprcat.dvi")
% (find-pspage "~/LATEX/2008comprcat.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2008comprcat.ps 2008comprcat.dvi")
% (find-pspage "~/LATEX/2008comprcat.ps")
% (ee-cp "~/LATEX/2008comprcat.pdf" (ee-twupfile "LATEX/2008comprcat.pdf") 'over)
% (ee-cp "~/LATEX/2008comprcat.pdf" (ee-twusfile "LATEX/2008comprcat.pdf") 'over)
\documentclass[oneside]{book}
\usepackage[latin1]{inputenc}
\usepackage{edrx08} % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty" -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex")
\begin{document}
\input 2008comprcat.dnt
% «.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
$$\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
$\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 -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= 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 +45 +40 +45 +45
%D 2Dx +15 +15
%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 +45 +40 +45 +45
%D 2Dx +15 +15
%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 _| @ 2 _|
%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 +50 +50 +50 +50
%D 2Dx +50 +50 +50 +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 +50 +50 +50 +50
%D 2Dx +50 +50 +50 +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= 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}
(defun s (title tag)
(insert (ee-template
`(("title" ,title)
("tag" ,tag)
("line" ,(ee-no-trailing-nl
(ee-no-properties
(ee-delete-and-extract-line 1))))) "\
% «.{tag}» (to \"{tag}\")
\\newpage
% --------------------
% «{tag}» (to \".{tag}\")
{line}
\\myslide {{title}} {{tag}}
")))
% «elisp» (to ".elisp")
% (s "elisp" "elisp")
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: