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

% (find-angg ".emacs" "dnc-to-std")
% (find-angg ".emacs" "std-to-dnc")

% «.adjs-of-change-of-base»	(to "adjs-of-change-of-base")
% «.new-bcc-1»			(to "new-bcc-1")
% «.bcc-categorically»		(to "bcc-categorically")
% «.bcc-hyperdoctrine»		(to "bcc-hyperdoctrine")
% «.bcc-collapse»		(to "bcc-collapse")
% «.bcc-sums-full-diag»		(to "bcc-sums-full-diag")
% «.bcc-smaller-diagram»	(to "bcc-smaller-diagram")
% «.bcc-smaller-diagrams»	(to "bcc-smaller-diagrams")
% «.bcc-trees»			(to "bcc-trees")
% «.first-preservations»	(to "first-preservations")
% «.first-preservations-2»	(to "first-preservations-2")


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

%
% (eedn4-51-bounded)

\def\Eq{\mathsf{Eq}}
%:'*^{\prime*}
%:&\&
%:\&\&
%:b=b'b{=}b'


{\bf These notes are being changed!!!}

\bsk

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 {Adjoints to change of base} {2}
\tocline {BCC, categorically} {3}
\tocline {BCC in a hyperdoctrine} {4}
\tocline {BCC: collapsing isomorphic objects} {5}
\tocline {BCC for dependent sums: full diagram} {6}
\tocline {BCC: smaller diagram} {7}
\tocline {BCC: smaller diagrams} {8}
\tocline {BCC: trees} {9}
\tocline {First preservations} {10}
\tocline {First preservations (2)} {11}



\newpage
% --------------------
% «adjs-of-change-of-base»  (to ".adjs-of-change-of-base")
% (s "Adjoints to change of base" "adjs-of-change-of-base")
\myslide {Adjoints to change of base} {adjs-of-change-of-base}


%D diagram adjs-to-change-of-base
%D 2Dx     100     +30    +30     +35    +30     +40    
%D 2D  100 A0 ===> A1     B0 ===> B1     C0 ===> C1     
%D 2D      -       -      -       -      -       -                                             
%D 2D      |  <->  |      |  <->  |      |  <->  |                                             
%D 2D      v       v      v       v      v       v            
%D 2D  +20 A2 <=== A3     B2 <=== B3     C2 <=== C3     
%D 2D      -       -      -       -      -       -                                             
%D 2D      |  <->  |      |  <->  |      |  <->  |                                             
%D 2D      v       v      v       v      v       v            
%D 2D  +20 A4 ===> A5     B4 ===> B5     C4 ===> C5     
%D 2D                                                   
%D 2D  +20 a0 |--> a1     b0 |--> b1     c0 |--> c1     
%D 2D
%D (( A0 .tex= Pab  A1 .tex= Îb.Pab
%D    A2 .tex= Qa   A3 .tex= Qa
%D    A4 .tex= Rab  A5 .tex= ýb.Rab
%D    a0 .tex= a,b  a1 .tex= a
%D    A0 A1 =>
%D    A0 A2 |-> A1 A3 |-> A0 A3 harrownodes nil 20 nil <->
%D    A2 A3 <=
%D    A2 A4 |-> A3 A5 |-> A2 A5 harrownodes nil 20 nil <->
%D    A4 A5 =>
%D    a0 a1 |->
%D ))
%D (( B0 .tex= Pab    B1 .tex= b=b'&Pabb
%D    B2 .tex= Qabb   B3 .tex= Qabb'
%D    B4 .tex= Rab    B5 .tex= b=b'¶Rab
%D    b0 .tex= a,b  b1 .tex= a,b,b'
%D    B0 B1 =>
%D    B0 B2 |-> B1 B3 |-> B0 B3 harrownodes nil 20 nil <->
%D    B2 B3 <=
%D    B2 B4 |-> B3 B5 |-> B2 B5 harrownodes nil 20 nil <->
%D    B4 B5 =>
%D    b0 b1 |->
%D ))
%D (( C0 .tex= Pa    C1 .tex= Îa.a=fb.Pb
%D    C2 .tex= Qfa   C3 .tex= Qb
%D    C4 .tex= Ra    C5 .tex= ýa.a=fb¶Pb
%D    c0 .tex= a     c1 .tex= b
%D    C0 C1 =>
%D    C0 C2 |-> C1 C3 |-> C0 C3 harrownodes nil 20 nil <->
%D    C2 C3 <=
%D    C2 C4 |-> C3 C5 |-> C2 C5 harrownodes nil 20 nil <->
%D    C4 C5 =>
%D    c0 c1 |-> .plabel= a f
%D ))
%D enddiagram
%D
$$\diag{adjs-to-change-of-base}$$

% \end{document}




% \end{document}


\newpage
% --------------------
% «bcc-categorically»  (to ".bcc-categorically")
% (s "BCC, categorically" "bcc-categorically")
\myslide {BCC, categorically} {bcc-categorically}

This is how the Beck-Chevalley condition (for dependent sums;

there is also a variation for dependent products, that we will

see soon) is usually stated:

\begin{quotation}

``If the square formed by $f,g,f',g'$ in the base category

in the diagram below is a pullback, and if $P$ is an object

over $C$, then the natural map from $\sum_{f'}g^{\prime*}P$ to $g^*\sum_{f}P$

is an isomorphism.''

\end{quotation}

The upper part of the diagram below shows how to build the map

$î: \sum_{f'}g^{\prime*}P \to g^*\sum_{f}P$.

\bsk

But what does that {\sl mean}?

%D diagram big-bcc-cat
%D 2Dx    100    +45     +45         +60   +45
%D 2D 100 B0 ======================> B1
%D 2D	  -/\                        -
%D 2D	  | \\                       |
%D 2D	  v  \\                      v
%D 2D +30 B2 <\> B2' <-> B2'' <===== B3
%D 2D	   /\  \\                     /\
%D 2D +30   \\   B4 =====================> B5
%D 2D	     \\  -                      \\ -
%D 2D	      \\ |                       \\|
%D 2D	       \\v                        \v
%D 2D +30        B6 <===================== B7
%D 2D
%D 2D +20 b0 <-> b0' <-> b0'' |----> b1
%D 2D	     |->                        |->
%D 2D +60        b2 |--------------------> b3
%D 2D
%D #       g'*P |------------------> Îf'g'*P
%D #        | ^                        |
%D #        |  \       |--->           |
%D #        v   \                      v
%D #   g'*f*ÎfP <\-> f'*g*ÎfP <-----| g*ÎfP
%D #         /\   -                     ^
%D #          \    P |--------------------> ÎfP
%D #           \   |                      \  -
%D #            \  |         <---|         \ | id
%D #             - v                        -v
%D #             f*ÎfP <------------------| ÎfP
%D #
%D #        Ax_{B}C -----------------> A
%D #           \  __|      f'            \
%D #         g' \                         \ g
%D #             v                         v
%D #               C ---------------------> B
%D #                         f
%D ((
%D    B0 .tex= g'*P        B1  .tex= Î_{f'}g'*P
%D    B2 .tex= g'*f^*Î_fP  B2' .tex= h^*Î_{f}P B2'' .tex= f'*g^*Î_fP
%D                         B3  .tex= g^*Î_{f}P
%D    B4 .tex= P           B5  .tex= Î_fP
%D    B6 .tex= f^*Î_fP     B7  .tex= Î_fP
%D    B0 B1 |-> B0 B2 -> B0 B2' -> B0 B2'' -> B1 B3 -> .plabel= l {î}
%D    B2 B2' <-> B2' B2'' <-> B2'' B3 <-|
%D    B0 B4 <-| B2 B6 <-| B2' B7 <-| B3 B7 <-|
%D    B4 B5 |-> B4 B6 -> B5 B7 -> .plabel= r \id B6 B7 <-|
%D    B0 B2'' midpoint B1 B3 midpoint  harrownodes nil 20 nil ->
%D    B0 B2   midpoint B4 B6 midpoint dvarrownodes nil 18 nil <-
%D    B4 B7   harrownodes nil 20 nil <-
%D ))
%D (( b0 .tex= A×_{B}C b0' .tex= A×_{B}C b0'' .tex= A×_{B}C  b1 .tex= A
%D    b2 .tex= C                                             b3 .tex= B
%D    b0 b0' =  b0' b0'' =  b0'' b1 -> .plabel= b f'
%D    b0 b2 -> .plabel= l g'  b0' b3 -> .plabel= l h  b1 b3 -> .plabel= l g
%D    b2 b3 -> .plabel= b f
%D    b0 relplace 18 10 \pbsymbol{10}
%D ))
%D enddiagram

$$\defÎ{\sum}
  \diag{big-bcc-cat}
$$


\newpage
% --------------------
% «bcc-hyperdoctrine»  (to ".bcc-hyperdoctrine")
% (s "BCC in a hyperdoctrine" "bcc-hyperdoctrine")
\myslide {BCC in a hyperdoctrine} {bcc-hyperdoctrine}

\widemtos

In the case of a hyperdoctrine that means that from an

object $\ssst{b,c}{P}$  and a map $a \mto b$ there are two ways to

build an object that deserves the name ``$\ssst{a}{Îc.P}$''...

\msk

...and without BCC we would know a map between them

going in one direction, $î: \ssst{a}{Îc.P} \to \ssst{a}{Îc.P}'$,

but we wouldn't know that it is an iso.

%D diagram big-bcc-logical
%D 2Dx    100    +40     +40         +60   +40
%D 2D 100 B0 ======================> B1
%D 2D	  -/\                        -
%D 2D	  | \\                       |
%D 2D	  v  \\                      v
%D 2D +30 B2 <\> B2' <-> B2'' <===== B3
%D 2D	   /\  \\                     /\
%D 2D +30   \\   B4 =====================> B5
%D 2D	     \\  -                      \\ -
%D 2D	      \\ |                       \\|
%D 2D	       \\v                        \v
%D 2D +30        B6 <===================== B7
%D 2D
%D 2D +20 b0 <-> b0' <-> b0'' |----> b1
%D 2D	     |->                        |->
%D 2D +60        b2 |--------------------> b3
%D 2D
%D ((
%D    B0 .tex= \s[a,c|P]   B1  .tex= \s[a|Îc.P]
%D    B2 .tex= \s[a,c|Îc.P] B2' .tex= \s[a,c|Îc.P]' B2'' .tex= \s[a,c|Îc.P]''
%D                          B3  .tex= \s[a|Îc.P]'
%D    B4 .tex= \s[b,c|P]    B5  .tex= \s[b|Îc.P]
%D    B6 .tex= \s[b,c|Îc.P] B7  .tex= \s[b|Îc.P]
%D    B0 B1 => B0 B2 |-> B0 B2' |-> B0 B2'' |-> B1 B3 |-> .plabel= l {î}
%D    B2 B2' <-> B2' B2'' <-> B2'' B3 <=
%D    B0 B4 <= B2 B6 <= B2' B7 <= B3 B7 <=
%D    B4 B5 => B4 B6 |-> B5 B7 |-> .plabel= r \id B6 B7 <=
%D    B0 B2'' midpoint B1 B3 midpoint  harrownodes nil 20 nil |->
%D    B0 B2   midpoint B4 B6 midpoint dvarrownodes nil 18 nil <-|
%D    B4 B7   harrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a,c b0' .tex= a,c b0'' .tex= a,c   b1 .tex= a
%D    b2 .tex= b,c b0'                            b3 .tex= b
%D    b0 b0' =  b0' b0'' =  b0'' b1 |->
%D    b0 b2 |-> b0' b3 |->  b1 b3 |->
%D    b2 b3 |->
%D    b0 relplace 18 10 \pbsymbol{10}
%D ))
%D enddiagram

% BCC: full diagram (no isos hidden), in $\Sub(\Set)$.

$$\diag{big-bcc-logical}$$

\newpage
% --------------------
% «bcc-collapse»  (to ".bcc-collapse")
% (s "BCC: collapsing isomorphic objects" "bcc-collapse")
\myslide {BCC: collapsing isomorphic objects} {bcc-collapse}

One trick to make the previous (big) diagram simpler to draw

is to draw the objects that are isomorphic and ``deserve the same

name'' --- but that may be different --- as a single object; these

collapsed objects (here just $\ssst{a,c}{Îc.P}$) have more than one

functor arrow pointing to them, which indicates that they have

more than one construction.


%D diagram big-bcc-logical-collapsed
%D 2Dx    100    +40                 +50   +40
%D 2D 100 B0 ======================> B1
%D 2D	  -/\                        -
%D 2D	  | \\                       |
%D 2D	  v  \\                      v
%D 2D +30 B2 <\\==================== B3
%D 2D	   /\  \\                     /\
%D 2D +20   \\   B4 =====================> B5
%D 2D	     \\  -                      \\ -
%D 2D	      \\ |                       \\|
%D 2D	       \\v                        \v
%D 2D +30        B6 <===================== B7
%D 2D
%D 2D +20 b0 |---------------------> b1
%D 2D	     |->                        |->
%D 2D +50        b2 |--------------------> b3
%D 2D
%D ((
%D    B0 .tex= \s[a,c|P]     B1 .tex= \s[a|Îc.P]
%D    B2 .tex= \s[a,c|Îc.P]  B3 .tex= \s[a|Îc.P]'
%D    B4 .tex= \s[b,c|P]     B5 .tex= \s[b|Îc.P]
%D    B6 .tex= \s[b,c|Îc.P]  B7 .tex= \s[b|Îc.P]
%D    B0 B1 => B0 B2 |-> B1 B3 |-> .plabel= l {î}
%D    B2 B3 <=
%D    B0 B4 <= B2 B6 <= B3 B7 <=
%D    B4 B5 => B4 B6 |-> B5 B7 |-> .plabel= r \id B6 B7 <=
%D    B0 B2 midpoint B1 B3 midpoint  harrownodes nil 20 nil |->
%D    B0 B2   midpoint B4 B6 midpoint dvarrownodes nil 18 nil <-|
%D    B4 B7   harrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a,c   b1 .tex= a
%D    b2 .tex= b,c   b3 .tex= b
%D    b0 b1 |->
%D    b0 b2 |->  b1 b3 |->
%D    b2 b3 |->
%D    b0 relplace 18 9 \pbsymbol{9}
%D ))
%D enddiagram

% BCC: full diagram (no isos hidden), in $\Sub(\Set)$.

$$\diag{big-bcc-logical-collapsed}$$

\newpage
% --------------------
% «bcc-sums-full-diag»  (to ".bcc-sums-full-diag")
% (s "BCC for dependent sums: full diagram" "bcc-sums-full-diag")
\myslide {BCC for dependent sums: full diagram} {bcc-sums-full-diag}

%D diagram big-bcc
%D 2Dx    100    +35     +35         +70   +35
%D 2D 100 B0 ======================> B1
%D 2D	  -/\                        -
%D 2D	  | \\                       |
%D 2D	  v  \\                      v
%D 2D +30 B2 <\> B2' <-> B2'' <===== B3
%D 2D	   /\  \\                     /\
%D 2D +30   \\   B4 =====================> B5
%D 2D	     \\  -                      \\ -
%D 2D	      \\ |                       \\|
%D 2D	       \\v                        \v
%D 2D +30        B6 <===================== B7
%D 2D
%D 2D +20 b0 <-> b0' <-> b0'' |----> b1
%D 2D	     |->                        |->
%D 2D +60        b2 |--------------------> b3
%D 2D
%D ((
%D    B0 .tex= \s[a,c|d]   B1  .tex= \s[a|c,d]
%D    B2 .tex= \s[a,c|c,d] B2' .tex= \s[a,c|c,d]' B2'' .tex= \s[a,c|c,d]''
%D                         B3  .tex= \s[a|c,d]'
%D    B4 .tex= \s[b,c|d]   B5  .tex= \s[b|c,d]
%D    B6 .tex= \s[b,c|c,d] B7  .tex= \s[b|c,d]
%D    B0 B1 => B0 B2 |-> B0 B2' |-> B0 B2'' |-> B1 B3 |-> .plabel= r {î}
%D    B2 B2' <-> B2' B2'' <-> B2'' B3 <=
%D    B0 B4 <= B2 B6 <= B2' B7 <= B3 B7 <=
%D    B4 B5 => B4 B6 |-> B5 B7 |-> .plabel= r \id B6 B7 <=
%D    B0 B2'' midpoint B1 B3 midpoint  harrownodes nil 20 nil |->
%D    B0 B2   midpoint B4 B6 midpoint dvarrownodes nil 18 nil <-|
%D    B4 B7   harrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a,c b0' .tex= a,c b0'' .tex= a,c   b1 .tex= a
%D    b2 .tex= b,c b0'                            b3 .tex= b
%D    b0 b0' =  b0' b0'' =  b0'' b1 |->
%D    b0 b2 |-> b0' b3 |->  b1 b3 |->
%D    b2 b3 |->
%D ))
%D enddiagram

BCC: full diagram (no isos hidden), in $\Set^\to$.

$\diag{big-bcc}$


\newpage
% --------------------
% «bcc-smaller-diagram»  (to ".bcc-smaller-diagram")
% (s "BCC: smaller diagram" "bcc-smaller-diagram")
\myslide {BCC: smaller diagram} {bcc-smaller-diagram}


%D diagram small-bcc
%D 2Dx    100    +35                 +40   +35
%D 2D 100 B0 ======================> B1
%D 2D	  -/\                        -
%D 2D	  | \\                       |
%D 2D	  v  \\                      v
%D 2D +30 B2 <\\==================== B3
%D 2D	   /\  \\                     /\
%D 2D +20   \\   B4 =====================> B5
%D 2D	     \\  -                      \\ -
%D 2D	      \\ |                       \\|
%D 2D	       \\v                        \v
%D 2D +30        B6 <===================== B7
%D 2D
%D 2D +20 b0 |---------------------> b1
%D 2D	     |->                        |->
%D 2D +50        b2 |--------------------> b3
%D 2D
%D ((
%D    B0 .tex= \s[a,c|d]   B1  .tex= \s[a|c,d]
%D    B2 .tex= \s[a,c|c,d] B3  .tex= \s[a|c,d]
%D    B4 .tex= \s[b,c|d]   B5  .tex= \s[b|c,d]
%D    B6 .tex= \s[b,c|c,d] B7  .tex= \s[b|c,d]
%D    B0 B1 => B0 B2 |-> B1 B3 |-> .plabel= r {î}
%D    B2 B3 <=
%D    B0 B4 <= B2 B6 <= B3 B7 <=
%D    B4 B5 => B4 B6 |-> B5 B7 |-> .plabel= r \id B6 B7 <=
%D    B0 B2 midpoint B1 B3 midpoint  harrownodes nil 20 nil |->
%D    B0 B2 midpoint B4 B6 midpoint dvarrownodes nil 18 nil <-|
%D    B4 B7 harrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a,c    b1 .tex= a
%D    b2 .tex= b,c    b3 .tex= b
%D    b0 b1 |->
%D    b0 b2 |-> b1 b3 |->
%D    b2 b3 |->
%D ))
%D enddiagram

BCC: smaller diagram.

$\diag{small-bcc}$

\newpage
% --------------------
% «bcc-smaller-diagrams»  (to ".bcc-smaller-diagrams")
% (s "BCC: smaller diagrams" "bcc-smaller-diagrams")
\myslide {BCC: smaller diagrams} {bcc-smaller-diagrams}

BCC: smaller diagrams.

%D diagram smaller-bcc
%D 2Dx    100    +30                 +30   +30
%D 2Dx    100    +20                 +25   +20
%D 2D 100 B0 ======================> B1
%D 2D	  -/\                        -
%D 2D	  | \\                       |
%D 2D	  v  \\                      v
%D 2D +20 B2 <\\==================== B3
%D 2D	   /\  \\                     /\
%D 2D +10   \\   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 +30        b2 |--------------------> b3
%D 2D
%D ((
%D    B0 .tex= d   B1  .tex= c,d
%D    B2 .tex= c,d B3  .tex= c,d
%D    B4 .tex= d   B5  .tex= c,d
%D    B6 .tex= c,d B7  .tex= c,d
%D    B0 B1 => B0 B2 |-> B1 B3 |-> .plabel= l {î}
%D    B2 B3 <=
%D    B0 B4 <= B2 B6 <= B3 B7 <=
%D    B4 B5 => B4 B6 |-> B5 B7 |-> .plabel= r \id B6 B7 <=
%D    B0 B2 midpoint B1 B3 midpoint  harrownodes nil 20 nil |->
%D    B0 B2 midpoint B4 B6 midpoint dvarrownodes nil 15 nil <-|
%D    B4 B7 harrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a,c    b1 .tex= a
%D    b2 .tex= b,c    b3 .tex= b
%D    b0 b1 |->
%D    b0 b2 |-> b1 b3 |->
%D    b2 b3 |->
%D    b0 relplace 12 7 \pbsymbol{7}
%D ))
%D enddiagram

%D diagram smaller-prod-bcc
%D 2Dx    100    +30                 +30   +30
%D 2Dx    100    +20                 +25   +20
%D 2D 100 B0 <====================== B1
%D 2D	  -/\                        -
%D 2D	  | \\                       |
%D 2D	  v  \\                      v
%D 2D +20 B2 =\\===================> B3
%D 2D	   /\  \\                     /\
%D 2D +10   \\   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 +30        b2 |--------------------> b3
%D 2D
%D ((
%D    B0 .tex= c|->d B1  .tex= c|->d
%D    B2 .tex= d     B3  .tex= c|->d
%D    B4 .tex= c|->d B5  .tex= c|->d
%D    B6 .tex= d   B7    .tex= c|->d
%D    B0 B1 <= B0 B2 |-> B1 B3 |-> .plabel= l {î}
%D    B2 B3 =>
%D    B0 B4 <= B2 B6 <= B1 B5 <= #   B3 B7 <=
%D    B4 B5 <= B4 B6 |-> B5 B7 |-> .plabel= r \id B6 B7 =>
%D    B0 B2 midpoint B1 B3 midpoint  harrownodes nil 20 nil |->
%D    B0 B2 midpoint B4 B6 midpoint dvarrownodes nil 15 nil <-|
%D    B4 B7 harrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a,c    b1 .tex= a
%D    b2 .tex= b,c    b3 .tex= b
%D    b0 b1 |->
%D    b0 b2 |-> b1 b3 |->
%D    b2 b3 |->
%D    b0 relplace 12 7 \pbsymbol{7}
%D ))
%D enddiagram

%:           b,c|-D
%:           -------
%:           b|-Æc.D
%:           --------
%:            b;p|-p       
%:         ----------------
%:  a|-b   b,c;d|-\ang{c,d}
%:  -----------------------
%:     a,c;d|-\ang{c,d}    
%:  -----------------------
%:  a;p|-\ang{c,d}[c,d:=p] 
%:                         
%:     ^bcc-sum-1
%:  
$$\cdiag{smaller-bcc} \qquad
 % \begin{matrix}
 \cded{bcc-sum-1}
 % \end{matrix}
$$

%:           b,c|-D    
%:           -------
%:           b|-åc.D
%:           --------
%:            b;f|-f   
%:         ---------   
%:  a|-b   b,c;f|-fc   
%:  ----------------   
%:     a,c;f|-fc       
%:    ----------       
%:    a;f|-ðc.fc       
%:                     
%:    ^bcc-prod-1 
%:  
$$\cdiag{smaller-prod-bcc} \qquad
 \begin{matrix}
 \ded{bcc-prod-1}
 \end{matrix}
$$



\newpage
% --------------------
% «bcc-trees»  (to ".bcc-trees")
% (s "BCC: trees" "bcc-trees")
\myslide {BCC: trees} {bcc-trees}


%D diagram smaller-bcc-eq
%D 2Dx    100    +30                 +30   +30
%D 2D 100 B0 ======================> B1
%D 2D	  -/\                        -
%D 2D	  | \\                       |
%D 2D	  v  \\                      v
%D 2D +20 B2 <\\==================== B3
%D 2D	   /\  \\                     /\
%D 2D +10   \\   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 +30        b2 |--------------------> b3
%D 2D
%D ((
%D    B0 .tex= d         B1  .tex= (c{=}c'),d
%D    B2 .tex= (c{=}c),d B3  .tex= (c{=}c'),d
%D    B4 .tex= d         B5  .tex= (c{=}c'),d
%D    B6 .tex= (c{=}c),d B7  .tex= (c{=}c'),d
%D    B0 B1 => B0 B2 |-> B1 B3 |-> .plabel= l {î}
%D    B2 B3 <=
%D    B0 B4 <= B2 B6 <= B3 B7 <=
%D    B4 B5 => B4 B6 |-> B5 B7 |-> .plabel= r \id B6 B7 <=
%D    B0 B2 midpoint B1 B3 midpoint  harrownodes nil 20 nil |->
%D    B0 B2 midpoint B4 B6 midpoint dvarrownodes nil 15 nil <-|
%D    B4 B7 harrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a,c    b1 .tex= a,c,c'
%D    b2 .tex= b,c    b3 .tex= b,c,c'
%D    b0 b1 |->
%D    b0 b2 |-> b1 b3 |->
%D    b2 b3 |->
%D    b0 relplace 12 7 \pbsymbol{7}
%D ))
%D enddiagram

%:           b,c|-D
%:           -------
%:           b,c,c'|-Æ(c{=}c').D
%:           ----------------------
%:             b,c,c';((c{=}c'),d)|-((c{=}c').d)       
%:             ---------------------------------
%:  a,c|-b,c   b,c;d|-\ang{(c{=}c),d}
%:  ---------------------------------
%:     a,c;d|-\ang{(c{=}c),d}
%:    -----------------------
%:    a,c;((c{=}c'),d)|-\ang{(c{=}c'),d}
%:                         
%:     ^bcc-eq-1-semi     
%:  
$$\cdiag{smaller-bcc-eq} \qquad
 \begin{matrix}
 \ded{bcc-eq-1-semi}
 \end{matrix}
$$



\newpage
% --------------------
% «first-preservations»  (to ".first-preservations")
% (s "First preservations" "first-preservations")
\myslide {First preservations} {first-preservations}

%D diagram cob-preserves-T-and-AND
%D 2Dx    100     +30    +30 +10 +30      +40
%D 2D 100                PP0 <=========== PP1
%D 2D	                  ^  ^             ^
%D 2D	                  |   \      <-|   |
%D 2D	                  -    -           -
%D 2D +30 PT0 <== PT1    PP2 <-| PP3 <=== PP4
%D 2D	   -              -    -           -
%D 2D	   |              |   /      <-|   |
%D 2D	   v              v  v             v
%D 2D +30 PT2            PP5 <=========== PP6
%D 2D
%D 2D +20 pta |-> ptb        ppa |------> ppb
%D 2D
%D (( PT0 .tex= \s[a|§]  PT1 .tex= \s[b|§]
%D    PT2 .tex= \s[a|§]'
%D    pta .tex= a        ptb .tex= b
%D    PT0 PT1 <= PT0 PT2 |-> .plabel= r {î}
%D    pta ptb |->
%D ))
%D (( PP0 .tex= \s[a|P]                          PP1 .tex= \s[b|P]
%D    PP2 .tex= \s[a|P&Q]'  PP3 .tex= \s[a|P&Q]  PP4 .tex= \s[b|P&Q]
%D    PP5 .tex= \s[a|Q]                          PP6 .tex= \s[b|Q]
%D                 ppa .tex= a                   ppb .tex= b
%D    PP0 PP1 <=
%D    PP0 PP2 <-| .plabel= r {\pi} PP0 PP3 <-|
%D    PP1 PP4 <-| .plabel= r {\pi}
%D    PP0 PP3 midpoint PP1 PP4 midpoint harrownodes nil 20 nil <-|
%D    PP2 PP3 <-| .plabel= a {î}    PP3 PP4 <=
%D    PP2 PP5 |-> .plabel= r {\pi'} PP3 PP5 |->
%D    PP4 PP6 |-> .plabel= r {\pi'}
%D    PP3 PP5 midpoint PP4 PP6 midpoint harrownodes nil 20 nil <-|
%D    PP5 PP6 <=
%D    ppa ppb |->
%D ))
%D enddiagram

%D diagram cob-preserves-exp
%D 2Dx    100 +20 +20       +40 +20 +20
%D 2D 100 E0 <============= E1
%D 2D	   v /\             v  /\
%D 2D +30 E2 <\\=========== E3  \\
%D 2D	    \\ \\             \\ \\
%D 2D +20    \\   E4 <============= E5
%D 2D	      \/  -             \/  v
%D 2D +30         E6                E7
%D 2D
%D 2D +20     ea |------------> eb
%D 2D
%D (( E0 .tex= \s[a|(Q¶R)&Q] E1 .tex= \s[b|(Q¶R)&Q]
%D    E2 .tex= \s[a|R]       E3 .tex= \s[b|R]
%D    E4 .tex= \s[a|Q¶R]     E5 .tex= \s[b|Q¶R]
%D    E6 .tex= \s[a|Q¶R]'    E7 .tex= \s[b|Q¶R]
%D    ea .tex= a             eb .tex= b
%D    E0 E1 <= E0 E2 |-> E1 E3 |-> E2 E3 <=
%D    E0 E4 <= E2 E6 =>  E1 E5 <=  E3 E7 =>
%D    E4 E5 <= E4 E6 |-> .plabel= r {î} E5 E7 |-> .plabel= r \id
%D    E0 E3 harrownodes nil 20 nil <-|
%D    E0 E2 midpoint E4 E6 midpoint dvarrownodes nil 16 nil |->
%D    E1 E3 midpoint E5 E7 midpoint dvarrownodes nil 16 nil <-|
%D    ea eb |->
%D ))
%D enddiagram

Change-of-base preserves terminals and binary products:

$\diag{cob-preserves-T-and-AND}$

\medskip

Change-of-base preserves exponentials:

$\diag{cob-preserves-exp}$

\medskip

In all the diagrams above the natural morphisms marked

`$î$' are required to be isos.

\medskip

Note that in the diagram for preservation of exponentials

the object at the upper left has two constructions; in fact

it is two objects, and we are hiding the iso between them.

\newpage
% --------------------
% «first-preservations-2»  (to ".first-preservations-2")
% (s "First preservations (2)" "first-preservations-2")
\myslide {First preservations (2)} {first-preservations-2}

A category with the structure above is a {\bf pre-hyperdoctrine}.

A {\bf hyperdoctrine} is a pre-hyperdoctrine that obeys certain

extra equations, like this one:

\medskip

In a pre-hyperdoctrine given $a \mton{f} b$ and two propositions $P(b)$

and $Q(b)$ over the space of `$b$'s we have two different constructions

for $P(f(a)) \& Q(f(a))$ over the space of `$a$'s, and a natural

morphism from one construction to the other one:

\medskip

$\dncdisplay[b|P\&Q]  := (P(b) \& Q(b))[b:=f(a)]$

$\dncdisplay[b|P\&Q]' := P(b)[b:=f(a)] \, \& \, Q(b)[b:=f(a)]$

\medskip

%D diagram cob-preserves-AND
%D 2Dx    100 +10 +30      +40
%D 2D 100 PP0 <=========== PP1
%D 2D      ^  ^             ^
%D 2D      |   \      <-|   |
%D 2D      -    -           -
%D 2D +30 PP2 <-| PP3 <=== PP4
%D 2D      -    -           -
%D 2D      |   /      <-|   |
%D 2D      v  v             v
%D 2D +30 PP5 <=========== PP6
%D 2D
%D 2D +20     ppa |------> ppb
%D 2D
%D (( PP0 .tex= \s[a|P]                          PP1 .tex= \s[b|P]
%D    PP2 .tex= \s[a|P&Q]'  PP3 .tex= \s[a|P&Q]  PP4 .tex= \s[b|P&Q]
%D    PP5 .tex= \s[a|Q]                          PP6 .tex= \s[b|Q]
%D                 ppa .tex= a                   ppb .tex= b
%D    PP0 PP1 <=
%D    PP0 PP2 <-| .plabel= r {\pi} PP0 PP3 <-| .plabel= r {f^*\pi}
%D    PP1 PP4 <-| .plabel= r {\pi}
%D    PP0 PP3 midpoint PP1 PP4 midpoint harrownodes nil 20 nil <-|
%D    PP2 PP3 <-| .plabel= a {î}    PP3 PP4 <=
%D    PP2 PP5 |-> .plabel= r {\pi'} PP3 PP5 |->  .plabel= r {f^*\pi'}
%D    PP4 PP6 |-> .plabel= r {\pi'}
%D    PP3 PP5 midpoint PP4 PP6 midpoint harrownodes nil 20 nil <-|
%D    PP5 PP6 <=
%D    ppa ppb |-> .plabel= a {f}
%D ))
%D enddiagram

$\diag{cob-preserves-AND}$

\medskip

we want these two constructions to be equivalent, so in the

definition of hyperdoctrine we include a condition that says

that the morphism `$î$' is an iso, i.e., that it has an inverse.



















%

\end{document}

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