% (find-angg "LATEX/2008hyp.tex")
% nontranslatables: «¶»ö
%   \catcode`¶=13 \def¶{\limp}

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

% 2020jan27:
% (find-dednat6 "demo-preproc.tex")


% «.haskell»			(to "haskell")
% «.type-theory-origins»	(to "type-theory-origins")
% «.eilenberg-maclane-1945»	(to "eilenberg-maclane-1945")
% «.type-checking-and-related»	(to "type-checking-and-related")
% «.weaker-systems»		(to "weaker-systems")

% «.brownie-points»		(to "brownie-points")
% «.subobjs-and-cob»		(to "subobjs-and-cob")
% «.hyp-definition»		(to "hyp-definition")
% «.quants-adjs-example»	(to "quants-adjs-example")
% «.preservations-overview»	(to "preservations-overview")
% «.pres-of-true-and-and»	(to "pres-of-true-and-and")
% «.pres-of-false-and-or»	(to "pres-of-false-and-or")
% «.pres-of-imp»		(to "pres-of-imp")
% «.bcc-for-forall»		(to "bcc-for-forall")
% «.bcc-for-exists»		(to "bcc-for-exists")
% «.bcc-for-equality»		(to "bcc-for-equality")
% «.frob-for-exists»		(to "frob-for-exists")
% «.frob-for-equality»		(to "frob-for-equality")
% «.frob-for-ex-eq»		(to "frob-for-ex-eq")
% «.frob-and-pres-imp»		(to "frob-and-pres-imp")
% «.bcc-ex-iff-bcc-fa»		(to "bcc-ex-iff-bcc-fa")
% «.constrs-to-proofs-and-back»	(to "constrs-to-proofs-and-back")
% «.adj-functors-as-seq-rules»	(to "adj-functors-as-seq-rules")
% «.adj-functors-as-seq-rules-2»  (to "adj-functors-as-seq-rules-2")
% «.adj-maps-as-seq-rules»	(to "adj-maps-as-seq-rules")
% «.adj-maps-as-seq-rules-2»	(to "adj-maps-as-seq-rules-2")
% «.adj-functors-as-ND-proofs»	(to "adj-functors-as-ND-proofs")
% «.adj-functors-as-ND-proofs-2»  (to "adj-functors-as-ND-proofs-2")
% «.adj-maps-as-ND-proofs»	(to "adj-maps-as-ND-proofs")
% «.adj-maps-as-ND-proofs-2»	(to "adj-maps-as-ND-proofs-2")
% «.adj-maps-as-ND-proofs-3»	(to "adj-maps-as-ND-proofs-3")
% «.frob-maps-as-ND-proofs»	(to "frob-maps-as-ND-proofs")
% «.frob-for-equality-2»	(to "frob-for-equality-2")
% «.dep-eq-from-simple-eq»	(to "dep-eq-from-simple-eq")
% «.eq-is-transitive»		(to "eq-is-transitive")
% «.hyp-subst-quant-refl»	(to "hyp-subst-quant-refl")
% «.hyp-sym-trans»		(to "hyp-sym-trans")
% «.weak-strong-exelim»		(to "weak-strong-exelim")
% «.rules-nd-sc»		(to "rules-nd-sc")
% «.rules-categorically»	(to "rules-categorically")


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

%
% (eedn4-51-bounded)
% (find-2005oct20seminar "" "PLC-diags-sqth1")
% (find-angg "LATEX/2005oct20-seminar.tex" "PLC-diags-sqth1")

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 {Haskell} {2}
\tocline {Type theory: origins} {3}
\tocline {Eilenbeg/MacLane 1945} {4}
\tocline {Type-checking and related problems} {5}
\tocline {Weaker systems} {6}
\tocline {Slides vs. brownie points} {7}
\tocline {Hyperdoctrines: subobjects and change-of-base} {8}
\tocline {Hyperdoctrine: definition} {9}
\tocline {Quantifiers as adjoints: an example} {10}
\tocline {Preservations by change-of-base: overview} {11}
\tocline {Preservation of `true' and `and'} {12}
\tocline {Preservation of `false' and `or'} {13}
\tocline {Preservation of `implies'} {14}
\tocline {BCC for `forall'} {15}
\tocline {BCC for `exists'} {16}
\tocline {BCC for equality} {17}
\tocline {Frobenius for `exists'} {18}
\tocline {Frobenius for equality} {19}
\tocline {Frobenius for exists-equal} {20}
\tocline {Frobenius is equivalent to preservation of `implies'} {21}
\tocline {BCC for `exists' holds iff BCC for `forall' holds} {22}
\tocline {From ``constructions'' to ``intuitionistic proofs'', and back} {23}
\tocline {The adjunction functors as sequent rules} {24}
\tocline {The adjunction functors as sequent rules (2)} {25}
\tocline {The adjunction maps as sequent rules} {26}
\tocline {The adjunction maps as sequent rules (2)} {27}
\tocline {The adjunction functors as ND proofs} {28}
\tocline {The adjunction functors as ND proofs (2)} {29}
\tocline {The adjunction maps as ND proofs} {30}
\tocline {The adjunction maps as ND proofs (2)} {31}
\tocline {The adjunction maps as ND proofs (3)} {32}
\tocline {The Frobenius maps as ND proofs} {33}
\tocline {Frobenius for equality (2)} {34}
\tocline {Dependent equality from simple equality} {35}
\tocline {Transitivity of equality} {36}
\tocline {Hyperdoctrines: substitution, quantifiers, reflexivity} {37}
\tocline {Hyperdoctrines: symmetry, transitivity} {38}
\tocline {Weak and strong exists-elim} {39}
\tocline {Rules in ND and sequent calculus} {40}
\tocline {Rules, categorically} {41}

%:&\&
%:\&\&
%:'*^{\prime*}
%:b=b'b{=}b'
%:b=b''b{=}b''
%:b'=b''b'{=}b''
%:a=fba{=}fb
%:b=fab{=}fa
%:×{×}
%:\s[\dncdisplay[

%:`\ign 
\def\ign#1{}

\def\Eq{Ð{Eq}}
\def\ExEq{Î{=}}
\def\co{\mathrm{co}}
\def\dncdisplay[#1|#2]{\begin{pmatrix} #2 \\ #1 \end{pmatrix}}

\def\lcurlybar#1{\left\{\mskip#1mu\middle|}
\def\rcurlybar#1{\middle|\mskip#1mu\right\}}
\def\scof#1#2{\lcurlybar{#1}#2\rcurlybar{#1}}
\def\scst#1#2#3{\lcurlybar{#1}#2\middle\|#3\rcurlybar{#1}}
\def\Sst#1#2{\scst{-4}{#1}{#2}}

\def\footwo#1#2{%
  \begin{array}{ccc}
  #1 && #2 \\
  \end{array}
  }
\def\footwov#1#2{%
  \begin{array}{ccc}
  #1 \\ \\ #2 \\
  \end{array}
  }
\def\foothreev#1#2#3{%
  \begin{array}{ccc}
  #1 \\ \\ #2 \\ \\ #3 \\
  \end{array}
  }
\def\foofour#1#2#3#4{%
  \begin{array}{ccc}
  #1 & #2 \\ \\
  #3 & #4 \\
  \end{array}
  }
\def\fooFour#1#2#3#4{%
  \begin{array}{ccc}
  #1 && #2 \\ \\
  #3 && #4 \\
  \end{array}
  }


\def\lcurlybar#1{\left\{\mskip#1mu\middle|}
\def\rcurlybar#1{\middle|\mskip#1mu\right\}}
\def\cbsof#1{\lcurlybar{-4}#1\rcurlybar{-4}}
\def\cbsst#1#2{\lcurlybar{-4}#1\,\middle|\,#2\rcurlybar{-4}}
\def\cbsubobj#1#2{\lcurlybar{-4}#1\,\middle\|\,#2\rcurlybar{-4}}


\newpage
% --------------------
% «haskell»  (to ".haskell")
% (s "Haskell" "haskell")
\myslide {Haskell} {haskell}

{\myttchars
% \footnotesize
\begin{verbatim}
-- (find-libhugsfile "libraries/Hugs/Prelude.hs")

foldl            :: (a -> b -> a) -> a -> [b] -> a
foldl f z []      = z
foldl f z (x:xs)  = foldl f (f z x) xs

foldl1           :: (a -> a -> a) -> [a] -> a
foldl1 f (x:xs)   = foldl f x xs

-- foldl1 max [1, 3, 2, 4]
---> foldl max 1 [3, 2, 4]
---> foldl max (max 1 3) [2, 4]
---> foldl max (max (max 1 3) 2) [4]
---> foldl max (max (max (max 1 3) 2) 4) []
--->           (max (max (max 1 3) 2) 4)
--->           (max (max 3         2) 4)
--->           (max 3                 4)
--->           4
\end{verbatim}
}


\newpage
% --------------------
% «type-theory-origins»  (to ".type-theory-origins")
% (s "Type theory: origins" "type-theory-origins")
\myslide {Type theory: origins} {type-theory-origins}

% (find-automathpage (+ 21 4) "In order to prevent the paradoxes")
(From the introduction to {\sl 25 Years of Automath}:)

\begin{quote}

In order to prevent the paradoxes, Whitehead and Russell analysed the
{\sl vicious circles} present in all the known paradoxes. They came to
the conviction that a hierarchy was necessary for a sound development
of arithmetic and they proposed a type system: the {\sl simple type
theory}. It turned out that a refinement was necessary, which they
called the {\sl ramified theory of types}. This worked as they
desired, albeit they needed an extra axiom, in order to ``soften'' the
strictness of the typing hierarchy. Only with this {\sl axiom of
reducibility} they were able to incorporate full arithmetic, in
particular the real numbers, based on Dedekind cuts.

This idea of using types emerged quite naturally, once the vicious
circles had been detected. In fact, one may say that types existed
since early mathematics was developed: categories like `natural
number' and `real number' in calculus, or `point' and `line' in
geometry, grouped elements together in clusters with a common meaning
or structure. In this sense, types were meant to emphasize the {\sl
similarities} between given entities. But at the same time, types can
be of use in establishing {\sl differences} between entities. The
latter aspects turned out to be of great importance in combatting
against the paradoxes.

\end{quote}


\newpage
% --------------------
% «eilenberg-maclane-1945»  (to ".eilenberg-maclane-1945")
% (s "Eilenbeg/MacLane 1945" "eilenberg-maclane-1945")
\myslide {Eilenbeg/MacLane 1945} {eilenberg-maclane-1945}

From Ralf Krömer's {\sl Tool and Object - A History and
Philosophy of Category Theory} (p.65) on the reception of the
first paper on Category Theory (Eilenberg/MacLane: ``General
Theory of Natural Equivalences'', 1945):

% (find-em45page (+ -229 231) "Contents")
% (find-kromerpage (+ 34  65) "2.3.2. The reception of the 1945 paper")
% (find-kromertext           "\n2.3.2 The reception of the 1945 paper")

\begin{quote}

  The readyness to write down and submit for publication a work almost
  completely concerned with conceptual clarification (and with the
  solution of some internal problems raised by the new concepts
  themselves) is a remarkable expression of courage. While (as Corry
  learned from Eilenberg, see [Corry 1996, 366 n.27]) Steenrod once
  stated concerning [1945] that ``no paper had ever influenced his
  thinking more'', P.A.\ Smith said that ``he had never read a more
  trivial paper in his life''. [Mac Lane 1988a, 334] writes, without
  mentioning a name: ``One of our good friends (an admirer of
  Eilenberg) read the paper and told us privately that he thought that
  the paper was without any content''.

\end{quote}

% (find-kromertext "The diagrams incorporate a large amount of information")

Krömer, p.82, quoting Eilenberg/Steenrod 1952:

\begin{quote}

  The reader will observe the presence of numerous diagrams in the
  text. [...] Two paths connecting the same pair of vertices usually
  give the same homomorphism. This is called a {\sl commutativity
    relation}. The combinatorially minded individual can regard it as
  a homology relation due to the presence of 2-dimensional cells
  adjoined to the graph. [...]

  The diagrams incorporate a large amount of information. [...] In the
  case of many theorems, the setting up of the correct diagram is the
  major part of the proof [1952, xi].

\end{quote}


\newpage
% --------------------
% «type-checking-and-related»  (to ".type-checking-and-related")
% (s "Type-checking and related problems" "type-checking-and-related")
\myslide {Type-checking and related problems} {type-checking-and-related}

% (find-angg ".emacs.papers" "urzyczyn")
% (find-urzypage (+ 12  89) "6. Type-checking and related problems")
% (find-urzytext "The type checking problem is")

From Urzyczyn/Sorensen's ``Lectures on the Curry-Howard Isomorphism''
(online draft, p.89):

\begin{quote}

  1. The type checking problem is to decide whether $\GG \vdash M:$
  holds, for a given context $\GG$, a term $M$ and a type $$.

  2. The type reconstruction problem, also called typability problem,
  is to decide, for a given term $M$, whether there exist a context
  $\GG$ and a type $$, such that $\GG \vdash M:$ holds, i.e.,
  whether $M$ is typable.

  3. The type inhabitation problem, also called type emptiness
  problem, is to decide, for a given type $$, whether there exists a
  closed term $M$, such that $\GG \vdash M:$ holds. (Then we say that
  $$ is non-empty and has an inhabitant $M$).

\end{quote}



\newpage
% --------------------
% «weaker-systems»  (to ".weaker-systems")
% (s "Weaker systems" "weaker-systems")
\myslide {Weaker systems} {weaker-systems}

Why do we want weaker systems?

Things that can be constructed in them may have nicer properties:

  Every reduction sequence terminates.

  All terms of type $A×B \to B×A$ are the flip function

  Each proof in Natural Deduction corresponds to a lambda-term

  Every term is typed

    Type-checking can be used to detect errors

\msk

Weaker systems should have more models:

  If a judgment $J$

  is true in a stronger system $S$

  but false in a weaker system $W$

  then there should be a model of $W$

  in which $J$ is not collapsed to ``true''.

\msk

How do we get intuition about weaker systems?

  Stronger system: $S$, the universe of ZFC

  Weaker system: $W$, where $¬¬P = P$ is not ``true''

  All constructions in $W$ can be carried out in $S$.



% \end{document}



\newpage
% --------------------
% «brownie-points»  (to ".brownie-points")
% (s "Slides vs. brownie points" "brownie-points")
\myslide {Slides vs. brownie points} {brownie-points}

% This technical report has an unusual format -- slides --
% an unsual aims. Let me explain. First of all, I am in a kind of
% a professional limbo: from 2005 to 2007 I worked as a programmer,
% but at the end of that I was on the verge of killing people and
% then blowing myself up -- because ``someone had to do that'' and
% because ``I had absolutely nothing to lose'' -- but then I
% applied to an academic position, went through all the admission
% process, and was selected for the job; I became an {\sl almost-
% professor} in a federal university in Brazil...
% ...then it turned out that one of the other candidates --
% who was applying to a position {\sl in another department} (!) --
% had found some slight legal inconsistencies in the official public
% anouncement of these job openings and of the rules of the selection
% process, and had denounced that, and demanded certain changes in
% the rules...
% 
% To make a long story short: there are 12 almost-professors,
% including me, waiting since june for the legal mumbo-jumbo to be
% completed so that we can be hired -- I am writing this in november.
% The process is taking longer than anyone expected, and
% as {\sl I have not gotten rid of my anger yet} -- far from that --
% I decided that I would not follow the ``path of the articles'',
% that would give me more CV-karma and more brownie points.

I have not been hired by UFF yet.

This is going to happen ``at any moment'' -- since june.

http://angg.twu.net/concurso.html

I am (choose one):

 almost a university professor

 currently unemployed

 in unpayed holidays

 on strike

\msk

Articles would get me more brownie points from funding agencies,

but right now seminars and slides are more useful --

\msk

I need to discuss with local people, who are:

 algebraic geometers,

 (modal) logicians,

 computer scientists

 grad students who just had a CT course (that was ``too algebraic'')




\newpage
% --------------------
% «subobjs-and-cob»  (to ".subobjs-and-cob")
% (s "Hyperdoctrines: subobjects and change-of-base" "subobjs-and-cob")
\myslide {Hyperdoctrines: subobjects and change-of-base} {subobjs-and-cob}

Our archetypal hyperdoctrine is this:

$\begin{array}{rrcl}
 \Cod: & \Sub(\Set) & \to & \Set \\
       & (A' \monicto A) & \mto & A \\
 \end{array}
$ 

\msk

A linguistic trick:

everything will simplify A LOT if we pretend

that all subobject are subsets.

Another shorthand: `$P$' instead of `$P(a)$'.

$\begin{array}{rcl}
       (\cbsst{a}{P} \monicto A) & \mto & A \\
       (\cbsst{a}{P} \monicto \cbsof{a}) & \mto & \cbsof{a} \\
       \cbsubobj{a}{P} & \mto & \cbsof{a} \\
       (a\|P) & \funto & a \\
 \end{array}
$ 

\msk

We will downcase the projection functor, $\Cod$, to $(a\|P) \funto a$.

We will often draw it vertically and omit the `$a\|$' and the `$\funto$':

%D diagram cod-omits
%D 2Dx     100  +30  +30  +29
%D 2D  100 A0   A1   A2   A3
%D 2D
%D 2D  +20 B0   B1   B2   B3
%D 2D
%D (( A0 .tex= \cbsubobj{a}{P} B0 .tex= A |->
%D    A1 .tex= a\|P B1 .tex= a =>
%D    A2 .tex= P    B2 .tex= a =>
%D    A3 .tex= P place  B3 .tex= a place
%D ))
%D enddiagram
%D
$$\diag{cod-omits}$$

\msk

The change-of-base functors in $\Cod: \Sub(\Set) \to \Set$

are induced by pullbacks:

%D diagram cob-as-PB-in-sub-set
%D 2Dx     100   +45   +30   +40
%D 2D  100 A0 -> A1    B0 -> B1
%D 2D      v _|  v     v _|  v 
%D 2D  +15 |     |     B02   B13
%D 2D      v     v     v     v 
%D 2D  +15 A2 -> A3    B2 -> B3
%D 2D
%D 2D  +15 A4 -> A5    B4 -> B5
%D 2D
%D (( A0 .tex= \cbsst{a}{P(f(a))}  A1 .tex= \cbsst{a}{P(b)}
%D    A2 .tex= A A3 .tex= B
%D    A4 .tex= A A5 .tex= B
%D    A0 A1  -> .plabel= a f'
%D    A0 A2 >-> .plabel= l f^*P
%D    A1 A3 >-> .plabel= r P
%D    A2 A3  -> .plabel= a f
%D    A0 relplace 7 7 \pbsymbol{7}
%D    A0 A3 harrownodes nil 20 nil <-| .plabel= a f^*
%D    A4 A5 -> .plabel= a f
%D ))
%D (( B02 .tex= f^*P  B13 .tex= P
%D    B4 .tex= A      B5 .tex= B
%D    B02 B13 -> sl^ .plabel= a \ov{f}P\equiv(f',f)
%D    B02 B13 <-| sl_ .plabel= b f^*
%D    B02 B4 |-> .plabel= l \Cod
%D    B13 B5 |-> .plabel= r \Cod
%D    B4  B5 -> .plabel= a f
%D ))
%D enddiagram
%D
$$\diag{cob-as-PB-in-sub-set}$$

\msk

The map $\ov{f}P: \cbsubobj{a}{P(f(a))} \to \cbsubobj{b}{P(b)}$

corresponds to a pullback square in $\Sub(\Set)$.

It is a {\sl cartesian map} in the fibration $\Cod: \Sub(\Set) \to \Set$.

(We will see the abstract definition of cartesian maps later).

We will indicate cartesian maps with a `$ñ$'.

We will downcase the change-of-base diagram as this:

%D diagram cob-in-set-dnc
%D 2Dx     100      +35   +25     +30
%D 2D  100 Pfa <=== Pb    B0 <=== B1
%D 2D
%D 2D  +25 a |----> b     B2 |--> B3
%D 2D
%D (( Pfa Pb a b
%D    @ 0 @ 1 |-> sl^ .plabel= a ñ @ 0 @ 1 <= sl_
%D    a b |-> .plabel= a f
%D ))
%D (( B0 .tex= P B1 .tex= P
%D    B2 .tex= a B3 .tex= b
%D    @ 0 @ 1 |-> sl^ .plabel= a ñ @ 0 @ 1 <= sl_
%D    @ 2 @ 3 |->
%D ))
%D enddiagram
%D
$$\diag{cob-in-set-dnc}$$


\newpage
% --------------------
% «hyp-definition»  (to ".hyp-definition")
% (s "Hyperdoctrine: definition" "hyp-definition")
\myslide {Hyperdoctrine: definition} {hyp-definition}

Formally, a hyperdoctrine is a fibration for which:

(i) the base category is cartesian closed,

(ii) each fiber is bicartesian closed,

(iii) the change-of-base functors preserve the BiCCC structure modulo iso,

(iv) each change-of-base functor has a left adjoint

\quad obeying Beck-Chevalley and Frobenius,

(v) each change-of-base functor has a right adjoint

\quad obeying Beck-Chevalley and Frobenius.

\msk

The base category is (bi)cartesian closed:

%D diagram CCC
%D 2Dx    100     +25     +25  +15  +20      +25
%D 2D 100     --| p0 |-	       t0   a0 <==== a1
%D 2D	     /    -    \       -     -        -
%D 2D	    /     |	\      |     |  <-->  |
%D 2D	   v      v	 v     v     v	      v
%D 2D +25 p1 <--| p2 |--> p3   t1   a2 ====> a3
%D 2D
%D 2D +15 c0 |--> c1 <--| c2   i0
%D 2D      /      -	 \     -
%D 2D       \     |	/      |
%D 2D        \    v    /       v
%D 2D +25     --> c3 <-	       i1
%D 2D
%D ((            p0 .tex=  a
%D    p1 .tex= b p2 .tex= b,c p3 .tex= c
%D    @ 0 @ 1 |-> @ 0 @ 2 |-> @ 0 @ 3 |->
%D    @ 1 @ 2 <-| @ 2 @ 3 |->
%D ))
%D (( c0 .tex= a c1 .tex= a÷b c2 .tex= b
%D               c3 .tex=  c
%D    @ 0 @ 1 |-> @ 1 @ 2 <-|
%D    @ 0 @ 3 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D ))
%D (( t0 .tex= a t1 .tex= *
%D    @ 0 @ 1 |->
%D ))
%D (( i0 .tex= ® i1 .tex= a
%D    @ 0 @ 1 |->
%D ))
%D (( a0 .tex= a,b a1 .tex= a
%D    a2 .tex=  c  a3 .tex= b|->c
%D    @ 0 @ 1 <= @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D    @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram

$$\diag{CCC}$$

\msk

Each fiber is bicartesian closed:

%D diagram HA
%D 2Dx    100     +25     +25  +15  +20      +25
%D 2D 100     --| p0 |-	       t0   a0 <==== a1
%D 2D	     /    -    \       -     -        -
%D 2D	    /     |	\      |     |  <-->  |
%D 2D	   v      v	 v     v     v	      v
%D 2D +25 p1 <--| p2 |--> p3   t1   a2 ====> a3
%D 2D
%D 2D +15 c0 |--> c1 <--| c2   i0
%D 2D      /      -	 \     -
%D 2D       \     |	/      |
%D 2D        \    v    /       v
%D 2D +25     --> c3 <-	       i1
%D 2D
%D ((            p0 .tex=  P
%D    p1 .tex= Q p2 .tex= Q&R p3 .tex= R
%D    @ 0 @ 1 |-> @ 0 @ 2 |-> @ 0 @ 3 |->
%D    @ 1 @ 2 <-| @ 2 @ 3 |->
%D ))
%D (( c0 .tex= P c1 .tex= PQ c2 .tex= Q
%D               c3 .tex=  R
%D    @ 0 @ 1 |-> @ 1 @ 2 <-|
%D    @ 0 @ 3 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D ))
%D (( t0 .tex= P t1 .tex= {§}
%D    @ 0 @ 1 |->
%D ))
%D (( i0 .tex= ® i1 .tex= P
%D    @ 0 @ 1 |->
%D ))
%D (( a0 .tex= P&Q a1 .tex= P
%D    a2 .tex=  R  a3 .tex= Q¶R
%D    @ 0 @ 1 <= @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D    @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram

$$\diag{HA}$$

\msk

Left adjoints ($Î/\&{=}/Î{=}$) and right adjoints ($ý/¶{=}/ý{=}$)

for change-of-base functors:

%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.b=fa&Pb
%D    C2 .tex= Qfa   C3 .tex= Qb
%D    C4 .tex= Ra    C5 .tex= ýa.b=fa¶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}



\newpage
% --------------------
% «quants-adjs-example»  (to ".quants-adjs-example")
% (s "Quantifiers as adjoints: an example" "quants-adjs-example")
\myslide {Quantifiers as adjoints: an example} {quants-adjs-example}

%D diagram quants-set
%D 2Dx     100       +55    +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	    |   <->   |      |   <->   |
%D 2D	    v         v      v         v
%D 2D  +30 A4 =====> A5     B4 =====> B5
%D 2D
%D 2D  +15 A6 |----> A7     B6 |----> B7
%D 2D
%D (( A0 .tex= \Sst{a,b}{P(a,b)} A1 .tex= \Sst{a}{Îb.P(a,b)}
%D    A2 .tex= \Sst{a,b}{Q(a)}   A3 .tex= \Sst{a}{Q(a)}
%D    A4 .tex= \Sst{a,b}{R(a,b)} A5 .tex= \Sst{a}{ýb.R(a,b)}
%D    A6 .tex= A×B               A7 .tex= A
%D    @ 0 @ 1 |->
%D    @ 0 @ 2 -> @ 1 @ 3 ->
%D    @ 2 @ 3 <-|
%D    @ 2 @ 4 -> @ 3 @ 5 ->
%D    @ 4 @ 5 |->
%D    @ 0 @ 3 harrownodes nil 20 nil <->
%D    @ 2 @ 5 harrownodes nil 20 nil <->
%D    @ 6 @ 7 ->
%D ))
%D (( B0 .tex= \sm{100\,000\\110\,000} B1 .tex= \sm{110\,000}
%D    B2 .tex= \sm{111\,000\\111\,000} B3 .tex= \sm{111\,000}
%D    B4 .tex= \sm{111\,100\\111\,110} B5 .tex= \sm{111\,100}
%D    B6 .tex= A×B B7 .tex= A
%D    @ 0 @ 1 |->
%D    @ 0 @ 2 -> @ 1 @ 3 ->
%D    @ 2 @ 3 <-|
%D    @ 2 @ 4 -> @ 3 @ 5 ->
%D    @ 4 @ 5 |->
%D    @ 0 @ 3 harrownodes nil 20 nil <->
%D    @ 2 @ 5 harrownodes nil 20 nil <->
%D    @ 6 @ 7 ->
%D ))
%D enddiagram

\def\sm#1{\begin{smallmatrix}#1\end{smallmatrix}}

`$Î$' and `$ý$' are left and right adjoint to

change-of-base along a projection $A×B \to A$...

That this is true is far from obvious,

so let's look at an example. If

$A \equiv \sm{\,}$ and

$B \equiv \sm{\\}$, then

$A×B \equiv \sm{\,\\\,}$;

using the obvious positional notation with 0s and 1s

to denote subsets of $A×B$ and $A$,

and for the right $P(a,b)$, $Q(a)$, $R(a,b)$, we have:

\msk

$\diag{quants-set}$

\bsk
\msk

Later we will see that `$Î \dashv ^* \dashv ý$' holds

even when the logic is just intuitionistic ---

and we will use this to ``define'' $Î$ and $ý$ in hyperdoctrines...

\msk

Also, we will see in which sense 

``hyperdoctrines are models of typed intuitionistic logic'',

and we will construct some hyperdoctrines in which the logic

is not classical.


\newpage
% --------------------
% «preservations-overview»  (to ".preservations-overview")
% (s "Preservations by change-of-base: overview" "preservations-overview")
\myslide {Preservations by change-of-base: overview} {preservations-overview}

Start with $f: A \to B$,

and $\cbsubobj{b}{P(b)}$ and $\cbsubobj{b}{Q(b)}$.

\msk

There are two different categorical ways to build

an object that ``deserves the name''

$\cbsubobj{a}{P(f(a))\&Q(f(a))}$.

\msk

We want these two ways to be isomorphic,

and there is a natural way to build

one of the directions of the iso ---

so the technical condition

``change-of-base functors preserve the BiCCC structure'' 

becomes, for each of the connectives $§, ®, \&, , ¶$,

that this natural half-side of the iso

will have an inverse.

\msk

More precisely:

%D diagram preservations-overview
%D 2Dx     100     +30     +40
%D 2D  100 T0      I0      IMP0
%D 2D
%D 2D
%D 2D  +30 T1      I1      IMP1
%D 2D
%D 2D  +20 A0 <==========> A1
%D 2D
%D 2D  +20 O0 <==========> O1
%D 2D
%D (( T0 .tex= f^*§_B  T1 .tex= §_A
%D    T0 T1 -> sl_ .plabel= l î=!
%D    T0 T1 <- sl^ .plabel= r ÐP§
%D ))
%D (( I0 .tex= ®_A   I1 .tex= f^*®_B
%D    I0 I1 -> sl_ .plabel= l î=!
%D    I0 I1 <- sl^ .plabel= r ÐP®
%D ))
%D (( A0 .tex= f^*P&f^*Q A1 .tex= f^*(P&Q)
%D    A0 A1 <- sl^ .plabel= a î=\ang{f^*,f^*'}
%D    A0 A1 -> sl_ .plabel= b ÐP\&
%D ))
%D (( O0 .tex= f^*Pf^*Q O1 .tex= f^*(PQ)
%D    O0 O1 -> sl^ .plabel= a î=[f^*\iota,f^*\iota']
%D    O0 O1 <- sl_ .plabel= b ÐP
%D ))
%D (( IMP0 .tex= f^*(P¶Q)   IMP1 .tex= f^*P¶f^*Q
%D    IMP0 IMP1 -> sl_ .plabel= l î=...
%D    IMP0 IMP1 <- sl^ .plabel= r ÐP¶
%D ))
%D enddiagram

\msk

$\diag{preservations-overview}$

\msk

We will see the diagrams for these constructions in the next slides.

The natural half for `$¶$', in particular, is a big construction.

\msk

The Beck-Chevalley conditions are similar: they say that the two

natural constructions for two objects that ``deserve the same name''

are isomorphic --- the natural half-side of an iso has an inverse.

\msk

Frobenius conditions are more like distributivities.

The case where they are more natural will appear later,

in another hyperdoctrine, where the same structure will

interpret different operations. There it will be this:

\msk

%D diagram frobenius-overview
%D 2Dx       100     +50
%D 2D  100 b,(c,d) (b,c),d
%D 2D
%D (( b,(c,d) (b,c),d |-> sl^ .plabel= a î
%D    b,(c,d) (b,c),d <-| sl_ .plabel= b Ð{Frob}
%D ))
%D enddiagram

$\diag{frobenius-overview}$






\newpage
% --------------------
% «pres-of-true-and-and»  (to ".pres-of-true-and-and")
% (s "Preservation of `true' and `and'" "pres-of-true-and-and")
\myslide {Preservation of `true' and `and'} {pres-of-true-and-and}

% (find-LATEX "2008hyp.tex" "first-preservations")
% (find-dn4 "experimental.lua" "thereplusxy" "x+=")

%D diagram new-pres-T-and-AND-dnc
%D 2Dx    100      +30   +30     +45      +45
%D 2D 100                A0 <============ A1
%D 2D	                  ^  ^             ^
%D 2D	                  |   \      <-|   |
%D 2D	                  -    -           -
%D 2D +20 T0 <==== T1    A2 <--| A3 <==== A4
%D 2D	   -              -    -           -
%D 2D	   |              |   /      <-|   |
%D 2D	   v              v  v             v
%D 2D +20 T2             A5 <============ A6
%D 2D
%D 2D +15 ta |---> tb    aa |-----------> ab
%D 2D
%D (( T0 .tex= §  T1 .tex= §
%D    T2 .tex= §
%D    ta .tex= a        tb .tex= b
%D    T0 T1 <= T0 T2 |-> sl_ .plabel= l î T0 T2 <-| sl^ .plabel= r ÐP§
%D    ta tb |->
%D ))
%D (( A0 .tex= P                  A1 .tex= P
%D    A2 .tex= P&Q  A3 .tex= P&Q  A4 .tex= P&Q
%D    A5 .tex= Q                  A6 .tex= Q
%D        aa x+= 10 .tex= a        ab .tex= b
%D    A0 A1 <=
%D    A0 A2 <-| A0 A3 <-|
%D    A1 A4 <-| 
%D    A0 A3 midpoint A1 A4 midpoint harrownodes nil 20 nil <-|
%D    A2 A3 <-| sl^ .plabel= a {î} A2 A3 |-> sl_ .plabel= b ÐP&  A3 A4 <=
%D    A2 A5 |-> A3 A5 |->
%D    A4 A6 |-> 
%D    A3 A5 midpoint A4 A6 midpoint harrownodes nil 20 nil <-|
%D    A5 A6 <=
%D    aa ab |->
%D ))
%D enddiagram

%D diagram new-pres-T-and-AND-std
%D 2Dx    100      +30   +30     +45      +45
%D 2D 100                A0 <============ A1
%D 2D	                  ^  ^             ^
%D 2D	                  |   \      <-|   |
%D 2D	                  -    -           -
%D 2D +20 T0 <==== T1    A2 <--| A3 <==== A4
%D 2D	   -              -    -           -
%D 2D	   |              |   /      <-|   |
%D 2D	   v              v  v             v
%D 2D +20 T2             A5 <============ A6
%D 2D
%D 2D +15 ta |---> tb    aa |-----------> ab
%D 2D
%D (( T0 .tex= f^*§_B  T1 .tex= §_B
%D    T2 .tex= §_A
%D    ta .tex= A      tb .tex= B
%D    T0 T1 <-| T0 T2 -> sl_ .plabel= l î T0 T2 <- sl^ .plabel= r ÐP§
%D    ta tb -> .plabel= a f
%D ))
%D (( A0 .tex= f^*P                          A1 .tex= P
%D    A2 .tex= f^*P&f^*Q  A3 .tex= f^*(P&Q)  A4 .tex= P&Q
%D    A5 .tex= f^*Q                          A6 .tex= Q
%D        aa x+= 10 .tex= A       ab .tex= B
%D    A0 A1 <-|
%D    A0 A2 <- A0 A3 <-
%D    A1 A4 <-
%D    A0 A3 midpoint A1 A4 midpoint harrownodes nil 20 nil <-|
%D    A2 A3 <- sl^ .plabel= a {î} A2 A3 -> sl_ .plabel= b ÐP&  A3 A4 <-|
%D    A2 A5 -> A3 A5 ->
%D    A4 A6 ->
%D    A3 A5 midpoint A4 A6 midpoint harrownodes nil 20 nil <-|
%D    A5 A6 <-|
%D    aa ab -> .plabel= a f
%D ))
%D enddiagram

$$\diag{new-pres-T-and-AND-dnc}$$

$$\diag{new-pres-T-and-AND-std}$$

\newpage
% --------------------
% «pres-of-false-and-or»  (to ".pres-of-false-and-or")
% (s "Preservation of `false' and `or'" "pres-of-false-and-or")
\myslide {Preservation of `false' and `or'} {pres-of-false-and-or}

%D diagram pres-bot-and-or-dnc
%D 2Dx    100      +30   +30     +45      +45
%D 2D 100 I0             O0 <============ O1
%D 2D	  -^              -  -             -
%D 2D	 î||              |   \      <-|   |
%D 2D	  v-              v    v           v
%D 2D +20 I1 <==== I2    O2 |--> O3 <==== O4
%D 2D	                  ^    ^           ^
%D 2D	                  |   /      <-|   |
%D 2D	                  -  -             -
%D 2D +20                O5 <============ O6
%D 2D
%D 2D +15 ia |---> ib    oa |-----------> ob
%D 2D
%D (( I0 .tex= ®
%D    I1 .tex= ®  I2 .tex= ®
%D    ia .tex= a  ib .tex= b
%D    I1 I2 <=
%D    I0 I1 |-> sl_ .plabel= l î I0 I1 <-| sl^ .plabel= r ÐP®
%D    ia ib |->
%D ))
%D (( O0 .tex= P                  O1 .tex= P
%D    O2 .tex= PQ  O3 .tex= PQ  O4 .tex= PQ
%D    O5 .tex= Q                  O6 .tex= Q
%D        oa x+= 10 .tex= a        ob .tex= b
%D    O0 O1 <=
%D    O0 O2 |-> O0 O3 |->
%D    O1 O4 |-> 
%D    O0 O3 midpoint O1 O4 midpoint harrownodes nil 20 nil <-|
%D    O2 O3 |-> sl^ .plabel= a {î} O2 O3 <-| sl_ .plabel= b ÐP  O3 O4 <=
%D    O2 O5 <-| O3 O5 <-|
%D    O4 O6 <-| 
%D    O3 O5 midpoint O4 O6 midpoint harrownodes nil 20 nil <-|
%D    O5 O6 <=
%D    oa ob |->
%D ))
%D enddiagram

%D diagram pres-bot-and-or-std
%D 2Dx    100      +30   +30     +45      +45
%D 2D 100 I0             O0 <============ O1
%D 2D	  -^              -  -             -
%D 2D	 î||              |   \      <-|   |
%D 2D	  v-              v    v           v
%D 2D +20 I1 <==== I2    O2 |--> O3 <==== O4
%D 2D	                  ^    ^           ^
%D 2D	                  |   /      <-|   |
%D 2D	                  -  -             -
%D 2D +20                O5 <============ O6
%D 2D
%D 2D +15 ia |---> ib    oa |-----------> ob
%D 2D
%D (( I0 .tex= ®_A
%D    I1 .tex= f^*®_B  I2 .tex= ®_B
%D    ia .tex= a  ib .tex= b
%D    I1 I2 <-|
%D    I0 I1 -> sl_ .plabel= l î I0 I1 <- sl^ .plabel= r ÐP®
%D    ia ib ->
%D ))
%D (( O0 .tex= f^*P                          O1 .tex= P
%D    O2 .tex= f^*Pf^*Q  O3 .tex= f^*(PQ)  O4 .tex= PQ
%D    O5 .tex= f^*Q                          O6 .tex= Q
%D        oa x+= 10 .tex= a        ob .tex= b
%D    O0 O1 <-|
%D    O0 O2 -> O0 O3 ->
%D    O1 O4 -> 
%D    O0 O3 midpoint O1 O4 midpoint harrownodes nil 20 nil <-|
%D    O2 O3 -> sl^ .plabel= a {î} O2 O3 <- sl_ .plabel= b ÐP  O3 O4 <-|
%D    O2 O5 <- O3 O5 <-
%D    O4 O6 <- 
%D    O3 O5 midpoint O4 O6 midpoint harrownodes nil 20 nil <-|
%D    O5 O6 <-|
%D    oa ob ->
%D ))
%D enddiagram

$$\diag{pres-bot-and-or-dnc}$$

$$\diag{pres-bot-and-or-std}$$




\newpage
% --------------------
% «pres-of-imp»  (to ".pres-of-imp")
% (s "Preservation of `implies'" "pres-of-imp")
\myslide {Preservation of `implies'} {pres-of-imp}


%D diagram new-pres-prod-1
%D 2Dx    100    +45                 +55   +45
%D 2Dx    100    +60                 +55   +60
%D 2D 100 B0 <-> B0' <============== B1
%D 2D	  -/\                        -/\
%D 2D	  | \\                       | \\
%D 2D	  v  \\                      v  \\
%D 2D +20 B2 <\\==================== B3  \\
%D 2D	   \\  \\                     \\  \\
%D 2D +15   \\   B4 <===================== B5
%D 2D	     \\  -                      \\ -
%D 2D	      \\ |                       \\|
%D 2D	       \/v                        Vv
%D 2D +20        B6                        B7
%D 2D
%D 2D +0  b0 |---------------------> b1
%D 2D	     |->                        |->
%D 2D +35        b2 |--------------------> b3
%D 2D
%D ((
%D    B0 .tex= (P¶Q)&P  B0' .tex= (P¶Q)&P   B1 .tex= (P¶Q)&P
%D    B2 .tex= Q        B3  .tex= Q
%D    B4 .tex= P¶Q      B5 .tex= P¶Q
%D    B6 .tex= P¶Q      B7 .tex= P¶Q
%D    B0  B0' <-| sl^ .plabel= a {î}
%D    B0  B0' |-> sl_ .plabel= b ÐP&
%D    B0' B1 <= B0 B2 |-> B0' B2 |-> B1 B3 |-> B2 B3 <=
%D    B0 B4 <= B2 B6 =>
%D    B1 B5 <= B3 B7 =>
%D    B4 B5 <= B5 B7 |-> .plabel= r \id
%D    B4 B6 |-> sl_ .plabel= l î B4 B6 <-| sl^ .plabel= r ÐP¶
%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 b2 midpoint .TeX= a b1 b3 midpoint .TeX= b |->
%D ))
%D enddiagram
%
$$\diag{new-pres-prod-1}$$

%D diagram new-pres-prod-2
%D 2Dx    100    +60                 +55   +60
%D 2D 100 B0 <-> B0' <============== B1
%D 2D	  -/\                        -/\
%D 2D	  | \\                       | \\
%D 2D	  v  \\                      v  \\
%D 2D +20 B2 <\\==================== B3  \\
%D 2D	   \\  \\                     \\  \\
%D 2D +25   \\   B4 <===================== B5
%D 2D	     \\  -                      \\ -
%D 2D	      \\ |                       \\|
%D 2D	       \/v                        Vv
%D 2D +20        B6                        B7
%D 2D
%D 2D +0  b0 |---------------------> b1
%D 2D	     |->                        |->
%D 2D +35        b2 |--------------------> b3
%D 2D
%D ((
%D    B0 .tex= f^*(P¶Q)&f^*P  B0' .tex= f^*((P¶Q)&P)   B1 .tex= (P¶Q)&P
%D    B2 .tex= f^*Q           B3  .tex= Q
%D    B4 .tex= f^*(P¶Q)       B5 .tex= P¶Q
%D    B6 .tex= f^*P¶f^*Q      B7 .tex= P¶Q
%D    B0  B0' <- sl^ .plabel= a {î}
%D    B0  B0' -> sl_ .plabel= b ÐP&
%D    B0' B1 <-| B0 B2 -> B0' B2 -> B1 B3 -> B2 B3 <-|
%D    B0 B4 <-| B2 B6 |->
%D    B1 B5 <-| B3 B7 |->
%D    B4 B5 <-| B5 B7 -> .plabel= r \id
%D    B4 B6 -> sl_ .plabel= l î B4 B6 <- sl^ .plabel= r ÐP¶
%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 b2 midpoint .TeX= A b1 b3 midpoint .TeX= B -> .plabel= a f
%D ))
%D enddiagram
%
$$\diag{new-pres-prod-2}$$


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


\newpage
% --------------------
% «bcc-for-forall»  (to ".bcc-for-forall")
% (s "BCC for `forall'" "bcc-for-forall")
\myslide {BCC for `forall'} {bcc-for-forall}


%D diagram bcc-for-forall-1
%D 2Dx    100    +45                 +55   +45
%D 2D 100 B0 <-> B0' <============== B1
%D 2D	  -/\                        -/\
%D 2D	  | \\                       | \\
%D 2D	  v  \\                      v  \\
%D 2D +20 B2 <\\==================== B3  \\
%D 2D	   \\  \\                     \\  \\
%D 2D +15   \\   B4 <===================== B5
%D 2D	     \\  -                      \\ -
%D 2D	      \\ |                       \\|
%D 2D	       \/v                        Vv
%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= ýc.P  B0' .tex= ýc.P   B1 .tex= ýc.P
%D    B2 .tex= P        B3  .tex= P
%D    B4 .tex= ýc.P     B5 .tex= ýc.P
%D    B6 .tex= ýc.P     B7 .tex= ýc.P
%D    B0  B0' <-> B0' B1 <= B0 B2 |-> B0' B2 |-> B1 B3 |-> B2 B3 <=
%D    B0 B4 <= B2 B6 =>
%D    B1 B5 <= B3 B7 =>
%D    B4 B5 <= B5 B7 |-> .plabel= r \id
%D    B4 B6 |-> sl_ .plabel= l î B4 B6 <-| sl^ .plabel= r Ð{BCC}ý
%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,c b1 .tex= b,c b2 .tex= a b3 .tex= b
%D    b0 b1 |-> b0 b2 |-> b1 b3 |-> b2 b3 |->
%D    b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-for-forall-1}$$

% dnc->std: (fooi "`->" ">->" "|->" "->" "<-|" "<-" "=>" "|->" "<=" "<-|")

%D diagram bcc-for-forall-2
%D 2Dx    100    +45                 +55   +45
%D 2D 100 B0 <-> B0' <============== B1
%D 2D	  -/\                        -/\
%D 2D	  | \\                       | \\
%D 2D	  v  \\                      v  \\
%D 2D +20 B2 <\\==================== B3  \\
%D 2D	   \\  \\                     \\  \\
%D 2D +15   \\   B4 <===================== B5
%D 2D	     \\  -                      \\ -
%D 2D	      \\ |                       \\|
%D 2D	       \/v                        Vv
%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= c'*f^*ý_cP  B0' .tex= f'*c^*ý_cP  B1 .tex= c^*ý_cP
%D    B2 .tex= f'*P        B3  .tex= P
%D    B4 .tex= f^*ý_cP     B5 .tex= ý_cP
%D    B6 .tex= ý_{c'}f'*P     B7 .tex= ý_cP
%D    B0  B0' <-> B0' B1 <-| B0 B2 -> B0' B2 -> B1 B3 -> B2 B3 <-|
%D    B0 B4 <-| B2 B6 |->
%D    B1 B5 <-| B3 B7 |->
%D    B4 B5 <-| B5 B7 -> .plabel= r \id
%D    B4 B6 -> sl_ .plabel= l î B4 B6 <- sl^ .plabel= r Ð{BCC}ý
%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×C b1 .tex= B×C b2 .tex= A b3 .tex= B
%D    b0 b1 -> .plabel= b f'
%D    b0 b2 -> .plabel= l c'
%D    b1 b3 -> .plabel= r c
%D    b2 b3 -> .plabel= a f
%D    b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-for-forall-2}$$


\newpage
% --------------------
% «bcc-for-exists»  (to ".bcc-for-exists")
% (s "BCC for `exists'" "bcc-for-exists")
\myslide {BCC for `exists'} {bcc-for-exists}

%D diagram bcc-for-exists-1
%D 2Dx    100     +45                +55   +45
%D 2D 100 B0 <====================== B1
%D 2D	  -\\                        -\\
%D 2D	  | \\                       | \\
%D 2D	  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= P                    B1 .tex= P
%D    B2 .tex= Îc.P B2' .tex= Îc.P  B3 .tex= Îc.P
%D    B4 .tex= Îc.P                 B5 .tex= Îc.P
%D    B6 .tex= Îc.P                 B7 .tex= Îc.P
%D    B0 B1 <= B0 B2 |-> B0 B2' |-> B1 B3 |-> B2 B2' <-> B2' B3 <=
%D    B0 B4 => B1 B5 =>
%D    B2 B6 <= B3 B7 <=
%D    B6 B7 <= B5 B7 |-> .plabel= r \id
%D    B4 B6 |-> sl_ .plabel= l î B4 B6 <-| sl^ .plabel= r Ð{BCC}Î
%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,c b1 .tex= b,c b2 .tex= a b3 .tex= b
%D    b0 b1 |-> b0 b2 |-> b1 b3 |-> b2 b3 |->
%D    b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-for-exists-1}$$

% dnc->std: (fooi "`->" ">->" "|->" "->" "<-|" "<-" "=>" "|->" "<=" "<-|")

%D diagram bcc-for-exists-2
%D 2Dx    100     +45                +55   +45
%D 2D 100 B0 <====================== B1
%D 2D	  -\\                        -\\
%D 2D	  | \\                       | \\
%D 2D	  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= f'*P                              B1 .tex= P
%D    B2 .tex= c'*f^*Î_cP  B2' .tex= f'*c^*Î_cP  B3 .tex= c^*Î_cP
%D    B4 .tex= Î_{c'}f'*P                        B5 .tex= Î_cP
%D    B6 .tex= f^*Î_cP                           B7 .tex= Î_cP
%D    B0 B1 <-| B0 B2 -> B0 B2' -> B1 B3 -> B2 B2' <-> B2' B3 <-|
%D    B0 B4 |-> B1 B5 |->
%D    B2 B6 <-| B3 B7 <-|
%D    B6 B7 <-| B5 B7 -> .plabel= r \id
%D    B4 B6 -> sl_ .plabel= l î B4 B6 <- sl^ .plabel= r Ð{BCC}Î
%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×C b1 .tex= B×C b2 .tex= A b3 .tex= B
%D    b0 b1 -> .plabel= b f'
%D    b0 b2 -> .plabel= l c'
%D    b1 b3 -> .plabel= r c
%D    b2 b3 -> .plabel= b f
%D    b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-for-exists-2}$$


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

%D diagram bcc-for-equality-1
%D 2Dx    100     +45                +55   +45
%D 2D 100 B0 <====================== B1
%D 2D	  -\\                        -\\
%D 2D	  | \\                       | \\
%D 2D	  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= P                              B1 .tex= P
%D    B2 .tex= c{=}c{&}P B2' .tex= c{=}c{&}P  B3 .tex= c{=}c{&}P
%D    B4 .tex= c{=}c'{&}P                     B5 .tex= c{=}c'{&}P
%D    B6 .tex= c{=}c'{&}P                     B7 .tex= c{=}c'{&}P
%D    B0 B1 <= B0 B2 |-> B0 B2' |-> B1 B3 |-> B2 B2' <-> B2' B3 <=
%D    B0 B4 => B1 B5 =>
%D    B2 B6 <= B3 B7 <=
%D    B6 B7 <= B5 B7 |-> .plabel= r \id
%D    B4 B6 |-> sl_ .plabel= l î B4 B6 <-| sl^ .plabel= r Ð{BCC}Î
%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,c b1 .tex= b,c b2 .tex= a,c,c' b3 .tex= b,c,c'
%D    b0 b1 |-> b0 b2 |-> b1 b3 |-> b2 b3 |->
%D    b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-for-equality-1}$$

%D diagram bcc-for-equality-2
%D 2Dx    100     +45                +55   +45
%D 2D 100 B0 <====================== B1
%D 2D	  -\\                        -\\
%D 2D	  | \\                       | \\
%D 2D	  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= f'*P                              B1 .tex= P
%D    B2 .tex= c'*f^*\Eq_{c}P  B2' .tex= f'*c^*\Eq_{c}P  B3 .tex= c^*\Eq_{c}P
%D    B4 .tex= \Eq_{c'}f'*P                      B5 .tex= \Eq_{c}P
%D    B6 .tex= f^*\Eq_{c}P                       B7 .tex= \Eq_{c}P
%D    B0 B1 <-| B0 B2 -> B0 B2' -> B1 B3 -> B2 B2' <-> B2' B3 <-|
%D    B0 B4 |-> B1 B5 |->
%D    B2 B6 <-| B3 B7 <-|
%D    B6 B7 <-| B5 B7 -> .plabel= r \id
%D    B4 B6 -> sl_ .plabel= l î B4 B6 <- sl^ .plabel= r Ð{BCC}=
%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×C b1 .tex= B×C b2 .tex= A×C×C b3 .tex= B×C×C
%D    b0 b1 -> .plabel= b f'
%D    b0 b2 -> .plabel= l c'
%D    b1 b3 -> .plabel= r c
%D    b2 b3 -> .plabel= b f
%D    b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-for-equality-2}$$


\newpage
% --------------------
% «frob-for-exists»  (to ".frob-for-exists")
% (s "Frobenius for `exists'" "frob-for-exists")
\myslide {Frobenius for `exists'} {frob-for-exists}

%D diagram frob-for-exists-1
%D 2Dx    100          +45 +35 +10
%D 2D 100 B0 ================> B1
%D 2D	  ^                  ^ ^ 
%D 2D	  |                 /  | 
%D 2D	  -                \   - 
%D 2D +20 B2 ========> B3 <--> B3'
%D 2D	  -                /   - 
%D 2D	  |                 \  |
%D 2D	  v                  v v
%D 2D +20 B4 <================ B5         
%D 2D
%D 2D +15 b0 |-----------> b1
%D 2D
%D ((
%D    B0 .tex= P                      B1  .tex=  Îc.P
%D    B2 .tex= P&Q  B3 .tex= Îc.(P&Q) B3' .tex= (Îc.P)&Q
%D    B4 .tex= Q                      B5  .tex=     Q
%D    B0 B1 =>   B2 B0 |-> B3 B1 |-> B3' B1 |->
%D    B4 B5 <=   B2 B4 |-> B3 B5 |-> B3' B5 |->
%D    B2 B3 =>   B3 B3' |-> sl^ .plabel= a î  B3 B3' <-| sl_ .plabel= b Ð{Frob}Î
%D    B0 B2 midpoint B1 B3 midpoint  harrownodes nil 20 nil |->
%D    B2 B4 midpoint B3 B5 midpoint  harrownodes nil 20 nil |->
%D ))
%D (( b0 .tex= b,c b1 .tex= b   b0 b1 |->
%D ))
%D enddiagram
%
$$\diag{frob-for-exists-1}$$

% dnc->std: (fooi "`->" ">->" "|->" "->" "<-|" "<-" "=>" "|->" "<=" "<-|")

%D diagram frob-for-exists-2
%D 2Dx    100          +45 +35 +10
%D 2D 100 B0 ================> B1
%D 2D	  ^                  ^ ^ 
%D 2D	  |                 /  | 
%D 2D	  -                \   - 
%D 2D +20 B2 ========> B3 <--> B3'
%D 2D	  -                /   - 
%D 2D	  |                 \  |
%D 2D	  v                  v v
%D 2D +20 B4 <================ B5         
%D 2D
%D 2D +15 b0 |-----------> b1
%D 2D
%D ((
%D    B0 .tex= P                            B1  .tex=  Î_cP
%D    B2 .tex= P&c^*Q  B3 .tex= Î_c(P&c^*Q) B3' .tex= (Î_cP)&Q
%D    B4 .tex= c^*Q                         B5  .tex=     Q
%D    B0 B1 |->   B2 B0 -> B3 B1 -> B3' B1 ->
%D    B4 B5 <-|   B2 B4 -> B3 B5 -> B3' B5 ->
%D    B2 B3 |->   B3 B3' -> sl^ .plabel= a î  B3 B3' <- sl_ .plabel= b Ð{Frob}Î
%D    B0 B2 midpoint B1 B3 midpoint  harrownodes nil 20 nil |->
%D    B2 B4 midpoint B3 B5 midpoint  harrownodes nil 20 nil |->
%D ))
%D (( b0 .tex= B×C b1 .tex= B   b0 b1 -> .plabel= a c
%D ))
%D enddiagram
%
$$\diag{frob-for-exists-2}$$

\newpage
% --------------------
% «frob-for-equality»  (to ".frob-for-equality")
% (s "Frobenius for equality" "frob-for-equality")
\myslide {Frobenius for equality} {frob-for-equality}

%D diagram frob-for-equality-1
%D 2Dx    100          +50 +40 +15
%D 2D 100 B0 ================> B1
%D 2D	  ^                  ^ ^ 
%D 2D	  |                 /  | 
%D 2D	  -                \   - 
%D 2D +20 B2 ========> B3 <--> B3'
%D 2D	  -                /   - 
%D 2D	  |                 \  |
%D 2D	  v                  v v
%D 2D +20 B4 <================ B5         
%D 2D
%D 2D +15 b0 |-----------> b1
%D 2D
%D ((
%D    B0 .tex= P                            B1  .tex=  c{=}c'{&}P
%D    B2 .tex= P&Q  B3 .tex= c{=}c'{&}(P&Q) B3' .tex= (c{=}c'{&}P)&Q
%D    B4 .tex= Q                            B5  .tex=     Q
%D    B0 B1 =>   B2 B0 |-> B3 B1 |-> B3' B1 |->
%D    B4 B5 <=   B2 B4 |-> B3 B5 |-> B3' B5 |->
%D    B2 B3 =>   B3 B3' |-> sl^ .plabel= a î  B3 B3' <-| sl_ .plabel= b Ð{Frob}=
%D    B0 B2 midpoint B1 B3 midpoint  harrownodes nil 20 nil |->
%D    B2 B4 midpoint B3 B5 midpoint  harrownodes nil 20 nil |->
%D ))
%D (( b0 .tex= b,c b1 .tex= b,c,c'   b0 b1 |->
%D ))
%D enddiagram
%
$$\diag{frob-for-equality-1}$$

%D diagram frob-for-equality-2
%D 2Dx    100          +45 +35 +10
%D 2Dx    100          +50 +40 +15
%D 2D 100 B0 ================> B1
%D 2D	  ^                  ^ ^ 
%D 2D	  |                 /  | 
%D 2D	  -                \   - 
%D 2D +20 B2 ========> B3 <--> B3'
%D 2D	  -                /   - 
%D 2D	  |                 \  |
%D 2D	  v                  v v
%D 2D +20 B4 <================ B5         
%D 2D
%D 2D +15 b0 |-----------> b1
%D 2D
%D ((
%D    B0 .tex= P                              B1  .tex=  \Eq_cP
%D    B2 .tex= P&c^*Q  B3 .tex= \Eq_c(P&c^*Q) B3' .tex= (\Eq_cP)&Q
%D    B4 .tex= c^*Q                           B5  .tex=     Q
%D    B0 B1 |->   B2 B0 -> B3 B1 -> B3' B1 ->
%D    B4 B5 <-|   B2 B4 -> B3 B5 -> B3' B5 ->
%D    B2 B3 |->   B3 B3' -> sl^ .plabel= a î  B3 B3' <- sl_ .plabel= b Ð{Frob}=
%D    B0 B2 midpoint B1 B3 midpoint  harrownodes nil 20 nil |->
%D    B2 B4 midpoint B3 B5 midpoint  harrownodes nil 20 nil |->
%D ))
%D (( b0 .tex= B×C b1 .tex= B×C×C   b0 b1 -> .plabel= a c
%D ))
%D enddiagram
%
$$\diag{frob-for-equality-2}$$


\newpage
% --------------------
% «frob-for-ex-eq»  (to ".frob-for-ex-eq")
% (s "Frobenius for exists-equal" "frob-for-ex-eq")
\myslide {Frobenius for exists-equal} {frob-for-ex-eq}

%D diagram frob-for-ex-eq-1
%D 2Dx    100          +60 +55 +25
%D 2D 100 B0 ================> B1
%D 2D	  ^                  ^ ^ 
%D 2D	  |                 /  | 
%D 2D	  -                \   - 
%D 2D +20 B2 ========> B3 <--> B3'
%D 2D	  -                /   - 
%D 2D	  |                 \  |
%D 2D	  v                  v v
%D 2D +20 B4 <================ B5         
%D 2D
%D 2D +15 b0 |-----------> b1
%D 2D
%D ((
%D    B0 .tex= Pa                                B1  .tex=  Îa.b=fa&Pa
%D    B2 .tex= Pa&Qfa  B3 .tex= Îa.b=fa&(Pa&Qfa) B3' .tex= (Îa.b=fa&Pa)&Qb
%D    B4 .tex= Qfa                               B5  .tex=     Qb
%D    B0 B1 =>   B2 B0 |-> B3 B1 |-> B3' B1 |->
%D    B4 B5 <=   B2 B4 |-> B3 B5 |-> B3' B5 |->
%D    B2 B3 =>   B3 B3' |-> sl^ .plabel= a î  B3 B3' <-| sl_ .plabel= b Ð{Frob}Î=
%D    B0 B2 midpoint B1 B3 midpoint  harrownodes nil 20 nil |->
%D    B2 B4 midpoint B3 B5 midpoint  harrownodes nil 20 nil |->
%D ))
%D (( b0 .tex= a b1 .tex= b   b0 b1 |->
%D ))
%D enddiagram
%
$$\diag{frob-for-ex-eq-1}$$

%D diagram frob-for-ex-eq-2
%D 2Dx    100          +60 +55 +25
%D 2D 100 B0 ================> B1
%D 2D	  ^                  ^ ^ 
%D 2D	  |                 /  | 
%D 2D	  -                \   - 
%D 2D +20 B2 ========> B3 <--> B3'
%D 2D	  -                /   - 
%D 2D	  |                 \  |
%D 2D	  v                  v v
%D 2D +20 B4 <================ B5         
%D 2D
%D 2D +15 b0 |-----------> b1
%D 2D
%D ((
%D    B0 .tex= P                              B1  .tex=  \Eq_fP
%D    B2 .tex= P&f^*Q  B3 .tex= \Eq_f(P&f^*Q) B3' .tex= (\Eq_fP)&Q
%D    B4 .tex= f^*Q                           B5  .tex=     Q
%D    B0 B1 |->   B2 B0 -> B3 B1 -> B3' B1 ->
%D    B4 B5 <-|   B2 B4 -> B3 B5 -> B3' B5 ->
%D    B2 B3 |->   B3 B3' -> sl^ .plabel= a î  B3 B3' <- sl_ .plabel= b Ð{Frob}Î=
%D    B0 B2 midpoint B1 B3 midpoint  harrownodes nil 20 nil |->
%D    B2 B4 midpoint B3 B5 midpoint  harrownodes nil 20 nil |->
%D ))
%D (( b0 .tex= A b1 .tex= B   b0 b1 -> .plabel= a f
%D ))
%D enddiagram
%
$$\diag{frob-for-ex-eq-2}$$



\newpage
% --------------------
% «frob-and-pres-imp»  (to ".frob-and-pres-imp")
% (s "Frobenius is equivalent to preservation of `implies'" "frob-and-pres-imp")
\myslide {Frobenius is equivalent to preservation of `implies'} {frob-and-pres-imp}

%D diagram lawfrob1
%D 2Dx       100          +40         +35             +40       +40            +45
%D 2D            \aa´()
%D 2D  100 P(Y)`0 -----> P(Y)`1    \aa´\phiÆf <----| \phiÆf (Îb.Pab)´Qa <=== Îb.Pab
%D 2D          |           |         î ^v Frob         ^       î ^v Frob        /\
%D 2D  +20     |           |     ((f·\aa)´\phi)Æf      |      Îb.(Pab´Qa)       ||
%D 2D      ()Æf|       ()Æf|            ^              |          /\            ||
%D 2D          v           v            |              -          ||            ||
%D 2D  +30 P(X)`0 -----> P(X)`1    (f·\aa)´\phi <---| \phi      Pab´Qa <====== Pab
%D 2D          (f·\aa)´()
%D 2D
%D (( P(Y)`0 P(Y)`1 
%D    P(X)`0 P(X)`1
%D    @ 0 @ 1 <- .plabel= a \aa´(\;)
%D    @ 0 @ 2 <- .plabel= l (\;)Æf
%D    @ 1 @ 3 <- .plabel= l (\;)Æf
%D    @ 2 @ 3 <- .plabel= b (f·\aa)´(\;)
%D ))
%D ((      \aa´\phiÆf     \phiÆf
%D    ((f·\aa)´\phi)Æf
%D     (f·\aa)´\phi       \phi
%D    @ 0 @ 1 <-|
%D    @ 0 @ 2 <- sl_ .plabel= l î   @ 0 @ 2 -> sl^ .plabel= r Ð{Frob}
%D    @ 2 @ 3 <-| @ 1 @ 4 <-|
%D    @ 3 @ 4 <-|
%D ))
%D (( (Îb.Pab)´Qa   Îb.Pab
%D     Îb.(Pab´Qa)
%D         Pab´Qa      Pab
%D    @ 0 @ 1 <=
%D    @ 0 @ 2 <-| sl_ .plabel= l î   @ 0 @ 2 |-> sl^ .plabel= r Ð{Frob}
%D    @ 2 @ 3 <= @ 1 @ 4 <=
%D    @ 3 @ 4 <=
%D ))
%D enddiagram
%D
$$\diag{lawfrob1}$$

%D diagram lawfrob2
%D 2Dx     100           +40       +35           +40         +40        +45
%D 2D            \aa=>()
%D 2D  100 P(Y)`0 -----> P(Y)`1    \psi |----> \aa=>\psi     Ra`0 ===> Qa¶Ra`0
%D 2D	       |           |         -             -          ||        ||
%D 2D	   f·()|       f·()|         |             v          ||        \/
%D 2D  +30     |           |         |        f·(\aa=>\psi)   ||       Qa¶Ra`1
%D 2D          v           v         v          î v^ P¶       \/       î v^ P¶
%D 2D  +20 P(X)`0 -----> P(X)`1   f·\psi |--> f·\aa=>f·\psi  Ra`2 ===> Qa¶Ra`2
%D 2D	       (f·\aa)=>()
%D 2D
%D (( P(Y)`0 P(Y)`1 
%D    P(X)`0 P(X)`1
%D    @ 0 @ 1 -> .plabel= a \aa=>(\;)
%D    @ 0 @ 2 -> .plabel= l f·(\;)
%D    @ 1 @ 3 -> .plabel= l f·(\;)
%D    @ 2 @ 3 -> .plabel= b (f·\aa)=>(\;)
%D ))
%D (( \psi      \aa=>\psi
%D           f·(\aa=>\psi)
%D    f·\psi f·\aa=>f·\psi
%D    @ 0 @ 1 |-> @ 0 @ 3 |-> @ 1 @ 2 |-> @ 3 @ 4 |->
%D    @ 2 @ 4 -> sl_ .plabel= l î   @ 2 @ 4 <- sl^ .plabel= r ÐP¶
%D ))
%D (( Ra`0   Qa¶Ra`0
%D           Qa¶Ra`1
%D    Ra`2 Qa¶Ra`2
%D    @ 0 @ 1 => @ 0 @ 3 => @ 1 @ 2 => @ 3 @ 4 =>
%D    @ 2 @ 4 |-> sl_ .plabel= l î   @ 2 @ 4 <- sl^ .plabel= r ÐP¶
%D ))
%D enddiagram
%D
$$\diag{lawfrob2}$$

%D diagram lawfrob-std
%D 2Dx                 100                          +80
%D 2D 100       \H{\aa´\phiÆf}{\psi} <---> \H{\phiÆf}{\aa=>\psi}
%D 2D                î v^ Frob                      ^
%D 2D +20 \H{((f·\aa)´\phi)Æf}{\psi}                |
%D 2D                   ^                           |
%D 2D                   |                           |
%D 2D                   |                           v
%D 2D +10               |                 \H{\phi}{f·(\aa=>\psi)}
%D 2D                   v                        î v^ P¶
%D 2D +20 \H{(f·\aa)´\phi}{f·\psi} <---> \H{\phi}{f·\aa=>f·\psi)}
%D 2D
%D ((       \H{\aa´\phiÆf}{\psi}  \H{\phiÆf}{\aa=>\psi}
%D    \H{((f·\aa)´\phi)Æf}{\psi}
%D                               \H{\phi}{f·(\aa=>\psi)}
%D      \H{(f·\aa)´\phi}{f·\psi} \H{\phi}{f·\aa=>f·\psi)}
%D    @ 0 @ 1 <->
%D    @ 0 @ 2 -> sl_ .plabel= l î   @ 0 @ 2 <- sl^ .plabel= r Ð{Frob}
%D    @ 1 @ 3 <-> @ 2 @ 4 <-> 
%D    @ 3 @ 5 -> sl_ .plabel= l î   @ 3 @ 5 <- sl^ .plabel= r ÐP¶
%D    @ 4 @ 5 <->
%D ))
%D enddiagram
%D
$$\def\H#1#2{(#1\to#2)}
  \diag{lawfrob-std}
$$

%D diagram lawfrob-dnc
%D 2Dx           100               +70
%D 2D  100 (Îb.Pab)´Qa|-Ra <-> Îb.Pab|-Qa¶Ra
%D 2D         î v^ Frob             ^                
%D 2D  +20 Îb.(Pab´Qa)|-Ra          |
%D 2D              ^                |
%D 2D              |                |
%D 2D              |                v
%D 2D  +10         |             Pab|-Qa¶Ra`1
%D 2D              v              î v^ P¶             
%D 2D  +20      Pab´Qa|-Ra <---> Pab|-Qa¶Ra`2
%D 2D
%D (( (Îb.Pab)´Qa|-Ra Îb.Pab|-Qa¶Ra
%D    Îb.(Pab´Qa)|-Ra
%D                     Pab|-Qa¶Ra`1
%D         Pab´Qa|-Ra  Pab|-Qa¶Ra`2
%D    @ 0 @ 1 <->
%D    @ 0 @ 2 -> sl_ .plabel= l î   @ 0 @ 2 <- sl^ .plabel= r Ð{Frob}
%D    @ 1 @ 3 <-> @ 2 @ 4 <-> 
%D    @ 3 @ 5 -> sl_ .plabel= l î   @ 3 @ 5 <- sl^ .plabel= r ÐP¶
%D    @ 4 @ 5 <->
%D ))
%D enddiagram
%D
$$\diag{lawfrob-dnc}$$

\newpage
% --------------------
% «bcc-ex-iff-bcc-fa»  (to ".bcc-ex-iff-bcc-fa")
% (s "BCC for `exists' holds iff BCC for `forall' holds" "bcc-ex-iff-bcc-fa")
\myslide {BCC for `exists' holds iff BCC for `forall' holds} {bcc-ex-iff-bcc-fa}

%D diagram lawbcc1
%D 2Dx       100        +40     +35          +40        +40             +45
%D 2D  100   X -------> X'  f·\psi |--> (f·\psi)Æx    x·\phi <-------| \phi
%D 2D        | _| x     |       ^       î v^ BCCÆ        -               -
%D 2D  +20   |          |       |       f'·(\psiÆy)      |               |
%D 2D        | f     f' |       |            ^           v               |
%D 2D  +10   |          |       |            |       (x·\phi)åf          |
%D 2D        v    y     v       -            -       î ^v BCCå           v	       
%D 2D  +20   Y -------> Y'    \psi |----> \psiÆy      y·(\phiåf') <--| \phiåf'
%D 2D                                                                              
%D 2D  +20 a,b,c |---> a,b   Pac`2 ====> Îc.Pac`2      Rab`1 <========= Rab`0
%D 2D        - _|       -      /\       î v^ BCCÎ        ||              ||	       
%D 2D  +20   |          |      ||        Îc.Pac`1        ||              ||	       
%D 2D        |          |      ||          /\            \/              ||	       
%D 2D  +10   |          |      ||          ||         ýb.Rab`2           ||	       
%D 2D        v          v      ||          ||        î ^v BCCý           \/	       
%D 2D  +20  a,c |-----> a    Pac`0 ====> Îc.Pac`0     ýb.Rab`1 <===== ýb.Rab`0
%D 2D      
%D (( X X'   Y Y'
%D    @ 0 @ 1 -> .plabel= a x   @ 0 _|
%D    @ 0 @ 2 -> .plabel= l f
%D    @ 1 @ 3 -> .plabel= l f'
%D    @ 2 @ 3 -> .plabel= a y
%D ))
%D (( f·\psi (f·\psi)Æx
%D           f'·(\psiÆy)
%D      \psi     \psiÆy
%D    @ 0 @ 1 |-> .plabel= a (\;)Æx
%D    @ 0 @ 3 <-| .plabel= l f·(\;)
%D    @ 1 @ 2 -> sl_ .plabel= l î   @ 1 @ 2 <- sl^ .plabel= r Ð{BCC}
%D    @ 2 @ 4 <-| .plabel= l f'·(\;)
%D    @ 3 @ 4 |-> .plabel= a (\;)Æy
%D ))
%D ((  x·\phi      \phi
%D    (x·\phi)åf
%D     y·(\phiåf') \phiåf'
%D    @ 0 @ 1 <-| .plabel= a x·(\;)
%D    @ 0 @ 2 |-> .plabel= l (\;)åf
%D    @ 1 @ 4 |-> .plabel= l (\;)åf'
%D    @ 2 @ 3 -> sl_ .plabel= l î   @ 2 @ 3 <- sl^ .plabel= r Ð{BCC}
%D    @ 3 @ 4 <-| .plabel= a y·(\;)
%D ))
%D (( a,b,c a,b   a,c a
%D    @ 0 @ 1 |-> @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D    @ 0 _|
%D ))
%D (( Pac`2 Îc.Pac`2
%D          Îc.Pac`1
%D    Pac`0 Îc.Pac`0
%D    @ 0 @ 1 =>  @ 0 @ 3 <=
%D    @ 1 @ 2 |-> sl_ .plabel= l î   @ 1 @ 2 <-| sl^ .plabel= r Ð{BCC}
%D    @ 2 @ 4 <=  @ 3 @ 4 =>
%D ))
%D ((    Rab`1    Rab`0
%D    ýb.Rab`2
%D    ýb.Rab`1 ýb.Rab`0
%D    @ 0 @ 1 <= @ 0 @ 2 => @ 1 @ 4 =>
%D    @ 2 @ 3 |-> sl_ .plabel= l î   @ 2 @ 3 <-| sl^ .plabel= r Ð{BCC}
%D    @ 3 @ 4 <=
%D ))
%D enddiagram
%
$$\diag{lawbcc1}$$

%D diagram lawbcc-std
%D 2Dx             100                     +60
%D 2D  100 \H{f·\psi}{x·\phi} <--> \H{(f·\psi)Æx}{\phi}
%D 2D               ^                       ^v
%D 2D  +20          |              \H{f'·(\psiÆy)}{\phi}
%D 2D               v                        ^
%D 2D  +10 \H{\psi}{(x·\phi)åf}              |
%D 2D              ^v                        v
%D 2D  +20 \H{\psi}{y·(\phiåf')} <-> \H{\psiÆy}{\phiåf'}
%D 2D
%D (( \H{f·\psi}{x·\phi}    \H{(f·\psi)Æx}{\phi}
%D                          \H{f'·(\psiÆy)}{\phi}
%D    \H{\psi}{(x·\phi)åf}
%D    \H{\psi}{y·(\phiåf')} \H{\psiÆy}{\phiåf'}
%D    @ 0 @ 1 <->  @ 0 @ 3 <->
%D    @ 1 @ 2 -> sl_ .plabel= l î   @ 1 @ 2 <- sl^ .plabel= r Ð{BCC}
%D    @ 2 @ 5 <->
%D    @ 3 @ 4 -> sl_ .plabel= l î   @ 3 @ 4 <- sl^ .plabel= r Ð{BCC}
%D    @ 4 @ 5 <->
%D ))
%D enddiagram
%D
$$\def\H#1#2{(#1\to#2)}
  \diag{lawbcc-std}
$$

%D diagram lawbcc-dnc
%D 2Dx          100             +60
%D 2D  100    Pac|-Rab <---> Îc.Pac|-Rab
%D 2D             ^              v^
%D 2D  +20        |        {}Îc.Pac|-Rab
%D 2D             v              ^
%D 2D  +10  Pac|-ýb.Rab{}        |
%D 2D           v^               v
%D 2D  +20  Pac|-ýb.Rab <-> Îc.Pac|-ýb.Rab
%D 2D
%D (( Pac|-Rab        Îc.Pac|-Rab
%D                  {}Îc.Pac|-Rab
%D    Pac|-ýb.Rab{}
%D    Pac|-ýb.Rab     Îc.Pac|-ýb.Rab
%D    @ 0 @ 1 <->  @ 0 @ 3 <->
%D    @ 1 @ 2 |-> sl_ .plabel= l î   @ 1 @ 2 <-| sl^ .plabel= r Ð{BCC}
%D    @ 2 @ 5 <->
%D    @ 3 @ 4 |-> sl_ .plabel= l î   @ 3 @ 4 <-| sl^ .plabel= r Ð{BCC}
%D    @ 4 @ 5 <->
%D ))
%D enddiagram
%D
$$\diag{lawbcc-dnc}$$



\newpage
% --------------------
% «constrs-to-proofs-and-back»  (to ".constrs-to-proofs-and-back")
% (s "From ``constructions'' to ``intuitionistic proofs'', and back" "constrs-to-proofs-and-back")
\myslide {From ``constructions'' to ``intuitionistic proofs'', and back} {constrs-to-proofs-and-back}

We have a notion of ``categorical construction''

and a notion of ``intuitionistic proof'';

neither of them are very clear now ---

but I will start with some examples,

and show how every ``categorical construction''

in a hyperdoctrine can be translated to an

``intuitionistic proof'', and how an

``intuitionistic proof'' in a certain

typed intuitionistic logic can be translated

to a ``categorical construction'' in a hyperdoctrine...

\msk

Only after seeing these two translations in detail

we will start to think about adding new constants,

axioms, operations and rules to our

``typed intuitionistic logic'', and how to add new

constants, operations, equalities, etc, to our

notion of hyperdoctrine.

\msk

Note: in this beginning all our categorical constructions

will look as if they were happening in Sub(Set)->Set ---

because at this moment that is the only hyperdoctrine we know ---

but the abstract diagrams that we will produce in the process

will later be seen to be appliable to every hyperdoctrine.

\msk

Similarly, all our intuitionistic proofs will look

as if they were just happening in a fragment of the full

language for sets and first-order predicates, but later

we will see that they will also apply to other ``languages''

and ``logics'', with ``models'' different from Sub(Set)->Set...

\msk

{\it But we need concrete examples to start with.}



\newpage
% --------------------
% «adj-functors-as-seq-rules»  (to ".adj-functors-as-seq-rules")
% (s "The adjunction functors as sequent rules" "adj-functors-as-seq-rules")
\myslide {The adjunction functors as sequent rules} {adj-functors-as-seq-rules}

%:
%:
%:   P&Q <=== P       P|-P'          R|-R'
%:    -  <b|  -      ---------&Q    ---------Q¶
%:    |       |      P&Q|-P'&Q      Q¶R|-Q¶R'
%:    v  |#>  v
%:    R ===> Q¶R     ^andQ--ftr     ^Qimp--ftr
%:
%:  (P,Q) ==> PQ
%:    -   |b>  -
%:    |        |     P|-P'  Q|-Q'       R|-R'            S|-S'  T|-T'
%:    v   <#|  v     ------------   ---------------K    ------------&
%:  (R,R) <=== R      PQ|-P'Q'     (R|-R'),(R|-R')      S&T|-S'&T'
%:    -   <b|  -
%:    |        |      ^or--ftr       ^dbl--ftr            ^and--ftr
%:    v   |#>  v
%:  (S,T) ==> S&T
%:
%:  Pab ===> Îb.Pab
%:   -   |b>   -
%:   |         |         Pab|-P'ab       Qa|-Q'a        Rab|-R'ab
%:   v   <#|   v      ---------------Î   -------W       ---------------ý
%:  Qa <====== Qa     Îb.Pab|-Îb.P'ab    Qa|-Q'a        ýb.Rab|-ýb.R'ab
%:   -   <b|   -
%:   |         |      ^ex--ftr           ^wkn--ftr      ^fa--ftr
%:   v   |#>   v
%:  Rab ===> ýb.Rab
%:
%:  a,b|-----> a
%:
%:  Pab ==> b=b'&Pab         Pab|-P'ab          Qabb'|-Q'abb'
%:   -  |b>   -         ------------------=&    ---------(b':=b)
%:   |        |         b=b'&Pab|-b=b'&Pab      Qabb|-Q'abb
%:   v  <#|   v
%:  Qabb <== Qabb'      ^=and--ftr              ^smash--ftr
%:   -  <b|   -
%:   |        |              Rab|-R'ab
%:   v  |#>   v         ------------------=¶
%:  Rab ===> b=b'¶Rab   b=b'¶Rab|-b=b'¶R'ab
%:
%:  a,b |--> a,b,b'     ^=imp--ftr
%:
%:
%:  Pa ==> Îa.b=fa&Pb            Pa|-P'a               Qb|-Q'b
%:   -    |b>   -       -----------------------Î=     ---------(b:=fa)
%:   |          |       Îa.b=fa&Pb|-Îa.b=fa&.Pb       Qfa|-Q'fa
%:   v    <#|   v
%:  Qfa <====== Qb      ^ex=--ftr                      ^ba--ftr
%:   -    <b|   -
%:   |          |                Ra|-R'a
%:   v    |#>   v       -----------------------ý=
%:  Ra ===> ýa.b=fa¶Rb  ýa.b=fa¶Ra|-ýa.b=fa¶R'a
%:
%:  a |------> b        ^fa=--ftr
%:
\def\foooandimpftr{   \footwov   { \ded{andQ--ftr} }{ \ded{Qimp--ftr} }}
\def\foooandorftr{    \foothreev { \ded{or--ftr}   }{ \ded{dbl--ftr}  }{ \ded{and--ftr}  }}
\def\foooexfaftr{     \footwov   { \ded{ex--ftr}   }{ \ded{fa--ftr}   }}
\def\foooexfaftr{     \foothreev { \ded{ex--ftr}   }{ \ded{wkn--ftr}   }{ \ded{fa--ftr}   }}
\def\foooeqftr{       \foothreev { \ded{=and--ftr}  }{ \ded{smash--ftr}  }{ \ded{=imp--ftr}  }}
\def\foooqeqftr{      \foothreev { \ded{ex=--ftr}  }{ \ded{ba--ftr}  }{ \ded{fa=--ftr}  }}

$$\begin{array}{cc}
  \cdiag{adj-cur-flsh}   & \foooandimpftr \\ \\
  \cdiag{adj-orand-flsh} & \foooandorftr \\ \\
  \cdiag{adj-exfa-flsh}  & \foooexfaftr  \\
  \end{array}
$$


\newpage
% --------------------
% «adj-functors-as-seq-rules-2»  (to ".adj-functors-as-seq-rules-2")
% (s "The adjunction functors as sequent rules (2)" "adj-functors-as-seq-rules-2")
\myslide {The adjunction functors as sequent rules (2)} {adj-functors-as-seq-rules-2}

$$\begin{array}{cc}
  \cdiag{adj-eq-flsh}    & \foooeqftr   \\\\
  \cdiag{adj-qeq-flsh}   & \foooqeqftr  \\
  \end{array}
$$



\newpage
% --------------------
% «adj-maps-as-seq-rules»  (to ".adj-maps-as-seq-rules")
% (s "The adjunction maps as sequent rules" "adj-maps-as-seq-rules")
\myslide {The adjunction maps as sequent rules} {adj-maps-as-seq-rules}

\def\Cur{¯{Cur}}
\def\sh{\sharp}
\def\fl{\flat}

%D diagram adj-cur-flsh
%D 2Dx      100     +30
%D 2D  100 P&Q <=== P
%D 2D	    -  <b|  -
%D 2D	    |       |
%D 2D	    v  |#>  v
%D 2D  +30  R ===> Q¶R
%D 2D
%D (( P&Q P R Q¶R
%D    @ 0 @ 1 <= @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D    @ 0 @ 3 harrownodes nil 20 nil <-| sl^ .plabel= a \flat
%D    @ 0 @ 3 harrownodes nil 20 nil |-> sl_ .plabel= b \sharp
%D ))
%D enddiagram

%D diagram adj-orand-flsh
%D 2Dx      100       +30
%D 2D  100 (P,Q) ==> PQ
%D 2D	     -   |b>  -
%D 2D	     |        |
%D 2D	     v   <#|  v
%D 2D  +30 (R,R) <=== R
%D 2D	     -   <b|  -
%D 2D	     |        |
%D 2D	     v   |#>  v
%D 2D  +30 (S,T) ==> S&T
%D 2D
%D (( (P,Q) PQ   (R,R) R   (S,T) S&T
%D    @ 0 @ 1 =>
%D    @ 0 @ 2 |-> @ 1 @ 3 |->
%D    @ 2 @ 3 <=
%D    @ 2 @ 4 |-> @ 3 @ 5 |->
%D    @ 4 @ 5 =>
%D    @ 0 @ 3 harrownodes nil 20 nil |-> sl^ .plabel= a \flat
%D    @ 0 @ 3 harrownodes nil 20 nil <-| sl_ .plabel= b \sharp
%D    @ 2 @ 5 harrownodes nil 20 nil <-| sl^ .plabel= a \flat
%D    @ 2 @ 5 harrownodes nil 20 nil |-> sl_ .plabel= b \sharp
%D ))
%D enddiagram

%D diagram adj-exfa-flsh
%D 2Dx     100        +30
%D 2D  100 Pab ===> Îb.Pab
%D 2D	    -   |b>   -
%D 2D	    |         |
%D 2D	    v   <#|   v
%D 2D  +30 Qa <====== Qa{}
%D 2D	    -   <b|   -
%D 2D	    |         |
%D 2D	    v   |#>   v
%D 2D  +30 Rab ===> ýb.Rab
%D 2D
%D 2D  +15 a,b |----> a
%D 2D
%D (( Pab Îb.Pab   Qa Qa{}   Rab ýb.Rab   a,b a
%D    @ 0 @ 1 =>
%D    @ 0 @ 2 |-> @ 1 @ 3 |->
%D    @ 2 @ 3 <=
%D    @ 2 @ 4 |-> @ 3 @ 5 |->
%D    @ 4 @ 5 =>
%D    @ 0 @ 3 harrownodes nil 20 nil |-> sl^ .plabel= a \flat
%D    @ 0 @ 3 harrownodes nil 20 nil <-| sl_ .plabel= b \sharp
%D    @ 2 @ 5 harrownodes nil 20 nil <-| sl^ .plabel= a \flat
%D    @ 2 @ 5 harrownodes nil 20 nil |-> sl_ .plabel= b \sharp
%D    @ 6 @ 7 |->
%D ))
%D enddiagram

%D diagram adj-eq-flsh
%D 2Dx     100        +40
%D 2D  100 Pab ==> b=b'&Pab
%D 2D	    -  |b>   -
%D 2D	    |        |
%D 2D	    v  <#|   v
%D 2D  +30 Qabb <== Qabb'
%D 2D	    -   <b|   -
%D 2D	    |         |
%D 2D	    v   |#>   v
%D 2D  +30 Rab ===> b=b'¶Rab
%D 2D
%D 2D  +15 a,b |--> a,b,b'
%D 2D
%D (( Pab b=b'&Pab   Qabb Qabb'   Rab b=b'¶Rab   a,b a,b,b'
%D    @ 0 @ 1 =>
%D    @ 0 @ 2 |-> @ 1 @ 3 |->
%D    @ 2 @ 3 <=
%D    @ 2 @ 4 |-> @ 3 @ 5 |->
%D    @ 4 @ 5 =>
%D    @ 0 @ 3 harrownodes nil 20 nil |-> sl^ .plabel= a \flat
%D    @ 0 @ 3 harrownodes nil 20 nil <-| sl_ .plabel= b \sharp
%D    @ 2 @ 5 harrownodes nil 20 nil <-| sl^ .plabel= a \flat
%D    @ 2 @ 5 harrownodes nil 20 nil |-> sl_ .plabel= b \sharp
%D    @ 6 @ 7 |->
%D ))
%D enddiagram

%D diagram adj-qeq-flsh
%D 2Dx     100        +40
%D 2D  100 Pa ==> Îa.b=fa&Pab
%D 2D	    -   |b>   -
%D 2D	    |         |
%D 2D	    v   <#|   v
%D 2D  +30 Qfa <==== Qb
%D 2D	    -   <b|   -
%D 2D	    |         |
%D 2D	    v   |#>   v
%D 2D  +30 Ra ===> ýa.b=fa¶Ra
%D 2D
%D 2D  +15 a |------> b
%D 2D
%D (( Pa Îa.b=fa&Pab   Qfa Qb   Ra ýa.b=fa¶Ra   a b
%D    @ 0 @ 1 =>
%D    @ 0 @ 2 |-> @ 1 @ 3 |->
%D    @ 2 @ 3 <=
%D    @ 2 @ 4 |-> @ 3 @ 5 |->
%D    @ 4 @ 5 =>
%D    @ 0 @ 3 harrownodes nil 20 nil |-> sl^ .plabel= a \flat
%D    @ 0 @ 3 harrownodes nil 20 nil <-| sl_ .plabel= b \sharp
%D    @ 2 @ 5 harrownodes nil 20 nil <-| sl^ .plabel= a \flat
%D    @ 2 @ 5 harrownodes nil 20 nil |-> sl_ .plabel= b \sharp
%D    @ 6 @ 7 |->
%D ))
%D enddiagram

%:                    P  [Q]^1                    P&Q
%:                    --------&I                  ---&E_1
%:   P&Q <=== P         P&Q            P&Q         P
%:    -  <b|  -         :::            ---&E_2     :
%:    |       |          R              Q         Q¶R       P&Q|-R          P|-Q¶R
%:    v  |#>  v        ---(¶I)          -------------¶E     ------\Cur^\sh  ------\Cur^\fl
%:    R ===> Q¶R       Q¶R                    R             P|-Q¶R          P&Q|-R
%:
%:                     ^cur-sh                ^cur-fl       ^cur--sh        ^cur--fl
%:
%:
%:  (P,Q) ==> PQ      [P]^1   [Q]^1     P         Q
%:    -   |b>  -         :       :      ---I_1   ---I_2
%:    |        |   PQ   R       R      PQ       PQ       P|-R  Q|-R       PQ|-R	   PQ|-R
%:    v   <#|  v   ---------------E     :         :        ----------^\fl  ------^\sh_1 ------^\sh_2
%:  (R,R) <=== R          R              R         R          PQ|-R          P|-R          Q|-R
%:
%:                        ^or-fl         ^or-sh1   ^or-sh2    ^or--fl         ^or--sh1      ^or--sh2
%:
%:  (R,R) <=== R        R   R            R        R
%:    -   <b|  -        :   :            :        :
%:    |        |        S   T           S&T      S&T       R|-S  R|-T       R|-S&T	   R|-S&T
%:    v   |#>  v        -----&I         ---&E_1  ---&E_2   ----------^\sh  ------^\fl_1  -----^\fl_2
%:  (S,T) ==> S&T        S&T             S        T          T|-S&T          R|-S          R|-T
%:
%:                       ^and-sh         ^and-fl1 ^and-fl2   ^and--sh        ^and--fl1     ^and--fl2
%:
%:  Pab ===> Îb.Pab         [Pab]^1          Pab
%:   -   |b>   -               :            ------ÎI
%:   |         |     Îb.Pab   Qa            Îb.Pab        Pab|-Qa            Îb.Pab|-Qa
%:   v   <#|   v     -----------ÎE            :          ----------Î^\fl     ----------Î^\sh
%:  Qa <====== Qa         Qa                  Qa         Îb.Pab|-Qa           Pab|-Qa
%:
%:  a,b|-----> a          ^ex-fl              ^ex-sh     ^ex--fl              ^ex--sh
%:
%:  Qa <====== Qa         [Qa]^1               Qa
%:   -   <b|   -             :                  :
%:   |         |      Qa    Rab            b  ýb.Rab      Qa|-Rab            Qa|-ýb.Rab
%:   v   |#>   v      ---------ýI          ---------ýE	 ----------ý^\sh     ----------ý^\fl
%:  Rab ===> ýb.Rab     ýb.Rab               Rab    	 Qa|-ýb.Rab           Qa|-Rab
%:
%:  a,b|-----> a        ^fa-sh               ^fa-fl      ^fa--sh              ^fa--fl
%:
%:  Pab ==> b=b'&Pab             b=b'&Pab             [b=b']^1  Pab
%:   -  |b>   -                  -------&E_2          ------------
%:   |        |       b=b'&Pab      Pab                 b=b'&Pab
%:   v  <#|   v       -------&E_1    :        ---=I       :
%:  Qbb <=== Qbb'       b=b'        Qabb       b=b        Qabb'         Pab|-Qabb         b=b'&Pab|-Qabb'
%:   -  <b|   -         ---------------=E     ---------------b':=b;1    ---------=&^\fl   ---------=&^\sh
%:   |        |               Qabb'                  Qabb               b=b'&Pab|-Qabb'   Pab|-Qabb
%:   v  |#>   v
%:  Rab ==> b=b'¶Rab          ^eq-fl                ^eq-sh              ^eq--fl           ^eq--sh
%:
%:  a,b |--> a,b,b'   [b=b']^1  Qabb'                          [Qabb']^1
%:		      ---------------?                            :
%:                        Qabb                        [b=b']^1  b=b'¶Rab
%:		           :             ---=I        ------------------¶E
%:  		          Rab            b=b    Qabb       Rab		    Qabb|-Rab        Qabb'|-b=b'¶Rab
%:  		       --------¶I;1      ---------------------b':=b;1	    ---------=¶^\sh  ---------=¶^\fl
%:  		       b=b'¶Rab                Rab			    Qabb'|-b=b'¶Rab  Qabb|-Rab
%:
%:  		       ^eqi-sh                 ^eqi-fl                      ^eqi--sh         ^eqi--fl
%:
%:  Pa ==> Îa.b=fa&Pab    Pa|-Qfa           Îa.b=fa&Pab|-Qb
%:   -    |b>   -         ---------Î=^\fl   ---------Î=^\sh
%:   |          |         Îa.b=fa&Pab|-Qb    Pa|-Qfa
%:   v    <#|   v
%:  Qfa <====== Qb        ^ex=--fl           ^ex=--sh
%:   -    <b|   -
%:   |          |         Qfa|-Ra          Qb|-ýa.b=fa¶Ra
%:   v    |#>   v         ---------=¶^\sh  ---------=¶^\fl
%:  Ra ===> ýa.b=fa¶Ra    Qb|-ýa.b=fa¶Ra   Qfa|-Ra
%:
%:  a |------> b          ^fa=--sh         ^fa=--fl

\def\foootwocur{    \footwo { \ded{cur--sh} }{ \ded{cur--fl} }}
\def\fooofourorand{ \fooFour{ \ded{or--fl}  }{ \ded{or--sh1}  \quad \ded{or--sh2}  }
                           { \ded{and--sh}  }{ \ded{and--fl1} \quad \ded{and--fl2} }}
\def\fooofourexfa{  \fooFour{ \ded{ex--fl}  }{ \ded{ex--sh} }
                           { \ded{fa--sh}   }{ \ded{fa--fl} }}
\def\fooofoureq{    \foofour{ \ded{eq--fl}  }{ \ded{eq--sh}  }
                           { \ded{eqi--sh}  }{ \ded{eqi--fl} }}
\def\fooofourqeq{   \foofour{ \ded{ex=--fl} }{ \ded{ex=--sh}  }
                            { \ded{fa=--sh} }{ \ded{fa=--fl} }}

\def\footwocur{    \footwo { \ded{cur-sh} }{ \ded{cur-fl} }}
\def\foofourorand{ \fooFour{ \ded{or-fl}  }{ \ded{or-sh1}  \quad \ded{or-sh2}  }
                           { \ded{and-sh} }{ \ded{and-fl1} \quad \ded{and-fl2} }}
\def\foofourexfa{  \fooFour{ \ded{ex-fl}  }{ \ded{ex-sh} }
                           { \ded{fa-sh}  }{ \ded{fa-fl} }}
\def\foofoureq{    \foofour{ \ded{eq-fl}  }{ \ded{eq-sh}  }
                           { \ded{eqi-sh} }{ \ded{eqi-fl} }}


$$\begin{array}{cc}
  \cdiag{adj-cur-flsh}   & \foootwocur    \\ \\
  \cdiag{adj-orand-flsh} & \fooofourorand \\ \\
  \cdiag{adj-exfa-flsh}  & \fooofourexfa \\
  \end{array}
$$


\newpage
% --------------------
% «adj-maps-as-seq-rules-2»  (to ".adj-maps-as-seq-rules-2")
% (s "The adjunction maps as sequent rules (2)" "adj-maps-as-seq-rules-2")
\myslide {The adjunction maps as sequent rules (2)} {adj-maps-as-seq-rules-2}

$$\begin{array}{cc}
  \cdiag{adj-eq-flsh}   & \fooofoureq    \\ \\
  \cdiag{adj-qeq-flsh}  & \fooofourqeq   \\
  \end{array}
$$



\newpage
% --------------------
% «adj-functors-as-ND-proofs»  (to ".adj-functors-as-ND-proofs")
% (s "The adjunction functors as ND proofs" "adj-functors-as-ND-proofs")
\myslide {The adjunction functors as ND proofs} {adj-functors-as-ND-proofs}

%:                       [Q]^1  Q¶R             P&Q
%:                       ----------¶E           ---&E_1
%:   P&Q <=== P               R                  P       P&Q
%:    -  <b|  -               :                  :       ---&E_2
%:    |       |               R'                 P'       Q
%:    v  |#>  v              ----¶I;1            ----------&I
%:    R ===> Q¶R             Q¶R'                  P'&Q
%:
%:                           ^Qimp-ftr             ^andQ-ftr
%:
%:  (P,Q) ==> PQ           [P]^1     [Q]^1      S&T      S&T
%:    -   |b>  -             :         :         ---&E_1  ---&E_2
%:    |        |             P'        Q'         S        T
%:    v   <#|  v           -----I_1  ----I_2    :        :
%:  (R,R) <=== R     PQ   P'Q'      P'Q'       S'       T'
%:    -   <b|  -     ---------------------E      -----------&I
%:    |        |          P'Q'                     S'&T'
%:    v   |#>  v
%:  (S,T) ==> S&T         ^or-ftr                   ^and-ftr
%:
%:  Pab ===> Îb.Pab
%:   -   |b>   -                 [Pab]^1        [b]^1  ýb.Rab
%:   |         |                   :            -------------ýE
%:   v   <#|   v                 P'ab               Rab
%:  Qa <====== Qa               -------ÎI            :
%:   -   <b|   -       Îb.Pab   Îb.P'ab            R'ab
%:   |         |       ----------------ÎE         -------ýI;1
%:   v   |#>   v           Îb.P'ab                ýb.R'ab
%:  Rab ===> ýb.Rab
%:                         ^ex-ftr                ^fa-ftr
%:  a,b|-----> a
%:

\def\footwocurftr{   \footwo { \ded{andQ-ftr} }{ \ded{Qimp-ftr} }}
\def\footwoorandftr{ \footwo { \ded{or-ftr}   }{ \ded{and-ftr}  }}
\def\footwoexfaftr{  \footwo { \ded{ex-ftr}   }{ \ded{fa-ftr}  }}

$$\begin{array}{cc}
  \cdiag{adj-cur-flsh}   & \footwocurftr   \\ \\
  \cdiag{adj-orand-flsh} & \footwoorandftr \\ \\
  \cdiag{adj-exfa-flsh}  & \footwoexfaftr  \\
% \cdiag{adj-eq-flsh}    & \footwoeqftr  \\
  \end{array}
$$

\newpage
% --------------------
% «adj-functors-as-ND-proofs-2»  (to ".adj-functors-as-ND-proofs-2")
% (s "The adjunction functors as ND proofs (2)" "adj-functors-as-ND-proofs-2")
\myslide {The adjunction functors as ND proofs (2)} {adj-functors-as-ND-proofs-2}

%:                                   b=b'&Pab
%:                                   -------&E_2
%:                       b=b'&Pab       Pab               [Qabb']^1
%:                       -------&E_1    :                   :
%:                         b=b'        P'ab         Qabb  Q'abb'
%:                         ---------------?        ----------b':=b
%:  Pab ==> b=b'&Pab           b=b'&P'ab               Q'abb
%:   -  |b>   -
%:   |        |                ^=and-ftr               ^smash-ftr
%:   v  <#|   v
%:  Qabb <== Qabb'       [b=b']^1  b=b'¶Rab
%:   -  <b|   -          ------------------¶E
%:   |        |                Rab
%:   v  |#>   v                 :
%:  Rab ===> b=b'¶Rab         R'ab
%:                          --------¶I;1
%:  a,b |--> a,b,b'         b=b'¶Rab
%:
%:                          ^=imp-ftr
%:
%:                                      [fa=b&Pa]^1                ýa.fa=b¶Ra
%:                                      -----------&E_2            ----------
%:  Pa ==> Îa.b=fa&Pab     [fa=b&Pa]^1      Pa           [fa=b]^1   fa=b¶Ra
%:   -    |b>   -          -----------&E_1   :           ------------------
%:   |          |             fa=b          P'a                Ra
%:   v    <#|   v             -----------------&I               :
%:  Qfa <====== Qb                     fa=b&P'a                R'a
%:   -    <b|   -                      -----------ÎI        --------1
%:   |          |         Îa.fa=b&Pa   Îa.fa=b&P'a          fa=b¶R'a
%:   v    |#>   v         ------------------------ÎE;1    -----------
%:  Ra ===> ýa.b=fa¶Ra         Îa.fa=b&P'a                ýa.fa=b¶R'a
%:
%:  a |------> b               ^ex=-ftr                   ^fa=-ftr
%:

\def\footwoeqftr{    \footwo { \ded{=and-ftr} }{ \ded{=imp-ftr}  }}
\def\footwoveqftr{  \footwov { \ded{=and-ftr} }{ \ded{=imp-ftr}  }}
\def\foofoureqftr{  \foofour { \ded{=and-ftr} }{ \ded{smash-ftr} }
                             { \ded{=imp-ftr} }{                 }}
\def\footwovqeqftr{ \footwov { \ded{ex=-ftr}  }{ \ded{fa=-ftr}   }}


$$\begin{array}{cc}
  \cdiag{adj-eq-flsh}    & \footwoveqftr   \\ \\
  \cdiag{adj-qeq-flsh}   & \footwovqeqftr  \\
  \end{array}
$$







\newpage
% --------------------
% «adj-maps-as-ND-proofs»  (to ".adj-maps-as-ND-proofs")
% (s "The adjunction maps as ND proofs" "adj-maps-as-ND-proofs")
\myslide {The adjunction maps as ND proofs} {adj-maps-as-ND-proofs}

$$\begin{array}{cc}
  \cdiag{adj-cur-flsh}   & \footwocur    \\ \\
  \cdiag{adj-orand-flsh} & \foofourorand \\ \\
  \cdiag{adj-exfa-flsh}  & \foofourexfa \\
  \end{array}
$$


\newpage
% --------------------
% «adj-maps-as-ND-proofs-2»  (to ".adj-maps-as-ND-proofs-2")
% (s "The adjunction maps as ND proofs (2)" "adj-maps-as-ND-proofs-2")
\myslide {The adjunction maps as ND proofs (2)} {adj-maps-as-ND-proofs-2}

\msk

$\diag{adj-eq-flsh}$

$$\foofoureq$$


\newpage
% --------------------
% «adj-maps-as-ND-proofs-3»  (to ".adj-maps-as-ND-proofs-3")
% (s "The adjunction maps as ND proofs (3)" "adj-maps-as-ND-proofs-3")
\myslide {The adjunction maps as ND proofs (3)} {adj-maps-as-ND-proofs-3}

\msk

$\diag{adj-qeq-flsh}$

%:
%:                                                  [b=fa]^1   Pa
%:                                                  -------------
%:                        [b=fa&Pa]^1                  b=fa&Pa
%:                        -----------                ----------
%:           [b=fa&Pa]^1      Pa                     Îa.b=fa&Pa
%:           -----------      ::                         ::
%:              b=fa         Qfa              [b=fa]^1   Qb
%:              ----------------      -----   -------------
%:  Îa.b=fa&Pa            Qb          fa=fa        Qfa
%:  ------------------------1         ----------------
%:             Qb                          Qfa
%:
%:             ^gen-exand-sharp            ^gen-exand-flat
%:
%:                                      [Qb]^1
%:                                        ::
%:    [fa=b]^1   Qb         [Qfa']^2   ýa.fa=b¶Ra
%:    -------------         ---------------------1
%:        Qfa                     ýa.fa=fa'¶Ra
%:        ::                      ------------
%:        Ra                 Qfa     fa=fa¶Ra
%:     -------1       -----  ----------------2
%:     fa=b¶Ra        fa=fa     fa=fa¶Ra
%:   ----------       ------------------
%:   ýa.fa=b¶Ra              Ra
%:
%:   ^gen-eximp-flat         ^gen-eximp-sharp
%:
$$\ded{gen-exand-sharp} \quad \ded{gen-exand-flat}$$
$$\ded{gen-eximp-flat} \qquad \ded{gen-eximp-sharp}$$


\newpage
% --------------------
% «frob-maps-as-ND-proofs»  (to ".frob-maps-as-ND-proofs")
% (s "The Frobenius maps as ND proofs" "frob-maps-as-ND-proofs")
\myslide {The Frobenius maps as ND proofs} {frob-maps-as-ND-proofs}

The preservations of $§, ®, \&, , ¶$ are all

trivially true intuitionistically, as they are all

of the form $\aa \vdash \aa$...

\msk

Same for Beck-Chevalley.

\msk

The $î$ arrows whose inverses are the Frobenius maps

can be constructed from operations whose translations

to Intuitionistic Logic we have already seen.

%D diagram frob-maps
%D 2Dx     100        +80       +30        +50
%D 2D  100 AL <=====> AR    al <=====> ar   
%D 2D                                       
%D 2D  +20 al <=====> ar    al <=====> ar   
%D 2D                                       
%D 2D  +30 BL <=====> BR    bl <=====> br
%D 2D                                       
%D 2D  +20 bl <=====> br    bl <=====> br
%D 2D                                       
%D 2D  +30 CL <=====> CR    cl <=====> cr
%D 2D
%D 2D  +20 cl <=====> cr    cl <=====> cr
%D 2D
%D (( AL .tex= Î_(P&^*Q)      AR .tex= (Î_P)&Q
%D    al .tex= Îb.(Pab&Qa)      ar .tex= (Îb.Pab)&Qa
%D    @ 0 @ 1  -> sl^ .plabel= a î  @ 0 @ 1 <-  sl_ .plabel= b Ð{Frob}Î
%D    @ 2 @ 3 |-> sl^ .plabel= a î  @ 2 @ 3 <-| sl_ .plabel= b Ð{Frob}Î
%D ))
%D (( BL .tex= \Eq_(P&^*Q)    BR .tex= (\Eq_P)&Q
%D    bl .tex= b=b'&(Pabb&Qab)  br .tex= (b=b'&Pabb)&Qab
%D    @ 0 @ 1  -> sl^ .plabel= a î  @ 0 @ 1 <-  sl_ .plabel= b Ð{Frob}=
%D    @ 2 @ 3 |-> sl^ .plabel= a î  @ 2 @ 3 <-| sl_ .plabel= b Ð{Frob}=
%D ))
%D (( CL .tex= \ExEq_f(P&f^*Q)  CR .tex= (\ExEq_fP)&Q
%D    cl .tex= Îa.b=fa&(Pa&Qfa) cr .tex= (Îa.b=fa&Pa)&Qb
%D    @ 0 @ 1  -> sl^ .plabel= a î  @ 0 @ 1 <-  sl_ .plabel= b Ð{Frob}Î=
%D    @ 2 @ 3 |-> sl^ .plabel= a î  @ 2 @ 3 <-| sl_ .plabel= b Ð{Frob}Î=
%D ))
%D enddiagram
%D
$$\diag{frob-maps}$$

\msk

We need to show that the Frobenius maps

``hold intuitionistically''.

\msk

Here is a ND proof for the first case:

(the other cases are similar - and the trees are big)

%:                           (Îb.Pab)&Qa
%:                           -----------&E_2
%:                  [Pab]^1      Qa
%:                  ---------------&I
%:  (Îb.Pab)&Qa            Pab&Qa
%:  -----------&E_1      -----------ÎI
%:    Îb.Pab             Îb.(Pab&Qa)
%:    ------------------------------ÎE;1
%:             Îb.(Pab&Qa)
%:
%:             ^frob-ex-ND
%:
$$\ded{frob-ex-ND}$$




\newpage
% --------------------
% «frob-for-equality-2»  (to ".frob-for-equality-2")
% (s "Frobenius for equality (2)" "frob-for-equality-2")
\myslide {Frobenius for equality (2)} {frob-for-equality-2}

(Now we will start to see consequences of the structure)

\msk

If we have $\Eq§$ and Frobenius, then we have $\Eq P$:

%D diagram EqTP-std
%D 2Dx     100     +50 +30 +30    +50
%D 2D  100 a ============> b
%D 2D      ^           --> ^
%D 2D      |          /    |
%D 2D      -         -     -
%D 2D  +20 c ====> d <===> e
%D 2D      ^       ^ -     -
%D 2D      |       |  \    |
%D 2D      v       |   --> v
%D 2D  +20 f <=====|====== g <=== h
%D 2D      ^ \\    |
%D 2D      |  \\   |
%D 2D      |   \\  v
%D 2D  +20 |    \> i
%D 2D      |       ^
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 j ====> k
%D 2D
%D 2D  +20 a,b |---> a,b,b' |--> a,b{}
%D 2D
%D (( a .tex= §          b .tex= \Eq§
%D    c .tex= §&^*^*P  d .tex= \Eq(§&^*^*P)   e .tex= \Eq§&^*P
%D    f .tex= ^*^*P                             g .tex= ^*P       h .tex= P
%D                       i .tex= \Eq(^*^*P)
%D    j .tex= P          k .tex= \Eq"P
%D    a,b .tex= A×B   a,b,b' .tex= A×B×B  a,b{} .tex= A×B
%D ))
%D (( a .tex= 1_X                                       b .tex= 1_XÆ\ang{X,f}
%D    c .tex= \phi'´1_X  d .tex= (\phi'´1_X)Æ\phi'´1_X  e .tex= _X·\phi´1_XÆ\ang{X,f}
%D    f .tex= \phi'                                     g .tex= _X·\phi   h .tex= \phi
%D                       i .tex= \phi'Æ\ang{X,f}
%D    j .tex= \phi       k .tex= \phiÆ\ang{X,f}
%D    a,b .tex= X  a,b,b' .tex= X×Y  a,b{} .tex= X
%D ))
%D (( a b |->   c a -> d b -> e b ->
%D    c d |->   d e -> sl^ .plabel= a î   d e <- sl_ .plabel= b Ð{Frob}
%D    c f <->   d i <-> d g -> e g -> 
%D    f g <-|   g h <-|
%D    f j <-> f i |->  i k <-> j k |->
%D ))
%D (( a,b a,b,b' -> .plabel= a    a,b,b' a,b{} -> .plabel= a 
%D ))
%D enddiagram

%D diagram EqTP-lawvere67
%D 2Dx     100     +50 +35 +35    +50
%D 2D  100 a ============> b
%D 2D      ^           --> ^
%D 2D      |          /    |
%D 2D      -         -     -
%D 2D  +20 c ====> d <===> e
%D 2D      ^       ^ -     -
%D 2D      |       |  \    |
%D 2D      v       |   --> v
%D 2D  +20 f <=====|====== g <=== h
%D 2D      ^ \\    |
%D 2D      |  \\   |
%D 2D      |   \\  v
%D 2D  +20 |    \> i
%D 2D      |       ^
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 j ====> k
%D 2D
%D 2D  +20 a,b |---> a,b,b' |--> a,b{}
%D 2D
%D (( a .tex= 1_X                                       b .tex= 1_XÆ\ang{X,f}
%D    c .tex= \phi'´1_X  d .tex= (\phi'´1_X)Æ\phi'´1_X  e .tex= _X·\phi´1_XÆ\ang{X,f}
%D    f .tex= \phi'                                     g .tex= _X·\phi   h .tex= \phi
%D                       i .tex= \phi'Æ\ang{X,f}
%D    j .tex= \phi       k .tex= \phiÆ\ang{X,f}
%D    a,b .tex= X  a,b,b' .tex= X×Y  a,b{} .tex= X
%D ))
%D (( a b |->   c a -> d b -> e b ->
%D    c d |->   d e -> sl^ .plabel= a î   d e <- sl_ .plabel= b Ð{Frob}
%D    c f <->   d i <-> d g -> e g -> 
%D    f g <-|   g h <-|
%D    f j <-> f i |->  i k <-> j k |->
%D ))
%D (( a,b a,b,b' -> .plabel= a \ang{X,f}   a,b,b' a,b{} -> .plabel= a _X
%D ))
%D enddiagram

%D diagram EqTP-dnc
%D 2Dx     100     +50 +30 +30    +50
%D 2D  100 a ============> b
%D 2D      ^           --> ^
%D 2D      |          /    |
%D 2D      -         -     -
%D 2D  +20 c ====> d <===> e
%D 2D      ^       ^ -     -
%D 2D      |       |  \    |
%D 2D      v       |   --> v
%D 2D  +20 f <=====|====== g <=== h
%D 2D      ^ \\    |
%D 2D      |  \\   |
%D 2D      |   \\  v
%D 2D  +20 |    \> i
%D 2D      |       ^
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 j ====> k
%D 2D
%D 2D  +20 a,b |---> a,b,b' |--> a,b{}
%D (( a .tex= §     b .tex= b=b'&§
%D    c .tex= §&P   d .tex= b=b'&(§&P)   e .tex= (b=b'&§)&P
%D    f .tex= P                          g .tex= P          h .tex= P
%D                  i .tex= b=b'&P
%D    j .tex= P     k .tex= b=b'&P
%D ))
%D (( a b =>   c a |-> d b |-> e b |->
%D    c d =>   d e |-> sl^ .plabel= a î   d e <-| sl_ .plabel= b Ð{Frob}
%D    c f <->  d i <-> d g |-> e g |-> 
%D    f g <=   g h <=
%D    f j <-> f i =>  i k <-> j k =>
%D ))
%D (( a,b a,b,b' |->  a,b,b' a,b{} |->
%D ))
%D enddiagram

% $$\diag{EqTP-std}$$

$$\diag{EqTP-lawvere67}$$

$$\diag{EqTP-dnc}$$

\bsk

From now on we will usually write ``$b{=}b'\&§$'' as just ``$b{=}b'$''.

Frobenius for equality implies that the four obvious definitions

for $b{=}b'\&P$ are isomorphic.



\newpage
% --------------------
% «dep-eq-from-simple-eq»  (to ".dep-eq-from-simple-eq")
% (s "Dependent equality from simple equality" "dep-eq-from-simple-eq")
\myslide {Dependent equality from simple equality} {dep-eq-from-simple-eq}


%D diagram bcc-dep-T-std
%D 2Dx    100     +45                +55   +45
%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= _2^*§         B1 .tex= §
%D    B2 .tex= ^*_{23}^*\Eq§  B2' .tex= _2^*^*\Eq§   B3 .tex= ^*\Eq§
%D    B4 .tex= \Eq_{'}§_{A×B}                           B5 .tex= \Eq§
%D    B6 .tex= _{23}^*\Eq_{}§_B                        B7 .tex= \Eq§
%D    B0 B0' <- sl^ .plabel= a î B0 B0' -> sl_ .plabel= b Ð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 <-| B5 B7 -> .plabel= r \id
%D    B4 B6 -> sl_ .plabel= l î B4 B6 <- sl^ .plabel= r Ð{BCC}Î
%D    B0' B2' midpoint B1 B3 midpoint  harrownodes nil 20 nil <-|
%D    B0  B2  midpoint B4 B6 midpoint dharrownodes nil 16 nil |->
%D    B1  B3  midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= A×B b1 .tex= B b2 .tex= A×B×B b3 .tex= B×B
%D    b0 b1 -> .plabel= b _2
%D    b0 b2 -> .plabel= l '
%D    b1 b3 -> .plabel= r 
%D    b2 b3 -> .plabel= b _{23}
%D    b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-dep-T-std}$$

%D diagram bcc-dep-T-dnc
%D 2Dx    100     +45                +55   +45
%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= §     B1 .tex= §
%D    B2 .tex= b=b  B2' .tex= b=b   B3 .tex= b=b 
%D    B4 .tex= b=b'                 B5 .tex= b=b'
%D    B6 .tex= b=b'                 B7 .tex= b=b'
%D    B0 B0' <-| sl^ .plabel= a î B0 B0' |-> sl_ .plabel= b Ð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 <= B5 B7 |-> .plabel= r \id
%D    B4 B6 |-> sl_ .plabel= l î B4 B6 <-| sl^ .plabel= r Ð{BCC}Î
%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,b b1 .tex= b b2 .tex= a,b,b' b3 .tex= b,b'
%D    b0 b1 |-> b0 b2 |-> b1 b3 |-> b2 b3 |->
%D    b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-dep-T-dnc}$$






\newpage
% --------------------
% «eq-is-transitive»  (to ".eq-is-transitive")
% (s "Transitivity of equality" "eq-is-transitive")
\myslide {Transitivity of equality} {eq-is-transitive}

%D diagram eqtransitivity-1
%D 2Dx     100    +40    +25    +40       +20    +35    +20    +35  
%D 2D  100 A0			       a0			     
%D 2D       - ==>		        - ==>		     
%D 2D  +20  |     A1		        |     a1		     
%D 2D       |      -		        |      -		     
%D 2D       v      |		        v      |		     
%D 2D  +20 A4      |     A6	       a4      |     a6	     
%D 2D         <=== v        ==>	          <=== v        ==>	     
%D 2D  +20        A5 <========= A7            a5 <========= a7   
%D 2D                                                            
%D 2D  +15 B4            B6	       b4            b6	     
%D 2D         |->           |->	          |->           |->	     
%D 2D  +20        B5 |--------> B7            b5 |--------> b7   
%D 2D                                                                
%D 2D  +20 a0                            
%D 2D       - ==>                
%D 2D  +20  |     a1                     
%D 2D       |      -                     
%D 2D       v      |                     
%D 2D  +20 a4      |     a6      
%D 2D         <=== v        ==>          
%D 2D  +20        a5 <========= a7   
%D 2D                                
%D 2D  +15 b4            b6      
%D 2D         |->           |->          
%D 2D  +20        b5 |--------> b7   
%D 2D                                                                
%D (( A0 .tex= '^*_{24}^*\Eq_§   A1 .tex= \Eq_{'}'^*_{24}^*\Eq_§
%D    A4 .tex= '^*_{24}^*\Eq_§   A5 .tex= _{24}^*\Eq_§
%D    A6 .tex= §       A7 .tex= \Eq_§
%D    A0 A1 |-> A0 A4 -> .plabel= l \id A1 A5 -> A4 A5 <-| A6 A7 |-> A5 A7 <-|
%D    A0 A4 midpoint A1 A5 midpoint dharrownodes nil 20 nil |->
%D ))
%D (( B4 .tex= (A×B)×B   B5 .tex= ((A×B)×B)×B
%D    B6 .tex= A×B       B7 .tex= (A×B)×B
%D    B4 B5 -> .PLABEL= _(0.35) '
%D    B6 B7 -> .PLABEL= ^(0.5)  
%D    B5 B7 -> .plabel= b     _{24}
%D ))
%D (( a0 .tex= b=b'    a1 .tex= b'=b''&b=b'
%D    a4 .tex= b=b'    a5 .tex=     b=b''
%D    a6 .tex= §       a7 .tex= b=b''
%D    a0 a1 => a0 a4 |-> .plabel= l \id a1 a5 |-> a4 a5 <= a6 a7 => a5 a7 <=
%D    a0 a4 midpoint a1 a5 midpoint dharrownodes nil 20 nil |->
%D ))
%D (( b4 .tex= (a,b),b'   b5 .tex= ((a,b),b'),b''
%D    b6 .tex= a,b        b7 .tex= (a,b),b''
%D    b4 b5 |-> .PLABEL= _(0.35) b'':=b'\phantom{,}
%D    b6 b7 |-> .PLABEL= ^(0.5) b'':=b
%D    b5 b7 |->
%D ))
%D enddiagram
%D

\msk

$\diag{eqtransitivity-1}$



\newpage
% --------------------
% «hyp-subst-quant-refl»  (to ".hyp-subst-quant-refl")
% (s "Hyperdoctrines: substitution, quantifiers, reflexivity" "hyp-subst-quant-refl")
\myslide {Hyperdoctrines: substitution, quantifiers, reflexivity} {hyp-subst-quant-refl}

%D diagram Hyp-subst
%D 2Dx         100             +50
%D 2Dx             +12             +12
%D 2D  100     P <============ P{}
%D 2D	       -               -
%D 2D          |      <-|      |
%D 2D	       v               v
%D 2D  +30     Q <============ Q{}
%D 2D
%D 2D  +20    a,c |---------> b,c
%D 2D   +5       /\              /\
%D 2D	         ||              ||
%D 2D  +10         a |-----------> b
%D 2D
%D (( P .tex= \s[a,c|P] P{} .tex= \s[b,c|P]
%D    Q .tex= \s[b,c|Q] Q{} .tex= \s[b,c|Q]
%D    @ 0 @ 1 <= sl_  @ 0 @ 1 |-> sl^ .plabel= a {ñ}
%D    @ 0 @ 2 |-> .plabel= l a,c;P|-Q
%D    @ 1 @ 3 |-> .plabel= r b,c;P|-Q
%D    @ 0 @ 3 harrownodes nil 20 nil <-|
%D    @ 2 @ 3 <= sl_  @ 2 @ 3 |-> sl^ .plabel= a {ñ}
%D
%D ))
%D (( a,c b,c  a b
%D    @ 0 @ 1 |-> # .plabel= a b:=b[a]
%D    @ 0 @ 2 <= @ 1 @ 3 <=
%D    @ 2 @ 3 |-> .plabel= b a|-b
%D ))
%D enddiagram

%D diagram Hyp-FaI
%D 2Dx         100             +40
%D 2Dx             +10             +10
%D 2D  100     P <============ P{}
%D 2D	       -               -
%D 2D          |      |->      |
%D 2D	       v               v
%D 2D  +30     Q ============> ýb.Q
%D 2D
%D 2D  +20    a,b |----------> a
%D 2D
%D (( P .tex= \s[a,c|P] P{} .tex= \s[b,c|P]
%D    Q .tex= \s[b,c|Q] ýb.Q .tex= \s[b,c|ýb.Q]
%D    @ 0 @ 1 <= sl_ @ 0 @ 1 |-> sl^ .plabel= a {ñ}
%D    @ 0 @ 2 |-> .plabel= l a,b;P|-Q
%D    @ 1 @ 3 |-> .plabel= r a;P|-ýb.Q
%D    @ 0 @ 3 harrownodes nil 20 nil |->
%D    @ 2 @ 3 =>
%D ))
%D (( a,b a
%D    @ 0 @ 1 |->
%D ))
%D enddiagram

%D diagram Hyp-FaE
%D 2Dx            100            +40          +40
%D 2D  100       {}Q <========== Q <======== Q{}
%D 2D	           -             -            -
%D 2D	           |    <-|      |     <-|    |
%D 2D	           v             v            v
%D 2D  +30       {}R <========== R ========> ýb.R
%D 2D
%D 2D  +20       {}a |--------> a,b |-------> a{}
%D 2D
%D (( {}Q .tex= \s[a|P]   Q .tex= \s[a,b|P]   Q{}  .tex= \s[a|P]
%D    {}R .tex= \s[a|Q]   R .tex= \s[a,b|Q]   ýb.R .tex= \s[a|ýb.Q]
%D    @ 0 @ 1 <= sl_  @ 0 @ 1 |-> sl^ .plabel= a {ñ}
%D    @ 1 @ 2 <= sl_  @ 1 @ 2 |-> sl^ .plabel= a {ñ}
%D    @ 0 @ 3 |-> .plabel= l a;Q|-R
%D    @ 1 @ 4 |->
%D    @ 2 @ 5 |-> .plabel= r a;Q|-ýb.R
%D    @ 0 @ 4 harrownodes nil 20 nil <-|
%D    @ 1 @ 5 harrownodes nil 20 nil <-|
%D    @ 3 @ 4 <= sl_  @ 3 @ 4 |-> sl^ .plabel= a {ñ}
%D    @ 4 @ 5 =>
%D ))
%D (( {}a a,b |-> .plabel= a a|-b
%D    a,b a{} |->
%D ))
%D enddiagram

%D diagram Hyp-ExE
%D 2Dx         100             +40
%D 2Dx             +10             +10
%D 2D  100     P ============> Îb.P
%D 2D	       -               -
%D 2D          |      |->      |
%D 2D	       v               v
%D 2D  +30     Q <============ Q{}
%D 2D
%D 2D  +20    a,b |----------> a
%D 2D
%D (( P .tex= \s[a,b|P] Îb.P .tex= \s[a|Îb.P]
%D    Q .tex= \s[b,c|Q] Q{} .tex= \s[a,b|Q]
%D    @ 0 @ 1 => sl_  @ 0 @ 1 |-> sl^ .plabel= a \co{ñ}
%D    @ 0 @ 2 |-> .plabel= l a,b;P|-Q
%D    @ 1 @ 3 |-> .plabel= r a;Îb.P|-Q
%D    @ 0 @ 3 harrownodes nil 20 nil |->
%D    @ 2 @ 3 <= sl_  @ 2 @ 3 |-> sl^ .plabel= a {ñ}
%D ))
%D (( a,b a
%D    @ 0 @ 1 |->
%D ))
%D enddiagram

%D diagram Hyp-ExI
%D 2Dx            100            +40          +40
%D 2D  100       {}P <========== P =======> {Îb.P}
%D 2D	           -             -            -
%D 2D	           |    <-|      |     <-|    | id
%D 2D	           v             v            v
%D 2D  +30      {}Îb.P <====== Îb.P <====== Îb.P{}
%D 2D
%D 2D  +20       {}a |--------> a,b |-------> a{}
%D 2D
%D (( {}P    .tex= \s[a|P]       P .tex= \s[a,b|P]     {Îb.P} .tex= \s[a|Îb.P]
%D    {}Îb.P .tex= \s[a|Îb.P] Îb.P .tex= \s[a,b|Îb.P]  Îb.P{} .tex= \s[a|Îb.P]
%D    @ 0 @ 1 <= sl_  @ 0 @ 1 |-> sl^ .plabel= a {ñ}
%D    @ 1 @ 2 => sl_  @ 1 @ 2 |-> sl^ .plabel= a \co{ñ}
%D    @ 0 @ 3 |-> .plabel= l a;P|-Îb.P
%D    @ 1 @ 4 |->
%D    @ 2 @ 5 |-> .plabel= r \id
%D    @ 0 @ 4 harrownodes nil 20 nil <-|
%D    @ 1 @ 5 harrownodes nil 20 nil <-|
%D    @ 3 @ 4 <= sl_  @ 3 @ 4 |-> sl^ .plabel= a {ñ}
%D    @ 4 @ 5 <= sl_  @ 4 @ 5 |-> sl^ .plabel= a {ñ}
%D ))
%D (( {}a a,b |-> .plabel= a a|-b
%D    a,b a{} |->
%D ))
%D enddiagram




The substitution rule:

\msk

$\diag{Hyp-subst}$

\bsk

The `($ý$I)' and `($ý$E)' rules:

\msk

$\diag{Hyp-FaI} \qquad \diag{Hyp-FaE}$

\bsk

The `($Î$E)' and `($Î$I)' rules:

\msk

$\diag{Hyp-ExE} \qquad \diag{Hyp-ExI}$

\bsk

%D diagram Hyp-eq-refl
%D 2Dx     100        +45
%D 2D  100 e0 ======> e1
%D 2D       -         -
%D 2D  refl |   <-|   | id
%D 2D       v         v
%D 2D  +35 e2 <====== e3
%D 2D
%D 2D  +20 b0 |-----> b1
%D 2D
%D (( e0 .tex= \s[a,b|§]      e1 .tex= \s[a,b,b'|b{=}b']
%D    e2 .tex= \s[a,b|b{=}b]  e3 .tex= \s[a,b,b'|b{=}b']
%D    b0 .tex= a,b   b1 .tex= a,b,b'
%D    e0 e1 => sl_  e0 e1 <-| sl^ .plabel= a \co{ñ}
%D    e0 e2 |-> .plabel= l a,b;§|-(b{=}b)           # \text{refl}
%D    e1 e3 |-> .plabel= r \text{id}
%D    e0 e3 harrownodes nil 20 nil <-|
%D    e2 e3 <= sl_  e2 e3 |-> sl^ .plabel= a {ñ}
%D    b0 b1 |-> .plabel= a b':=b
%D ))
%D enddiagram

The ``reflexivity'' rule for equality (on variables):

\msk

$\diag{Hyp-eq-refl}$



\newpage
% --------------------
% «hyp-sym-trans»  (to ".hyp-sym-trans")
% (s "Hyperdoctrines: symmetry, transitivity" "hyp-sym-trans")
\myslide {Hyperdoctrines: symmetry, transitivity} {hyp-sym-trans}

%D diagram Hyp-eq-sym
%D 2Dx     100   +30  +30   +30
%D 2D  100 e0 ======> e1
%D 2D       -         -
%D 2D  refl |   |->   | sym
%D 2D       v         v
%D 2D  +35 e2 <====== e3
%D 2D                   /\
%D 2D                    \\
%D 2D                     \\
%D 2D  +35       e4 ======> e5
%D 2D
%D 2D  +21 b2 |-----> b3
%D 2D                   /
%D 2D                    \
%D 2D                     v
%D 2D  +35       b4 |-----> b5
%D 2D
%D (( e0 .tex= \s[a,b|§]      e1 .tex= \s[a,b,b'|b{=}b']
%D    e2 .tex= \s[a,b|b{=}b]  e3 .tex= \s[a,b,b'|b'{=}b]
%D    e4 .tex= \s[a,b'|§]     e5 .tex= \s[a,b',b|b'{=}b]
%D    b2 .tex= a,b   b3 .tex= a,b,b'
%D    b4 .tex= a,b'  b5 .tex= a,b',b
%D    e0 e1 => sl_  e0 e1 |-> sl^ .plabel= a \co{ñ}
%D    e0 e2 |-> .plabel= l \text{refl}
%D    e1 e3 |-> .plabel= r a,b,b';(b{=}b')|-(b'{=}b)      # \text{sym}
%D    e0 e3 harrownodes nil 20 nil |->
%D    e2 e3 <= sl_  e2 e3 |-> sl^ .plabel= a {ñ}
%D    e3 e5 <= sl_  e3 e5 |-> sl^ .plabel= a {ñ}
%D    e4 e5 => sl_  e4 e5 |-> sl^ .plabel= a \co{ñ}
%D    b2 b3 |-> .plabel= a b':=b
%D    b3 b5 |->
%D    b4 b5 |-> .plabel= a b':=b
%D ))
%D enddiagram

%D diagram Hyp-eq-trans
%D 2Dx     100   +30  +30   +30
%D 2D  100 e0 ======> e1
%D 2D       -         -
%D 2D    id |   |->   | trans
%D 2D       v         v
%D 2D  +35 e2 <====== e3
%D 2D                   /\
%D 2D                    \\
%D 2D                     \\
%D 2D  +35       e4 ======> e5
%D 2D
%D 2D  +21 b2 |-----> b3
%D 2D                   /
%D 2D                    \
%D 2D                     v
%D 2D  +35       b4 |-----> b5
%D 2D
%D (( e0 .tex= \s[a,b,b'|b{=}b']  e1 .tex= \s[a,b,b',b''|b'{=}b''&b{=}b']
%D    e2 .tex= \s[a,b,b'|b{=}b']  e3 .tex= \s[a,b,b',b''|b{=}b'']
%D    e4 .tex= \s[a,b|§]          e5 .tex= \s[a,b',b''|b{=}b'']
%D    b2 .tex= a,b,b'   b3 .tex= a,b,b',b''
%D    b4 .tex= a,b      b5 .tex= a,b',b''
%D    e0 e1 => sl_  e0 e1 |-> sl^ .plabel= a \co{ñ}
%D    e0 e2 |-> .plabel= l \text{id}
%D    e1 e3 |-> .plabel= r a,b,b',b'';(b'{=}b'')&(b{=}b')|-(b{=}b'')    # \text{trans}
%D    e0 e3 harrownodes nil 20 nil |->
%D    e2 e3 <= sl_  e2 e3 |-> sl^ .plabel= a {ñ}
%D    e3 e5 <= sl_  e3 e5 |-> sl^ .plabel= a {ñ}
%D    e4 e5 => sl_  e4 e5 |-> sl^ .plabel= a \co{ñ}
%D    b2 b3 |-> .plabel= a b'':=b'
%D    b3 b5 |->
%D    b4 b5 |-> .plabel= a b'':=b
%D ))
%D enddiagram

The ``symmetry'' rule for equality (on variables):

\msk

$\diag{Hyp-eq-sym}$

\bsk

The ``transitivity'' rule for equality (on variables):

\msk

$\diag{Hyp-eq-trans}$

\newpage
% --------------------
% «weak-strong-exelim»  (to ".weak-strong-exelim")
% (s "Weak and strong exists-elim" "weak-strong-exelim")
\myslide {Weak and strong exists-elim} {weak-strong-exelim}


There are two versions of $(ÎE)$, $(ÎE^-)$ and $(ÎE^+)$.

They are ``equivalent enough'', and $(ÎE^-)$ is much simpler
categorically.

The rules, in natural deduction and sequent calculus forms:
%:
%:             [P(a,b)]^1  Q(a)
%:             ::::::::::::::::
%:  Îb.P(a,b)        R(a)               a,b;P(a,b),Q(a)|-R(a)
%:  ---------------------1;(ÎE^+)	----------------------(ÎE^+)
%:            R(a)			a;Îb.P(a,b),Q(a)|-R(a)
%:
%:  	      ^ex-elim-+-nd	        ^ex-elim-+-sc
%:
%:             [P(a,b)]^1
%:             ::::::::::
%:  Îb.P(a,b)     Q(a)                 a,b;P(a,b)|-Q(a)
%:  ------------------1;(ÎE^-)        -----------------(ÎE^-)
%:           Q(a)                     a;Îb.P(a,b)|-Q(a)
%:
%:  	      ^ex-elim---nd	        ^ex-elim---sc
%:
$$\ded{ex-elim-+-nd} \qquad \ded{ex-elim-+-sc}$$
$$\ded{ex-elim---nd} \qquad \ded{ex-elim---sc}$$
%
\indent $(ÎE^-)$ is a particular case of $(ÎE^+)$ --- take $Q(a):=§$
in $(ÎE^+)$.

\medskip

In the presence of $(¶)$ the rule $(ÎE^-)$ implies $(ÎE^+)$:
%:
%:                [P(a,b)]^2  [Q(a)]^1
%:                ::::::::::::::::::::
%:                       R(a)
%:                     ---------1;(¶I)
%:        Îb.P(a,b)    Q(a)¶R(a)
%:        ---------------------2;(ÎE^+)
%:  Q(a)        Q(a)¶R(a)
%:  ---------------------(¶E)
%:           R(a)
%:
%:           ^ex-elim---implies-+
%:
$$\ded{ex-elim---implies-+}$$

%D diagram exists-elim--
%D 2Dx       100            +35
%D 2D 100  P(a,b) ====> Îb.P(a,b)
%D 2D	     -              -
%D 2D	     |     |-->     |
%D 2D	     v              v
%D 2D +25 {}Q(a) <======= Q(a)
%D 2D
%D 2D +15   a,b |---------> a
%D 2D
%D ((   P(a,b) Îb.P(a,b)
%D      {}Q(a)   Q(a)
%D       a,b      a
%D    @ 0 @ 1 =>
%D    @ 0 @ 2 |-> @ 1 @ 3 |->
%D    @ 0 @ 3 harrownodes nil 20 nil |->
%D    @ 2 @ 3 <=
%D    @ 4 @ 5 |->
%D ))
%D enddiagram

%D diagram exists-elim-+
%D 2Dx       100            +45             +50              +55
%D 2D 100 P(a,b)&Q(a) <=== P(a,b) ====> Îb.P(a,b) ===> (Îb.P(a,b))&Q(a)
%D 2D	       -             -              -                -
%D 2D	       |    |-->     |     |-->     |      |-->      |
%D 2D	       v             v              v                v
%D 2D +25   {}R(a) ===> {}Q(a)¶R(a) <= Q(a)¶R(a){} <======= R(a)
%D 2D
%D 2D +15   {}a,b ========= a,b |---------> a ============== a{}
%D 2D
%D (( P(a,b)&Q(a)   P(a,b)    Îb.P(a,b) (Îb.P(a,b))&Q(a)
%D      {}R(a)   {}Q(a)¶R(a) Q(a)¶R(a){}       R(a)
%D      {}a,b        a,b          a            a{}
%D    @ 0 @ 1 <=  @ 1 @ 2 =>  @ 2 @ 3 =>
%D    @ 0 @ 4 |-> @ 1 @ 5 |-> @ 2 @ 6 |-> @ 3 @ 7 |->
%D    @ 0 @ 5 harrownodes nil 20 nil |->
%D    @ 1 @ 6 harrownodes nil 20 nil |->
%D    @ 2 @ 7 harrownodes nil 20 nil |->
%D    @ 4 @ 5 =>  @ 5 @ 6 <=  @ 6 @ 7 <=
%D    @ 8 @ 9 =   @ 9 @ 10 |-> @ 10 @ 11 =
%D ))
%D enddiagram

$(ÎE^-)$, categorically:

$\diag{exists-elim--}$

\medskip

$(ÎE^+)$, categorically:

$\diag{exists-elim-+}$

Note that $\O[\dncdisplay[a,b|Q(a)¶R(a)]]$ has two constructions,

with a hidden iso between them.

\newpage
% --------------------
% «rules-nd-sc»  (to ".rules-nd-sc")
% (s "Rules in ND and sequent calculus" "rules-nd-sc")
\myslide {Rules in ND and sequent calculus} {rules-nd-sc}


\def\hli{\mathstrut \\ \hline \mathstrut \\}

%:
%:   (&I):  P   P			          --| P |--
%:	    :   :			         /    -    \
%:	    Q   R        P|-Q    P|-R	        /     |     \
%:	    -----(&I)    ------------(&I)      v      v      v
%:	     Q&R           P|-Q&R             Q <--| Q&R |--> R
%:
%:           ^andI-nd      ^andI-sc
%:
%:
%:  (&E):     Q&R            Q&R
%:	      ---(&E_1)      ---(&E_2)
%:	   P   Q          P   R            P,Q|-S           P,R|-S
%:	   :::::          :::::           --------(&E_1)   --------(&E_2)
%:	     S              S             P,Q&R|-S        P,Q&R|-S
%:
%:	     ^andE1-nd      ^andE2-nd     ^andE1-sc       ^andE2-sc
%:
%:
%:   (¶I):   P   [Q]^1                   P&Q <=== P
%:           :::::::::                    -       -
%:               R         P,Q|-R         |  |->  |
%:              ---1;(¶I)  ------(¶I)     v       v
%:              Q¶R        P|-Q¶R         R ===> Q¶R
%:
%:              ^impI-nd   ^impI-sc
%:                                                   ---| P |----
%:                                                  /     -      \
%:   (¶E):    P     P                              /      |       \
%:            :     :                             v       v        v
%:            Q    Q¶R       P|-Q   P|-Q¶R       Q <--| (Q¶R)&Q |--> Q¶R{}
%:            --------(¶E)   -------------(¶E)            -    <===  -
%:               R               P|-R                     |    <--|  |\id
%:                                                        v          v
%:               ^impE-nd        ^impE-sc                 R ======> Q¶R
%:
%:
%:
%:   (ýI):    P(a)                                Q(a) <====== Q(a)
%:	     ::::::                                -            -
%:	     Q(a,b)        a,b;P(a)|-Q(a,b)        |    |-->    |
%:	   ---------(ýI)   ----------------(ýI)    v            v
%:	   ýb.Q(a,b)       a;P(a)|-ýb.Q(a,b)     R(a,b) ===> ýb.R(a,b)
%:
%:	     ^FaI-nd       ^FaI-sc                a,b |-------> a
%:
%:
%:   (ýE):   a       Q(a)
%:	     :        :
%:	    f(a)   ýb.R(a,b)        a|-f(a)  a;Q(a)|-ýb.R(a,b)
%:	    ----------------(ýE)    --------------------------(ýE)
%:	        R(a,f(a))              a;Q(a)|-R(a,f(a))
%:
%:	        ^FaE-nd                ^FaE-sc
%:
%:                                   Q(a) <====== Q(a) <===== Q(a)
%:				      -            -           -
%:				      |    <--|    |    <--|   |
%:				      v            v           v
%:				   R(a,f(a)) ==> R(a,b) ==> ýb.R(a,b)
%:                                       b:=f(a)
%:                                    a |-------> a,b |------> a
%:
%:   (ÎI):    Q(a)
%:	   :::::::::
%:	   P(a,f(a))         a;Q(a)|-P(a,f(a))
%:	   ---------(ÎI)     -----------------(ÎI)
%:	   Îb.P(a,b)         a;Q(a)|-Îb.P(a,b)
%:
%:	    ^ExI-nd           ^ExI-sc
%:
%:	                     P(a,f(a)) <===== P(a,b) =====> Îb.P(a,b)
%:	    	  	         -              -               -
%:	    		         |     <--|     |     <--|      |\id
%:	    	  	         v              v               v
%:	    		     Îb.P(a,b) <=== Îb.P(a,b) <===  Îb.P(a,b)
%:	    		             b:=f(a)
%:	    		         a |---------> a,b |----------> a
%:
%:
%:   (ÎE):          [P(a,b)]^1  Q(a)
%:	            ::::::::::::::::
%:	 Îb.P(a,b)        R(a)         a,b;P(a,b),Q(a)|-R(a)
%:	 ---------------------(ÎE)     ----------------------(ÎE)
%:	          R(a)                 a;Îb.P(a,b),Q(a)|-R(a)
%:
%:                ^ExE-nd                  ^ExE-sc
%:

The rules, in natural deduction form ($(ýE)$ is wrong):
%
$$\begin{array}{c|c}
  \ded{andI-nd} & \ded{andE1-nd} \qquad \ded{andE2-nd} \\ \hli
  \ded{impI-nd} & \ded{impE-nd} \\ \hli
  \ded{FaI-nd}  & \ded{FaE-nd}  \\ \hli
  \ded{ExI-nd}  & \ded{ExE-nd}  \\
  \end{array}
$$

The rules, in sequent calculus form ($(ýE)$ is wrong):
%
$$\begin{array}{c|c}
  \ded{andI-sc} & \ded{andE1-sc} \qquad \ded{andE2-sc} \\ \hli
  \ded{impI-sc} & \ded{impE-sc} \\ \hli
  \ded{FaI-sc}  & \ded{FaE-sc}  \\ \hli
  \ded{ExI-sc}  & \ded{ExE-sc}  \\
  \end{array}
$$


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


%D diagram andI-cat
%D 2Dx    100     +25     +25
%D 2D 100     --| P |--
%D 2D	     /    -    \
%D 2D	    /     |     \
%D 2D	   v      v      v
%D 2D +25 Q <--| Q&R |--> R
%D 2D
%D (( P  Q Q&R R
%D    @ 0 @ 1 |-> @ 0 @ 2 |-> @ 0 @ 3 |->
%D    @ 1 @ 2 <-| .plabel= a \pi
%D    @ 2 @ 3 |-> .plabel= a \pi'
%D ))
%D enddiagram

%D diagram andE-cat
%D 2Dx      100     +35       +35
%D 2D 100   Q <---| Q&R |---> R
%D 2D	   ||   -   ||    -   ||
%D 2D	   ||   |   ||    |   ||
%D 2D	   \/   v   \/    v   \/
%D 2D +25 P&Q <--| P&Q&R |--> P&R
%D 2D
%D ((   Q   Q&R   R
%D    P&Q P&Q&R P&R
%D    @ 0 @ 1 <-| .plabel= a \pi
%D    @ 1 @ 2 |-> .plabel= a \pi'
%D    @ 0 @ 3 => @ 1 @ 4 => @ 2 @ 5 =>
%D    @ 0 @ 4 varrownodes nil 18 nil |->
%D    @ 1 @ 5 varrownodes nil 18 nil |->
%D    @ 3 @ 4 <-| @ 4 @ 5 |->
%D ))
%D enddiagram

%D diagram impI-cat
%D 2Dx     100     +25
%D 2D 100 P&Q <=== P
%D 2D	   -       -
%D 2D	   |  |->  |
%D 2D	   v       v
%D 2D +25  R ===> Q¶R
%D 2D
%D (( P&Q P R Q¶R
%D    @ 0 @ 1 <=
%D    @ 0 @ 2 |-> @ 1 @ 3 |->
%D    @ 0 @ 3 harrownodes nil 20 nil |->
%D    @ 2 @ 3 =>
%D ))
%D enddiagram

%D diagram impE-cat
%D 2Dx    100      +35        +35
%D 2D 100     ---| P |----
%D 2D	     /     -      \
%D 2D	    /      |       \
%D 2D	   v       v        v
%D 2D +25 Q <--| (Q¶R)&Q |--> Q¶R{}
%D 2D	           -    <===  -
%D 2D	           |    <--|  |\id
%D 2D	           v          v
%D 2D +25          R ======> Q¶R
%D 2D
%D ((      P
%D    Q (Q¶R)&Q Q¶R{}
%D         R    Q¶R
%D    @ 0 @ 1 |-> @ 0 @ 2 |-> @ 0 @ 3 |->
%D    @ 1 @ 2 <-|     .plabel= a {\phantom{\;\;\;\;}\pi'}
%D    @ 2 @ 3 |-> sl^ .plabel= a {\pi}
%D    @ 2 @ 3 <= sl_
%D    @ 2 @ 4 |-> @ 3 @ 5 |-> .plabel= r \id
%D    @ 2 @ 5 harrownodes nil 20 nil <-|
%D    @ 4 @ 5 =>
%D ))
%D enddiagram

%D diagram faI-cat
%D 2Dx     100           +35
%D 2D 100  Q(a) <====== Q(a){}
%D 2D	    -            -
%D 2D	    |    |-->    |
%D 2D	    v            v
%D 2D +25 R(a,b) ===> ýb.R(a,b)
%D 2D
%D 2D +15  a,b |-------> a
%D 2D
%D ((  Q(a)   Q(a){}
%D    R(a,b) ýb.R(a,b)
%D     a,b      a
%D    @ 0 @ 1 <=
%D    @ 0 @ 2 |-> @ 1 @ 3 |->
%D    @ 0 @ 3 harrownodes nil 20 nil |->
%D    @ 2 @ 3 =>
%D    @ 4 @ 5 |->
%D ))
%D enddiagram

%D diagram faE-cat
%D 2Dx       100         +35          +35
%D 2D 100 {}Q(a) <====== Q(a) <===== Q(a){}
%D 2D	     -            -           -
%D 2D	     |    <--|    |    <--|   |
%D 2D	     v            v           v
%D 2D +25 R(a,f(a)) ==> R(a,b) ==> ýb.R(a,b)
%D 2D	        b:=f(a)
%D 2D +15    a |-------> a,b |------> a{}
%D 2D
%D ((  {}Q(a)    Q(a)   Q(a){}
%D    R(a,f(a)) R(a,b) ýb.R(a,b)
%D       a       a,b      a{}
%D    @ 0 @ 1 <= @ 1 @ 2 <=
%D    @ 0 @ 3 |-> @ 1 @ 4 |-> @ 2 @ 5 |->
%D    @ 0 @ 4 harrownodes nil 20 nil <-|
%D    @ 1 @ 5 harrownodes nil 20 nil <-|
%D    @ 3 @ 4 => @ 4 @ 5 =>
%D    @ 6 @ 7 |-> .plabel= a b:=f(a)  @ 7 @ 8 |->
%D ))
%D enddiagram

%D diagram exI-cat
%D 2Dx          100           +40              +40
%D 2D 100   P(a,f(a)) <===== P(a,b) =====> Îb.P(a,b){}{}
%D 2D	        -              -               -
%D 2D	        |     <--|     |     <--|      |\id
%D 2D	        v              v               v
%D 2D +25 {}Îb.P(a,b) <=== Îb.P(a,b) <===  Îb.P(a,b){}
%D 2D	            b:=f(a)
%D 2D +15       a |---------> a,b |----------> a{}
%D 2D
%D ((   P(a,f(a))   P(a,b)  Îb.P(a,b){}{}
%D    {}Îb.P(a,b) Îb.P(a,b) Îb.P(a,b){}
%D          a        a,b        a{}
%D    @ 0 @ 1 <= @ 1 @ 2 =>
%D    @ 0 @ 3 |-> @ 1 @ 4 |-> @ 2 @ 5 |->
%D    @ 0 @ 4 harrownodes nil 20 nil <-|
%D    @ 1 @ 5 harrownodes nil 20 nil <-|
%D    @ 3 @ 4 <= @ 4 @ 5 <=
%D    @ 6 @ 7 |-> .plabel= a b:=f(a)  @ 7 @ 8 |->
%D ))
%D enddiagram

The rules, categorically ($(\&E)$ needs explanations, $(ýE)$ is wrong):
%
$$\begin{array}{c|c}
  \diag{andI-cat} & \diag{andE-cat} \\ \hli
  \diag{impI-cat} & \diag{impE-cat} \\ \hli
  \diag{faI-cat}  & \diag{faE-cat}  \\ \hli
  \diag{exI-cat}  & \text{(see next page)} \\
  \end{array}
$$


%

\end{document}

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