|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (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: