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

% «.lemma-4.8.2»	(to "lemma-4.8.2")
% «.quotient-types»	(to "quotient-types")
% «.eq-on-morphisms»	(to "eq-on-morphisms")
% «.eq-on-morphisms-2»	(to "eq-on-morphisms-2")
% «.adjunctions»	(to "adjunctions")


\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 2008quotypes.dnt

%
% (eedn4-51-bounded)

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 {Lemma 4.8.2} {2}
\tocline {Quotient types} {3}
\tocline {How the `Eq' functor acts on morphisms} {4}
\tocline {How the `Eq' functor acts on morphisms (2)} {5}

\def\byR{_{\!/\!R}}
\def\ovl{\overline}
\def\Eq{¯{Eq}}
\def\Ker{¯{Ker}}
%:§_§\!_


\newpage
% --------------------
% «lemma-4.8.2»  (to ".lemma-4.8.2")
% (s "Lemma 4.8.2" "lemma-4.8.2")
\myslide {Lemma 4.8.2} {lemma-4.8.2}

(Jacobs, p.292)

% (find-jacobspage (+ 19 292) "4.8.2. Lemma")

%D diagram ??
%D 2Dx     100    +40        +60
%D 2D  100 A0 |------------\
%D 2D       v               v
%D 2D  +20 A1 |-> A2         A3
%D 2D       v      v        ^
%D 2D  +20 A4 |-> A5 |-----/
%D 2D
%D 2D  +15 B0 |------------> B1
%D 2D         |->    |----->
%D 2D  +20        B2
%D 2D
%D (( A0 .tex= Raa'
%D    A1 .tex= \oa{=}\oa'   A2 .tex= \oa{=}\oa'   A3 .tex= b{=}b'
%D    A4 .tex= b{=}b'       A5 .tex= b{=}b'
%D    B0 .tex= a;a'                               B1 .tex= b;b'
%D                          B2 .tex= \oa;\oa'
%D    A0 A1 |-> A0 A3 |->
%D    A1 A2 |-> .plabel= a {ñ}
%D    A1 A4 |-> A2 A5 |->
%D    A4 A5 |-> .plabel= a {ñ} A5 A3 |-> .plabel= a {ñ}
%D ))
%D (( A0 B2 => A3 B1 <=
%D ))
%D (( B0 B1 |->
%D    B0 B2 |-> B2 B1 |->
%D ))
%D enddiagram
%D
$$\def\oa{\ovl{a}}
  \diag{??}
$$

%D diagram ???
%D 2Dx     100    +40        +60
%D 2D  100 A0 |------------\
%D 2D       v               v
%D 2D  +20 A1 |-> A2         A3
%D 2D       v      v        ^
%D 2D  +20 A4 |-> A5 |-----/
%D 2D
%D 2D  +15 B0 |------------> B1
%D 2D         |->    |----->
%D 2D  +20        B2
%D 2D
%D (( A0 .tex= R
%D    A1 .tex= \Ker(c_R)   A2 .tex= \Eq(I/R)   A3 .tex= \Eq(J)
%D    A4 .tex= \Ker(u)     A5 .tex= \Ker(v)
%D    B0 .tex= I                               B1 .tex= J
%D                          B2 .tex= I/R
%D    A0 A1 -> A0 A3 ->
%D    A1 A2 -> .plabel= a {ñ}
%D    A1 A4 -> A2 A5 ->
%D    A4 A5 -> .plabel= a {ñ} A5 A3 -> .plabel= a {ñ}
%D ))
%D (( A0 B2 |-> A3 B1 <-|
%D ))
%D (( B0 B1 -> .plabel= a u
%D    B0 B2 -> .plabel= b c_R B2 B1 -> .plabel= b v
%D ))
%D enddiagram
%D
$$\def\oa{\ovl{a}}
  \diag{???}
$$

% \end{document}


\newpage
% --------------------
% «quotient-types»  (to ".quotient-types")
% (s "Quotient types" "quotient-types")
\myslide {Quotient types} {quotient-types}

(Jacobs, p.282/290)

% (find-jacobspage (+ 19 282) "4.7_  Quotient types")
% (find-jacobspage (+ 19 290) "4.7_  Quotient types, categorically")

%D diagram quo1
%D 2Dx     100          +35          +35
%D 2D  100 Raa'                     b{=}b'
%D 2D
%D 2D  +20 R^*aa'
%D 2D
%D 2D  +25 a;a'    a\byR;{a'}\byR    b;b'
%D 2D
%D ((  Raa'                     b{=}b'   # 0   1
%D     R^*aa'                            # 2
%D     a;a'    a\byR;{a'}\byR    b;b'    # 3 4 5
%D     @ 0 @ 1 |->
%D     @ 0 @ 2 |-> @ 0 @ 4  => @ 1 @ 5 <=
%D     @ 2 @ 3  =>
%D                 @ 2 @ 4  =>
%D     @ 3 @ 4 |-> @ 4 @ 5 |->
%D     @ 1 @ 4 varrownodes nil 22 nil <->
%D ))
%D enddiagram
%D
$$\diag{quo1}$$

%D diagram quo2
%D 2Dx        100              +40            +55
%D 2D  100 \ovl{R}aa'    a\byR{=}{a'}\byR
%D 2D
%D 2D  +20    Raa'                           b{=}b'
%D 2D
%D 2D  +30                a\byR;{a'}\byR
%D 2D
%D 2D  +20    a;a'                            b;b'
%D 2D
%D (( \ovl{R}aa' a\byR{=}{a'}\byR          # 0 1
%D        Raa'                     b{=}b'  # 2   3
%D                 a\byR;{a'}\byR          #   4
%D        a;a'                      b;b'   # 5   6
%D    @ 0 @ 1 <= sl_ @ 0 @ 1 |-> sl^ .plabel= a ñ
%D    @ 0 @ 2 <-| @ 1 @ 4 <=  @ 1 @ 3 |->
%D    @ 2 @ 5  => @ 2 @ 4  => @ 2 @ 3 |-> @ 3 @ 6 <=
%D    @ 5 @ 4 |-> @ 4 @ 6 |-> @ 5 @ 6 |->
%D ))
%D enddiagram
%D
$$\diag{quo2}$$


\bsk
%:
%:  a,a'|-Ï[Raa']       a|-b            a|-b   a|-b'
%:  -------------Q    --------QI    ----------------------QI=
%:      |-A/R         a|-b\byR      a,Rbb'|-b\byR={b'}\byR
%:
%:      ^Q               ^QI              ^QI=
%:
%:
%:  a,b|-c_b  a,b,b',Rbb'|-c_b=c_{b'}          a|-b   a|-b'
%:  ---------------------------------QE    ------------------------Qeff
%:       a,b\byR|-c_{b\byR}                a,b\byR{=}{b'}\byR|-Rbb'
%:
%:         ^QE                                ^Qeff
%:
$$\ded{Q} \qquad \ded{QI} \qquad \ded{QI=}$$
$$\ded{QE} \qquad \ded{Qeff}$$


\newpage
% --------------------
% «eq-on-morphisms»  (to ".eq-on-morphisms")
% (s "How the `Eq' functor acts on morphisms" "eq-on-morphisms")
\myslide {How the `Eq' functor acts on morphisms} {eq-on-morphisms}

% (find-jacobspage (+ 19 291) "\"equality relation\" functor")
(Jacobs, p.291)

% (find-LATEX "2008hyp.tex" "dep-eq-from-simple-eq")

%D diagram QEq1-dnc
%D 2Dx    100     +45                +55   +45
%D 2Dx    100     +55                +60   +55
%D 2D 100 B0 <==> B0' <============= B1
%D 2D	  -\\      -                 -\\
%D 2D	  | \\     |       <--|      | \\
%D 2D	  v  \\    v                 v  \\
%D 2D +20 B2 <\\> B2' <============= B3  \\
%D 2D	   /\  \/                     /\  \/
%D 2D +15   \\   B4                    \\  B5
%D 2D	     \\  -                      \\ -
%D 2D	      \\ |                       \\|
%D 2D	       \\v                        \v
%D 2D +20        B6 <===================== B7
%D 2D
%D 2D +10 b0 |---------------------> b1
%D 2D	     |->                        |->
%D 2D +35        b2 |--------------------> b3
%D 2D
%D ((
%D    B0 .tex= §      B0' .tex= §     x+= -3    B1 .tex= a{=}a
%D    B2 .tex= b{=}b  B2' .tex= b{=}b x+= -3    B3 .tex= b{=}b
%D    B4 .tex= a{=}a'                           B5 .tex= b{=}b'
%D    B6 .tex= b{=}b'                           B7 .tex= b{=}b'
%D  # B0 B0' <-| sl^ .plabel= a î
%D    B0 B0' |->     .plabel= a ÐP§
%D    B0 B2 |-> B0' B2' |-> B2 B2' <-|
%D    B1 B3  |-> B0' B1 <= B2' B3 <=
%D    B0 B4 => B1 B5 =>
%D    B2 B6 <= B3 B7 <=
%D    B6 B7 <= B6 B7 |-> sl^^ .plabel= a {ñ}
%D    B5 B7 |-> .plabel= r \id
%D    B4 B6 |->
%D  # B4 B6 <-| sl^ .plabel= r Ð{BCC}Î
%D    B0  B2  midpoint B0' B2' midpoint  harrownodes 7 17 nil <-|
%D    B0' B2' midpoint B1  B3  midpoint  harrownodes nil 20 nil <-|
%D    B0  B2  midpoint B4  B6  midpoint dharrownodes nil 20 nil |->
%D    B1  B3  midpoint B5  B7  midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a b1 .tex= b b2 .tex= a,a' b3 .tex= b,b'
%D    b0 b1 |-> b0 b2 |-> b1 b3 |-> b2 b3 |->
%D  # b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{QEq1-dnc}$$

%D diagram QEq1-std
%D 2Dx    100     +55                +60   +55
%D 2D 100 B0 <==> B0' <============= B1
%D 2D	  -\\      -                 -\\
%D 2D	  | \\     |       <--|      | \\
%D 2D	  v  \\    v                 v  \\
%D 2D +20 B2 <\\> B2' <============= B3  \\
%D 2D	   /\  \/                     /\  \/
%D 2D +15   \\   B4                    \\  B5
%D 2D	     \\  -                      \\ -
%D 2D	      \\ |                       \\|
%D 2D	       \\v                        \v
%D 2D +20        B6 <===================== B7
%D 2D
%D 2D +10 b0 |---------------------> b1
%D 2D	     |->                        |->
%D 2D +35        b2 |--------------------> b3
%D 2D
%D ((
%D    B0 .tex= §_I                     B0' .tex= u^*§_J           x+= 3    B1 .tex= §_J
%D    B2 .tex= _I^*(u{×}u)^*\Eq_J§_J  B2' .tex= u^*_J^*\Eq_J§_J x+= 3    B3 .tex= _J^*\Eq_J§_J
%D    B4 .tex= \Eq_I§_I                                                    B5 .tex= \Eq_J§_J
%D    B6 .tex= (u{×}u)^*\Eq_J§_J                                           B7 .tex= \Eq_J§_J
%D  # B0 B0' <- sl^ .plabel= a î
%D    B0 B0' ->     .plabel= a ÐP§
%D    B0 B2 -> B0' B2' -> B2 B2' <-
%D    B1 B3  -> B0' B1 <-| B2' B3 <-|
%D    B0 B4 |-> B1 B5 |->
%D    B2 B6 <-| B3 B7 <-|
%D    B6 B7 <-| B6 B7 -> sl^^ .PLABEL= ^(0.5) {ñ}
%D    B5 B7 -> .plabel= r \id
%D    B4 B6 ->
%D  # B4 B6 <- sl^ .plabel= r Ð{BCC}Î
%D    B0  B2  midpoint B0' B2' midpoint  harrownodes  7  17 nil <-|
%D    B0' B2' midpoint B1  B3  midpoint  harrownodes nil 20 nil <-|
%D    B0  B2  midpoint B4  B6  midpoint dharrownodes  5  20 nil |->
%D    B1  B3  midpoint B5  B7  midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= I b1 .tex= J b2 .tex= I×I b3 .tex= J×J
%D    b0 b1 -> .plabel= b u
%D    b0 b2 -> .plabel= l _I
%D    b1 b3 -> .plabel= b _J
%D    b2 b3 -> .plabel= r u×u
%D  # b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{QEq1-std}$$


\newpage
% --------------------
% «eq-on-morphisms-2»  (to ".eq-on-morphisms-2")
% (s "How the `Eq' functor acts on morphisms (2)" "eq-on-morphisms-2")
\myslide {How the `Eq' functor acts on morphisms (2)} {eq-on-morphisms-2}

% (find-jacobspage (+ 19 291) "\"equality relation\" functor")
(Jacobs, p.291)

%:           u;(J)=(I);u×u     \Eq_J(§(J))
%:    ----------------------------------------------
%:    u^*(J)^*\Eq_J(§(J))->(I)^*(u×u)^*\Eq_J(§(J))
%:  
%:                ^Eq1a
%:  
%:                            \Eq_J(§(J))->\Eq_J(§(J))                          
%:                            ------------------------                          
%:                       u     §(J)->(J)^*\Eq_J(§(J))                          
%:                       -------------------------------                        
%:  §(I)  u  §(J)        u^*(§(J))->u^*(J)^*\Eq_J(§(J))      u;(J)=(I);u×u
%:  ---------------ÐP§   ----------------------------------------------------
%:  §(I)->u^*(§(J))                 u^*(§(J))->(I)^*(u×u)^*\Eq_J(§(J))
%:  -------------------------------------------------------------------
%:            §(I)->(I)^*(u×u)^*\Eq_J(§(J))     
%:            ------------------------------     
%:            \Eq_I(§(I))->(u×u)^*\Eq_J(§(J))
%:
%:                 ^Eq1b
%:
%:                                          u×u   \Eq_J(§(J))
%:                                     ------------------------------{ñ}
%:  \Eq_I(§(I))->(u×u)^*\Eq_J(§(J))    (u×u)^*\Eq_J(§(J))->\Eq_J(§(J))  
%:  ------------------------------------------------------------------
%:                  \Eq_I(§(I))->\Eq_J(§(J))
%:  
%:                         ^Eq1c
%:  
$$\ded{Eq1a}$$
$$\ded{Eq1b}$$
$$\ded{Eq1c}$$

\msk

%:   (a|->b|->b,b')=(a|->a,a'|->b,b')   \ssst{b,b'}{b{=}b'}
%:   ------------------------------------------------------
%:                 a||b{=}b|-b{=}b
%:
%:                 ^Eq1a-dnc
%:
%:                                             b,b'||b{=}b'|-b{=}b'
%:                                             -------------------
%:                                      a|->b      b||§|-b{=}b
%:                                      ----------------------
%:   \ssst{a}{§}  a|->b  \ssst{b}{§}               a||§|-b{=}b    (a|->b|->b,b')=(a|->a,a'|->b,b)
%:   -------------------------------               ----------------------------------------------
%:                a||§|-§                                       a||§|-b{=}b
%:                ---------------------------------------------------------
%:                                 a||§|-b{=}b
%:                             -------------------
%:                             a,a'||a{=}a'|-b{=}b'
%:
%:                             ^Eq1b-dnc
%:
%:                             a,a'|->b,b'   \ssst{b,b'}{b{=}b'}
%:                          ---------------------------------------
%:   a,a'||a{=}a'|-b{=}b'   (a,a'\,||\,b{=}b')|->(b,b'\,||\,b{=}b')
%:   --------------------------------------------------------------
%:             (a,a'\,||\,a{=}a')|->(b,b'\,||\,b{=}b')
%:
%:                             ^Eq1c-dnc
%:
$$\ded{Eq1a-dnc}$$
$$\ded{Eq1b-dnc}$$
$$\ded{Eq1c-dnc}$$


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

% (find-LATEX "2008comprcat.tex" "ccw1")
% (find-jacobspage (+ 19 294) "4.8.3. Theorem")
(Jacobs, p.294)

%D diagram ??
%D 2Dx         100   +20  +20  +20   +20
%D 2D  100           § ======> a=a'      
%D 2D                v          v        
%D 2D  +20         {}Rbb <==== Rbb'{}    
%D 2D                  <==        <==    
%D 2D  +20           a |-----> a,a'      
%D 2D  +10               Rbb <====== Rbb'
%D 2D             <-|  |->        |->    
%D 2D  +20 b|_{Rbb} `---> b |------> b,b'
%D 2D                                    
%D 2D
%D ((            §         a=a'        #  0 1
%D             {}Rbb       Rbb'{}      #  2 3
%D                   Rbb         Rbb'  #   4 5
%D     @ 0 @ 1 =>
%D     @ 0 @ 2 |-> @ 1 @ 3 |->
%D     @ 2 @ 3 <=
%D     @ 2 @ 4 <= @ 3 @ 5 <=
%D     @ 4 @ 5 <=
%D ))
%D ((            a         a,a'        #  0 1
%D     b|_{Rbb}       b          b,b'  # 2 3 4
%D     @ 0 @ 1 |->   @ 0 @ 2 <-| @ 0 @ 3 |-> @ 1 @ 4 |->
%D     @ 2 @ 3 `-> @ 3 @ 4 |->
%D ))
%D (( Rbb b|_{Rbb} =>
%D    Rbb b =>
%D ))
%D enddiagram
%D
$$\diag{??}$$

%D diagram 4.8.3
%D 2Dx     100          +40         +40         +40         +40
%D 2D  100 Raa' |-----------------> b=b' |----------------> Scc'
%D 2D	    ||  \\                   /\                  //  || 
%D 2D	    ||   \\                  ||                 //   || 
%D 2D	    \/    \/                 ||                \/    \/ 
%D 2D  +20 a;a' |-->> a/R;a'/R |--> b;b' |--> c|S;c'|S `--> c;c'
%D 2D
%D (( Raa'            b=b'            Scc'      # 0   1   2
%D    a;a'  a/R;a'/R  b;b'  c|S;c'|S  c;c'      # 3 4 5 6 7
%D          c|S;c'|S .tex= c|_{Scc},c'|_{Sc'c'}            
%D    @ 0 @ 1 |-> @ 1 @ 2 |->
%D    @ 0 @ 3 => @ 0 @ 4 => @ 1 @ 5 <= @ 2 @ 6 => @ 2 @ 7 =>
%D    @ 3 @ 4 |->> @ 4 @ 5 |-> @ 5 @ 6 |-> @ 6 @ 7 `->
%D ))
%D enddiagram
%D
$$\diag{4.8.3}$$









%

\end{document}

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