% (find-angg "LATEX/2010comprcats.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2010comprcats.tex && latex    2010comprcats.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2010comprcats.tex && pdflatex 2010comprcats.tex"))
% (eev "cd ~/LATEX/ && Scp 2010comprcats.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (defun d () (interactive) (find-dvipage "~/LATEX/2010comprcats.dvi"))
% (find-dvipage "~/LATEX/2010comprcats.dvi")
% (find-pspage  "~/LATEX/2010comprcats.pdf")
% (find-pspage  "~/LATEX/2010comprcats.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2010comprcats.ps 2010comprcats.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2010comprcats.ps 2010comprcats.dvi && ps2pdf 2010comprcats.ps 2010comprcats.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage  "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2010comprcats.pdf" (ee-twupfile "LATEX/2010comprcats.pdf") 'over)
% (ee-cp "~/LATEX/2010comprcats.pdf" (ee-twusfile "LATEX/2010comprcats.pdf") 'over)

% «.transl-ccw1»		(to "transl-ccw1")
% «.transl-jacobs-dtt»		(to "transl-jacobs-dtt")

\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 2010comprcats.dnt

%
% (eedn4-51-bounded)

%\mylosopen{tmp.los}
%\def\myslide   #1#2{\newpage{\bf #1}\par\label{#2}\addtolos{#1}}

%\mylosopen{tmp.los}
\def\myslide   #1#2{\newpage{\bf #1}\par\label{#2}}

%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")

% --------------------
% «transl-ccw1»  (to ".transl-ccw1")
% (s "Translation: Comprehension Categories" "transl-ccw1")
\myslide {Translation: Comprehension Categories} {transl-ccw1}

% (find-LATEX "2008comprcat.tex")
% (find-LATEX "2008comprcat.tex" "ccw1")
% (find-dvipage "~/LATEX/2008comprcat.dvi" 10)
% (find-jacobspage (+ 19 616) "Definition 10.4.7")

The diagrams below are for a theorem hidden

inside def.\ 10.4.7 of [Jacobs99] (p.\ 616;

``Comprehension Categories with Unit'') ---

the theorem says that in a CCw1 the natural transformation

$\ssst{b}{Q(b)} \TNto (\sst{b}{Q(b)} \to B)$

(`$\pi:\{·\} \to p$' in Jacobs's notation)

takes cartesian morphisms in $\bbE$ to

pullback squares in $\bbB$.

\msk

In the left half below we use Jacobs's notation,

in the right half a downcased notation closer to

the archetypical model (``$\CanSub(\Set)$ is a CCw1'').



%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    # In CanSub(Set):
%D                      a0 .tex= \s[a|§]
%D    a1 .tex= a|_§     a2 .tex=    a         a3 .tex= \s[b|R]
%D                      a4 .tex=    b|_R      a5 .tex=    b
%D    a6 .tex= \s[a|§]  a7 .tex= \s[{c|_R}|§]                   a8 .tex= \s[c|R]
%D    a9 .tex=    a    a10 .tex=    c|_R      a11 .tex=   c|_R  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

$$\diag{ccwu-pb}
  \qquad
  \diag{ccwu-pb-dnc}
$$



% --------------------
% «transl-jacobs-dtt»  (to ".transl-jacobs-dtt")
% (s "Translation: Jacobs's notation for DTT" "transl-jacobs-dtt")
\myslide {Translation: Jacobs's notation for DTT} {transl-jacobs-dtt}

\def\vvGG {\vec v¨\Gamma}
\def\vvGGx{\vec v¨\Gamma,x¨}

\def\vv{\vec v}

\def\pover#1#2{\begin{pmatrix} #1 \\ \dnto \\ #2 \end{pmatrix}}
\def\pog #1{\pover{\Gamma;#1}{\Gamma}}
\def\pogx#1{\pover{\Gamma,x¨;#1}{\Gamma,x¨}}
\def\bigsum {\displaystyle\sum }
\def\bigprod{\displaystyle\prod}

\def\unpackasin#1#2#3{\text}
\def\sfop#1{\operatorname{\sf #1}}
\def\unpack{\sfop{unpack}}
\def\unpackasin#1#2#3{\sfop{unpack} #1 \sfop{as} \ang{#2} \sfop{in} #3}

% (find-books "__cats/__cats.el" "jacobs")
% (find-jacobspage (+ 19 586) "10.3.3." "(i) Dependent products")
% (find-jacobspage (+ 19 606) "10.3.3." "(i) Dependent products")
% (find-jacobspage (+ 19 606) "10.3.3." "(ii) Weak dependent sums")

Jacobs, p.586, rules for DTT ($åI/ð$, $åE/\app$, $ÆI/\ang,$, $ÆEw/\unpack$); 

Jacobs, p.606, prop.\ 10.3.3,

(i) Dependent products, and

(ii) Weak dependent sums:

%D diagram Jacobs-10.3.3.(i),(ii)
%D 2Dx     100    +55        +65     +65
%D 2D  100        c |-----> b,c ==== b,c'
%D 2D             |          |
%D 2D             |   |-->   |
%D 2D             |   <--|   |
%D 2D             v          v
%D 2D  +50 d'' == d' <-----| d
%D 2D             |          |
%D 2D             |   <--|   |
%D 2D             |   |-->   |
%D 2D             v          v
%D 2D  +50        e |-----> b>e ==== b>e'
%D 2D
%D 2D  +30       a,b |-----> a
%D 2D
%D (( c .tex= \pogx{y¨}   b,c .tex= \pog{z¨Æx¨.}  b,c' .tex= \bigprod\pogx{y¨}
%D    e .tex= \pogx{y¨}   b>e .tex= \pog{z¨åx¨.}  b>e' .tex= \bigsum\pogx{y¨}
%D    d'' .tex= ^*\pog{w¨}  d' .tex= \pogx{w¨}    d .tex= \pog{w¨}
%D    a,b .tex= (\vv¨\Gamma,x¨)   a .tex= (\vv¨\Gamma)
%D    c b,c |-> b,c b,c' =
%D    e b>e |-> b>e b>e' =
%D    d'' d' = d' d <-|
%D    c d harrownodes nil 20 nil |-> sl^ .plabel= a \flat\,/\,ÆEw\,/\unpack
%D    c d harrownodes nil 20 nil <-| sl_ .plabel= b \sharp\,/\,ÆI\,/\,\ang{,}
%D    e d harrownodes nil 20 nil <-| sl^ .plabel= a \flat\,/\,åE\,/\app
%D    e d harrownodes nil 20 nil |-> sl_ .plabel= b \sharp\,/\,åI\,/\,ð
%D      # Labels on the left side:
%D    c d' -> .PLABEL= _(0.43) \vvGG,x¨;y¨|-N¨
%D    c d' -> .PLABEL= _(0.57) \vvGG,x¨;y¨|-M[\ang{x,y}/z]:
%D    d' e -> .PLABEL= _(0.43) \vvGG,x¨;w¨|-Mx¨
%D    d' e -> .PLABEL= _(0.57) \vvGG,x¨;w¨|-N¨
%D      # Labels on the right side:
%D    b,c d -> .PLABEL= ^(0.43) \vvGG,x¨;y¨|-(\unpackasin{z}{x,y}{N})¨
%D    b,c d -> .PLABEL= ^(0.57) \vvGG,z¨Æx¨.|-M:
%D    d b>e -> .PLABEL= ^(0.43) \vvGG;w¨|-M¨åx:.
%D    d b>e -> .PLABEL= ^(0.57) \vvGG;w¨|-(ðx¨.N)¨åx:.
%D    a,b a -> .plabel= a \pi
%D ))
%D enddiagram
%D
$$\diag{Jacobs-10.3.3.(i),(ii)}$$





%

\end{document}

% Local Variables:
% coding:           raw-text-unix
% ee-anchor-format: "«%s»"
% End:
