|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2010hyps.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2010hyps.tex && latex 2010hyps.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2010hyps.tex && pdflatex 2010hyps.tex"))
% (eev "cd ~/LATEX/ && Scp 2010hyps.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (defun d () (interactive) (find-dvipage "~/LATEX/2010hyps.dvi"))
% (find-dvipage "~/LATEX/2010hyps.dvi")
% (find-pspage "~/LATEX/2010hyps.ps")
% (find-pspage "~/LATEX/2010hyps.pdf")
% (find-xpdfpage "~/LATEX/2010hyps.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvipdf 2010hyps.pdf 2010hyps.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2010hyps.ps 2010hyps.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2010hyps.ps 2010hyps.dvi && ps2pdf 2010hyps.ps 2010hyps.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2010hyps.pdf" (ee-twupfile "LATEX/2010hyps.pdf") 'over)
% (ee-cp "~/LATEX/2010hyps.pdf" (ee-twusfile "LATEX/2010hyps.pdf") 'over)
% (find-twusfile "LATEX/" "2010hyps")
% http://angg.twu.net/LATEX/2010hyps.pdf
% «.HYPERDOCTRINES» (to "HYPERDOCTRINES")
% «.hyperdoctrines» (to "hyperdoctrines")
% «.subobjects» (to "subobjects")
% «.subobjects-2» (to "subobjects-2")
% «.subobjects-3» (to "subobjects-3")
% «.subobjects-4» (to "subobjects-4")
% «.cartesianness» (to "cartesianness")
% «.cartesianness-2» (to "cartesianness-2")
% «.pbs-are-cartesian» (to "pbs-are-cartesian")
% «.cleavages» (to "cleavages")
% «.cleavages-2» (to "cleavages-2")
% «.cleavage-induces-cob» (to "cleavage-induces-cob")
% «.adjs-to-change-of-base» (to "adjs-to-change-of-base")
% «.nd-in-pred-set-quants» (to "nd-in-pred-set-quants")
% «.rules-quantifiers» (to "rules-quantifiers")
% «.rules-quantifiers-2» (to "rules-quantifiers-2")
% «.rules-equality» (to "rules-equality")
% «.adjs-to-cob-quants» (to "adjs-to-cob-quants")
% «.adjs-to-cob-equality» (to "adjs-to-cob-equality")
% «.adjs-to-cob-generic» (to "adjs-to-cob-generic")
% «.adjs-to-cob-candidates» (to "adjs-to-cob-candidates")
% «.Pand» (to "Pand")
% «.Pand-2» (to "Pand-2")
% «.Ptrue» (to "Ptrue")
% «.Pimp» (to "Pimp")
% «.BCCL» (to "BCCL")
% «.BCCR» (to "BCCR")
% «.Frobenius» (to "Frobenius")
% «.cheap-hyps» (to "cheap-hyps")
% «.pimp-implies-frob» (to "pimp-implies-frob")
% «.pimp-implies-frob-2» (to "pimp-implies-frob-2")
% «.pimp-implies-frob-3» (to "pimp-implies-frob-3")
% «.BCCL-implies-BCCR» (to "BCCL-implies-BCCR")
% «.equality-lemmas» (to "equality-lemmas")
% «.lambda-calc-in-a-hyp» (to "lambda-calc-in-a-hyp")
% «.prop-calc-in-a-hyp» (to "prop-calc-in-a-hyp")
% «.fa-E-in-a-hyp» (to "fa-E-in-a-hyp")
% «.fa-I-in-a-hyp» (to "fa-I-in-a-hyp")
% «.ex-I-in-a-hyp» (to "ex-I-in-a-hyp")
% «.ex-E-in-a-hyp» (to "ex-E-in-a-hyp")
\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 2010hyps.dnt
%*
% (eedn4-51-bounded)
%Index of the slides:
%\msk
% To update the list of slides uncomment this line:
%\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")
\setlength{\parindent}{0em}
% For "article":
% (find-dn4ex "edrx08.sty" "slides")
%\nolos
\def\myslide #1#2{\newpage{\bf \textcolor{Chocolate4}{#1}}\par\label{#2}}
\def\myslide #1#2{\newpage{\bf \textcolor{Firebrick4}{#1}}\par\label{#2}}
\mylosopen{tmp.los}
\def\myslide #1#2{\newpage{\bf #1}\par\label{#2}\addtolos{#1}}
% \mylosopen{tmp.los}
% \def\myslide #1#2{\newpage{\bf #1}\par\label{#2}}
% Experimental, 2010jun19:
\def\anchortargettext#1#2#3{\hypertarget{#1}{\href{\##2}{#3}}}
\def\tocline#1#2{\par #1 \dotfill #2}
\def\tocline#1#2{\par \anchortargettext{.#2}{#2}{#1} \dotfill #2}
\def\myslide#1#2{\newpage{\bf #1}\par\label{#2}\addtolos{#1}}
\def\myslide#1#2{\newpage{\bf \anchortargettext{\the\count0}{.\the\count0}{#1}}\par\label{#2}\addtolos{#1}}
% \def\addtolos#1{\addtocontents{mylos}{\protect\tocline{#1} {\thepage}}}
\def\tocsection#1{\par\msk {\leavevmode\phantom{x}#1:}}
\def\mysectiona#1#2{\addtocontents{mylos}{\protect\tocsection{#1}}}
\def\mysection#1#2{\newpage\mysectiona{#1}{#2}\vskip 2cm{\Large #1}}
\def\mysection#1#2{\addtocontents{mylos}{\protect\tocsection{#1}}}
% --------------------
% «HYPERDOCTRINES» (to ".HYPERDOCTRINES")
% (sec "Hyperdoctrines" "HYPERDOCTRINES")
\mysection {Hyperdoctrines} {HYPERDOCTRINES}
\def\parphst{\par\indent\phantom{$*$ }}
% --------------------
% «hyperdoctrines» (to ".hyperdoctrines")
% (s "Hyperdoctrines" "hyperdoctrines")
\myslide {Hyperdoctrines} {hyperdoctrines}
\par The following is the precise definition of a hyperdoctrine.
\par It is too technical, so we will spend the next slides dissecting it.
\msk
\par A hyperdoctrine is a (cloven) fibration, $p:\bbE \to \bbB$,
\par plus some extra structure:
\par $*$ the base category $\bbB$ is a CCC
\parphst (i.e., $(\bbB, ×, 1, \to)$ is a CCC))
\par $*$ each fiber $\bbE_B$ is a CCC
\parphst (i.e., each $(\bbE_B, ∧, §, ⊃)$ is a CCC)
\par $*$ for each map $g:B \to C$ in $\bbB$
\parphst the change-of-base functor $f^*$ has adjoints $Î_f \dashv f^* \dashv ý_f$
\par $*$ change-of-base preserves $∧$, $§$, $⊃$ modulo iso
\parphst ($\Pand$, $\Ptrue$, $\Pimp$)
\par $*$ the left and right Beck-Chevalley conditions hold
\parphst ($\BCCL$, $\BCCR$)
\par $*$ the Frobenius condition holds
\parphst ($\Frob$)
\bsk
\par The precise definition of what a fibration is
\par is quite technical. I will give it in full here ---
\par it will take several slides --- but if you are a
\par non-specialist you should only pay only attention
\par to the last two operations: change-of-base functors
\par and the isomorphism between two changes of base
\par for the same $g:B \to C$.
% --------------------
% «subobjects» (to ".subobjects")
% (s "Subobjects" "subobjects")
\myslide {Subobjects} {subobjects}
\par Our archetypical fibration will be $\Cod: \CanSub(\Set) \to \Set$,
\par where the ``codomain functor'', $\Cod$, takes each
\par ``canonical subobject'' $P$ in $\Set$
\par (where $P$ is an inclusion map $\sst{bÝB}{P(b)} \ito B$)
\par and returns its codomain, $B$.
\msk
\par The categorical way to describe ``injective maps''
\par is via the notion of ``monic''.
\par The monic arrows of $\Set$ are exactly the injective maps.
\par In $\Set$ {\sl some} injective maps are inclusions.
\par Let's regard $\Set$ as category with a (given) distinguished
\par class of monics --- the ``inclusions''.
\par A {\sl subobject of $B$} is a monic $A \monicto B$
\par with codomain $B$.
\par A {\sl canonical subobject of $B$} is an inclusion $B' \ito B$
\par with codomain $B$.
\msk
\par Two subobjects of $B$, $B' \monicto B$ and $B'' \monicto B$
\par are {\sl isomorphic} when there is an iso $B' \bij B''$
\par making the obvious triangle commute:
%
%D diagram subobjs-1
%D 2Dx 100 +15 +15
%D 2D 100 B' <--> B''
%D 2D
%D 2D +20 B
%D 2D
%D (( B' B'' <->
%D B' B >->
%D B'' B >->
%D ))
%D enddiagram
%D
$$\diag{subobjs-1}$$
\par Each subobject $f: B' \monicto B$
\par is isomorphic to a unique canonical subobject of $B$:
%
%D diagram subobjs-2
%D 2Dx 100 +25 +50
%D 2D 100 B' <--> B'' = B'''
%D 2D
%D 2D +30 B
%D 2D
%D (( B'' .tex= ¯{Im(f)}
%D B' B'' <->
%D B' B >-> .plabel= l f
%D B'' B `->
%D B''' .tex= \sst{bÝB}{f^{-1}(b)\neq\emp}
%D B'' B''' =
%D ))
%D enddiagram
%D
$$\diag{subobjs-2}$$
% --------------------
% «subobjects-2» (to ".subobjects-2")
% (s "Subobjects (2)" "subobjects-2")
\myslide {Subobjects (2)} {subobjects-2}
We will use the following notations for
canonical subobjects. In the archetypal case,
%D diagram pdiagcansub
%D 2Dx 100
%D 2D 100 #1
%D 2D +18 #2
%D 2D
%D (( #1 #2 `->
%D ))
%D enddefpdiagram 2
%D diagram cansubs
%D 2Dx 100 +55 +55
%D 2D 100 T1 T2
%D 2D
%D 2D +30 P1 P2 E
%D 2D
%D 2D +30 A1 A2 B
%D 2D
%D (( T1 .tex= \tbox{explicit,\\long"form:}
%D T2 .tex= \tbox{shorthand\\(note"the"`$||$'!):}
%D P1 .tex= \pdiagcansub{\sst{aÝA}{P(a)}}{A} BOX
%D A1 .tex= A
%D P2 .tex= \ssst{a}{P(a)}
%D A2 .tex= A
%D E .tex= \bbE=\CanSub(\Set)
%D B .tex= \bbB=\Set
%D T1 place T2 place
%D P1 place A1 place
%D P2 place A2 place
%D E B -> .plabel= r p=\Cod
%D ))
%D enddiagram
%D
$$\def\tbox#1{\begin{tabular}{l}#1\end{tabular}}
\diag{cansubs}
$$
and in the generic/abstract case,
%D diagram fib-notation
%D 2Dx 100 +20
%D 2D 100 P E
%D 2D
%D 2D +20 A B
%D 2D
%D (( P place A place
%D E .tex= \bbE
%D B .tex= \bbB
%D E B -> .plabel= r p
%D ))
%D enddiagram
%D
$$\diag{fib-notation}$$
$\bbE$ is the ``entire category'',
$\bbB$ is the ``base category'',
$p$ is the ``projection'',
$P$ is a ``proposition over $A$''.
\msk
Note that instead of drawing a vertical arrow
$P \mto pP{=}A$ we just draw $P$ over $A$.
(We will do the same for morphisms, by the way).
\msk
% --------------------
% «subobjects-3» (to ".subobjects-3")
% (s "Subobjects (3)" "subobjects-3")
\myslide {Subobjects (3)} {subobjects-3}
\par If $B$ is an object of $\bbB$, the {\sl fiber over $B$}, $\bbE_B$,
\par is the subcategory of $\bbE$ composed of the objects and morphisms
\par of $\bbE$ that are taken to $B$ and $\id_B$ by the projection $p$.
\msk
\par Being ``over $B$'' means ``belonging to $\bbE_B$''.
\par A morphism of $\bbE$ is said to be {\sl vertical} if its image
\par is an identity in $\bbB$.
\par We will have a notion of ``horizontal morphisms'' too,
\par but it will be harder to formalize --- it will involve {\sl cartesianness}.
\par Let's start with an example.
\msk
\par Every map $g:B \to C$ in the base category
\par induces a ``change-of-base functor'', $g^*:\bbE_C \to \bbE_B$,
\par and a natural transformation $\ov{g}:g^* \to \id_{\bbE_C}$,
\par as in the diagram below:
%D diagram cob-1
%D 2Dx 100 +50 +35 +35
%D 2D 100 {b||Q(b)} -\ Q ----\
%D 2D | \ | \
%D 2D v v v v
%D 2D +30 {b||R(gb)} -> {c||R(c)} g^*R -----> R
%D 2D | | | |
%D 2D v v v v
%D 2D +30 {b||S(gb)} -> {c||S(c)} g^*S -----> S
%D 2D
%D 2D +20 {B} ---------> {C} B -------> C
%D 2D
%D (( {b||Q(b)} .tex= \ssst{b}{Q(b)}
%D {b||R(gb)} .tex= \ssst{b}{R(g(b))} {c||R(c)} .tex= \ssst{c}{R(c)}
%D {b||S(gb)} .tex= \ssst{b}{S(g(b))} {c||S(c)} .tex= \ssst{c}{S(c)}
%D @ 0 @ 1 -> @ 0 @ 2 ->
%D @ 1 @ 2 ->
%D @ 1 @ 3 -> @ 2 @ 4 ->
%D @ 3 @ 4 ->
%D {B} {C} -> .plabel= a g
%D ))
%D (( Q g^*R R g^*S S
%D @ 0 @ 1 -> .plabel= l k @ 0 @ 2 -> .plabel= r j
%D @ 1 @ 2 -> .plabel= a \ov"g_R
%D @ 1 @ 3 -> .plabel= l g^*i
%D @ 2 @ 4 -> .plabel= r i
%D @ 3 @ 4 -> .plabel= a \ov"g_S
%D B C -> .plabel= a g
%D ))
%D enddiagram
%D
$$\diag{cob-1}$$
\par The vertical map $i:R \to S$ exists iff $\sst{c}{R(c)} \subseteq \sst{c}{S(c)}$,
\par i.e., if $ýc.R(c)⊃S(c)$.
\par The diagonal map $j:Q \to S$ exists iff its factorization through $\ov{g}_R$, $k$,
\par exists (because every map in $\bbE$ factors as ``vertical map followed by
\par an horizontal map'', and we shall see), and:
\par the vertical map $k:Q \to g^*R$ exists iff $\sst{b}{Q(b)} \subseteq \sst{b}{R(g(b))}$,
\par i.e., if $ýb.Q(b)⊃R(g(b))$ --- so the vertical/horizontal factorization
\par gives us a way to interpret diagonal morphisms ``logically''.
% --------------------
% «subobjects-4» (to ".subobjects-4")
% (s "Subobjects (4)" "subobjects-4")
\myslide {Subobjects (4)} {subobjects-4}
The horizontal maps of the diagram
%
$$\diag{cob-1}$$
are pullbacks in $\Set$:
%D diagram cob-2
%D 2Dx 100 +50
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +20 B0 B1
%D 2D
%D 2D +20 B2 B3
%D 2D
%D (( A0 .tex= \sst{b}{R(g(b))} A1 .tex= \sst{c}{R(c)}
%D A2 .tex= B A3 .tex= C
%D B0 .tex= \sst{b}{S(g(b))} B1 .tex= \sst{c}{S(c)}
%D B2 .tex= B B3 .tex= C
%D A0 A1 -> A0 A2 `-> A1 A3 `-> A2 A3 ->
%D A0 relplace 7 7 \pbsymbol{7}
%D B0 B1 -> B0 B2 `-> B1 B3 `-> B2 B3 ->
%D B0 relplace 7 7 \pbsymbol{7}
%D ))
%D enddiagram
%D
$$\diag{cob-2}$$
{\sl And so what?...}
% --------------------
% «cartesianness» (to ".cartesianness")
% (s "Cartesianness" "cartesianness")
\myslide {Cartesianness} {cartesianness}
% (find-LATEX "2009unilog-dnc.tex")
% (find-LATEX "2009unilog-dnc.tex" "proto-cart-morphs")
\par A {\sl vee} in a category $\bbE$ is a pair
\par of morphisms in $\bbE$, $(h':P \to R, \; g':Q \to R)$
\par with common codomain.
\par A {\sl completion} for a vee $(h':P \to R, \; g':Q \to R)$
\par is an arrow $f': P \to Q$ making the triangle commute.
\par A functor $p: \bbE \to \bbB$ takes completions of $(h',g')$
\par to completions of $(ph', pg')$; let's call this induced map $Ðp_{h'g'}^\nat$.
\msk
\par A vee $(h',g')$ in $\bbE$ has {\sl unique liftings} (for $p: \bbE \to \bbB$)
\par if the map $Ðp_{h'g'}$ induced by $p$ is a bijection.
\par A map $g':Q \to R$ in $\bbE$ is {\sl cartesian}
\par if any vee $(h',g')$ with $g'$ as its ``lower leg''
\par has unique liftings.
%D diagram vee-over-vee
%D 2Dx 100 +25 +35
%D 2D 100 P
%D 2D
%D 2D +25 Q R
%D 2D
%D 2D +20 pP
%D 2D
%D 2D +25 pQ pR
%D 2D
%D (( P R -> .plabel= a h'
%D P Q --> .plabel= b f'
%D Q R -> .plabel= b g'
%D pP .tex= A{=}pP
%D pQ .tex= B{=}pQ
%D pR .tex= C{=}pR
%D pP pR -> .plabel= a h=ph'
%D pP pQ --> .plabel= b f=pf'
%D pQ pR -> .plabel= b g=pg'
%D P pQ varrownodes nil 20 5 -> .plabel= l Ðp_{h'g'}^\nat
%D ))
%D enddiagram
$$\diag{vee-over-vee}$$
\par To make things more manageable we will use
\par some shorthands: $A:=pP$, $B:=pQ$, $C:=pR$,
\par $f:=pf'$, $g:=pg'$, $h:=ph'$,
\par Invertibility of $Ðp_{h'g'}^\nat$ means that
\par for any completion $f$ for the vee $(h,g)$
\par there is exactly one completion $f':P \to Q$ for $(h',g')$
\par ``over $f$'', i.e., such that $f=pf'$.
% --------------------
% «cartesianness-2» (to ".cartesianness-2")
% (s "Cartesianness (2)" "cartesianness-2")
\myslide {Cartesianness (2)} {cartesianness-2}
\par A {\sl proto-vee} in a category $\bbE$ is a pair
\par of morphisms in $\bbE$, $(h':P \to R, \; g':Q \to R)$
\par with common codomain.
\par A {\sl proto-completion} for a vee $(h':P \to R, \; g':Q \to R)$
\par is an arrow $f': P \to Q$ \mycrossover{making the triangle commute}.
\par A functor $p: \bbE \to \bbB$ takes proto-completions of $(h',g')$
\par to proto-completions of $(ph', pg')$; let's call this induced map $Ðp_{h'g'}^\nat$.
\msk
\par Note that this new induced map has a bigger domain...
\par the old one had to act on all completions,
\par the new one has to act on all {\sl proto-}completions.
\msk
\par A {\sl vee with proto-unique liftings}
\par is a triple $(h',g',Ðp_{h'g'})$,
\par where $Ðp_{h'g'}$ is a proto-inverse for $Ðp_{h'g'}^\nat$.
%D diagram vee-over-vee-2
%D 2Dx 100 +25 +35
%D 2D 100 P
%D 2D
%D 2D +25 Q R
%D 2D
%D 2D +20 pP
%D 2D
%D 2D +25 pQ pR
%D 2D
%D (( P R -> .plabel= a h'
%D P Q --> .plabel= b f'
%D Q R -> .plabel= b g'
%D pP .tex= A{=}pP
%D pQ .tex= B{=}pQ
%D pR .tex= C{=}pR
%D pP pR -> .plabel= a h=ph'
%D pP pQ --> .plabel= b f=pf'
%D pQ pR -> .plabel= b g=pg'
%D P pQ varrownodes nil 20 5 -> sl_ .PLABEL= _(0.40) Ðp_{h'g'}^\nat
%D P pQ varrownodes nil 20 0 <- sl^ .PLABEL= ^(0.60) Ðp_{h'g'}
%D ))
%D enddiagram
$$\diag{vee-over-vee-2}$$
\par {\sl Proto-cartesianness} for an arrow $g'$
\par is the assurance that any vee $(h',g')$ with lower leg $g'$
\par has proto-unique liftings.
\par More formally:
\par a {\sl proto-cartesian morphism} is a pair $(g',\cart)$,
\par where $\cart \equiv (P, h' \mto Ðp_{h'g'})$ is an operation
\par that produces all the required proto-inverses.
% --------------------
% «pbs-are-cartesian» (to ".pbs-are-cartesian")
% (s "Pullbacks are cartesian" "pbs-are-cartesian")
\myslide {Pullbacks are cartesian} {pbs-are-cartesian}
\par Cartesian maps are not so weird
\par as the preceding definition suggests...
\msk
\par {\sl Fact.} When $p=\Cod$, ``pullback squares are cartesian''.
\par The core of the proof is the following diagram.
\def\poo#1#2#3{\begin{pmatrix}
#1 \\
\scriptstyle{#2} \dnto \phantom{\scriptstyle{#2}} \\
#3 \\
\end{pmatrix}
}
\def\poom#1#2{(#1,#2)}
\def\poom#1#2{\begin{smallmatrix}#1,\\#2\end{smallmatrix}}
\def\poom#1#2{\left(\begin{smallmatrix}#1,\\#2\end{smallmatrix}\right)}
\def\poom#1#2{\begin{smallmatrix}#1\\#2\end{smallmatrix}}
\def\poom#1#2{\psm{#1\\#2}}
%
%D diagram pullbacks-are-cartesian
%D 2Dx 100 +40 +50
%D 2D 100 AA
%D 2D
%D 2D +30 BB CC
%D 2D
%D 2D +15 A
%D 2D
%D 2D +30 B C
%D 2D
%D (( AA .tex= \poo{A''}{a}{A}
%D BB .tex= \poo{B×_{C}C''}{\pi}{B}
%D CC .tex= \poo{C''}{c}{C}
%D AA BB -> .plabel= l f'=\poom{\ang{a;f,\,h''}}{f}
%D BB CC -> .plabel= b g'=\poom{\pi'}{g}
%D AA CC -> sl^^ .plabel= a h'=\poom{h''}{h}
%D A B -> .plabel= l f
%D B C -> .plabel= b g
%D A C -> .plabel= a h
%D ))
%D enddiagram
%D
%D diagram pullbacks-are-cartesian-2
%D 2Dx 100 +40 +50
%D 2D 100 A''
%D 2D
%D 2D +30 A B×C'' C''
%D 2D
%D 2D +30 B C
%D 2D
%D (( B×C'' .tex= B×_{C}C''
%D A'' C'' -> .plabel= a h''
%D A'' A -> .plabel= l a
%D A'' B×C'' -> .plabel= m \ang{a;f,\,h''}
%D B×C'' C'' -> .plabel= b \pi'
%D B×C'' B -> .plabel= l \pi
%D C'' C -> .plabel= r c
%D A B -> .plabel= b f
%D B C -> .plabel= b g
%D
%D ))
%D enddiagram
%D
$$\diag{pullbacks-are-cartesian}
\quad
\diag{pullbacks-are-cartesian-2}
$$
The arrow $g'=\poom{\pi'}{g}$ is a ``pullback square''.
Fix any $h'=\poom{h''}{h}$ with the same codomain as $g'$.
For any completion $f$ of the lower vee $(h, g)$,
its lifting is $f'=\poom{\ang{a;f,\,h''}}{f}$.
% --------------------
% «cleavages» (to ".cleavages")
% (s "Cleavages" "cleavages")
\myslide {Cleavages} {cleavages}
\par Here's the abstract view of cartesianness \& friends ---
\par formulated in a way that projects well into the syntactical world.
\par Note that the conditions $pR=C$, $pg'=g$, etc, are always implicit;
\par the conditions $h=f;g$ and $h'=f';g'$ are implicit
\par whenever $f,g$ (resp. $f',g'$) are defined
\par {\sl and when we are in the real world;}
\par in the syntactical world they are irrelevant.
$$\diag{vee-over-vee-2}$$
\par {\sl Unique liftings} for a vee $(h', g')$ is an inverse $Ðp_{h'g'}$
\par for the natural operation $Ðp_{h'g'}^\nat$.
\par {\sl Cartesianness} for an arrow $g'$
\par is an operation $Ð{cart}_{g'} \equiv (P,h' \mto Ðp_{h'g'})$.
\par A {\sl cartesian lifting} for $g:B \to C$ at $R$
\par is a triple $Ð{clift}_{gR} \equiv (Q, g', Ð{cart}_{g'})$.
\par A {\sl family of cartesian liftings} for $g:B \to C$
\par is an operation $Ð{clifts}_g \equiv (R \mto Ð{clift}_{gR})$.
\par A {\sl cleavage} (for the functor $p: \bbE \to \bbB$)
\par is an operation $Ð{cleavage} \equiv (g \mto Ð{clifts}_g)$.
\msk
\par Or all at once:
\par a cleavage (for the functor $p: \bbE \to \bbB$) is an operation
\par $Ð{cleavage} \equiv (g \mto (R \mto (Q, g', (P,h' \mto (f \mto f')))))$,
\par or, more detailedly,
\par $Ð{cleavage} \equiv (B,C,g \mto (R \mto (Q, g', (A,P,h,h' \mto (f \mto f')))))$.
\msk
\par A {\sl cloven fibration} is a 4-uple $(\bbB, \bbE, p, Ð{cleavage})$,
\par where $p:\bbE \to \bbB$ and $Ð{cleavage}$ is a cleavage for $p$.
\msk
\par One further subtlety is needed to make this work in the
\par syntactical world: as we need a restricted version of
\par equality to be able to say ``$P$ is over $A$'', ``$f'$ is over $f$'', etc,
\par $\bbE$ should be a ``category defined over $\bbB$''.
\par (Details later!)
% --------------------
% «cleavages-2» (to ".cleavages-2")
% (s "Cleavages (2)" "cleavages-2")
\myslide {Cleavages (2)} {cleavages-2}
\par A cleavage is
\par $Ð{cleavage} \equiv (B,C,g \mto (R \mto (Q, g', (A,P,h,h' \mto (f \mto f')))))$,
\par but that specification is too long (for humans).
\ssk
\par If we underline the letters whose values
\par are subsumed from subsequent ones, we get:
{
\def\u#1{\und{#1}}
\par $Ð{cleavage} \equiv (\u B,\u C,g \mto (R \mto (\u Q, g', (\u A,\u P,\u h,h' \mto (f \mto f')))))$,
}
\par and if we erase the ``redundant'' letters, we get:
\par $Ð{cleavage} \equiv g \mto (R \mto g', (h', f \mto f'))$
\par which is equivalent to:
\par $Ð{cleavage} \equiv g, R \mto g', (f, h' \mto f')$
%D diagram vee-over-vee-3
%D 2Dx 100 +25 +35
%D 2D 100 P
%D 2D
%D 2D +25 Q R
%D 2D
%D 2D +10 pP
%D 2D
%D 2D +25 pQ pR
%D 2D
%D (( P R --> .plabel= a h'
%D P Q --> .plabel= b f'
%D Q R -> .plabel= b g'
%D pP .tex= A
%D pQ .tex= B
%D pR .tex= C
%D pP pR --> .plabel= a h
%D pP pQ --> .plabel= b f
%D pQ pR -> .plabel= b g
%D # P pQ varrownodes nil 20 5 -> sl_ .PLABEL= _(0.40) Ðp_{h'g'}^\nat
%D # P pQ varrownodes nil 20 0 <- sl^ .PLABEL= ^(0.60) Ðp_{h'g'}
%D ))
%D enddiagram
$$\diag{vee-over-vee-3}$$
\par Let's call the $Q$ and the $g'$ produced by the cleavage $g^*R$ and $\ov{g}_R$:
%D diagram vee-over-vee-4
%D 2Dx 100 +25 +35
%D 2D 100 P
%D 2D
%D 2D +25 Q R
%D 2D
%D 2D +10 pP
%D 2D
%D 2D +25 pQ pR
%D 2D
%D (( Q .tex= Q=g^*R
%D P R --> .plabel= a h'
%D P Q --> .plabel= b f'
%D Q R -> .plabel= b g'=\ov{g}_R
%D pP .tex= A
%D pQ .tex= B
%D pR .tex= C
%D pP pR --> .plabel= a h
%D pP pQ --> .plabel= b f
%D pQ pR -> .plabel= b g
%D # P pQ varrownodes nil 20 5 -> sl_ .PLABEL= _(0.40) Ðp_{h'g'}^\nat
%D # P pQ varrownodes nil 20 0 <- sl^ .PLABEL= ^(0.60) Ðp_{h'g'}
%D ))
%D enddiagram
$$\diag{vee-over-vee-4}$$
\par If we consider $Ð{cleavage}$ as fixed, we get an operation
\par $f,g,h' \mto f'$
\par that factors $f'$ through the cartesian lifting of $g$ at $R = \tgt f'$,
\par and if we make $f=\id_B$ (and thus $A:=B$), then we get an operation
\par $g,h' \mto f'$
\par where now $f'$ is a vertical morphism.
\par It can be simplified. As $g := h := ph'$, it becomes
\par $h' \mto f'$,
\par the factorization of a ``diagonal'' morphism in $\bbE$, $h'$,
\par into a vertical morphism, $f'$, followed by a horizontal one, $g' = \ov{ph'}_{\tgt h'}$.
\msk
\par This factorization is reversible, in a sense:
\par given $f'$ vertical and $g'$ cartesian (horizontal --- not necessarily a $\ov{g}_R$),
\par their composite $h'$ is ``diagonal'' (``$h'$ diagonal'' means just ``$h' Ý \bbE$'').
% --------------------
% «cleavage-induces-cob» (to ".cleavage-induces-cob")
% (s "Cleavage induces change-of-base" "cleavage-induces-cob")
\myslide {Cleavage induces change-of-base} {cleavage-induces-cob}
\par A cheap cloven fibration is just a 4-uple $(\bbB, \bbE, p, Ð{cleavage})$;
\par An expensive one also comes with change-of-base functions,
\par factorization through cartesian morphisms,
\par rules that say that the composites of cartesians are cartesian,
\par a family of adjunctions $R \mto (p_R \dashv Ð{clift_R})$ {\quad [$\ot$ {\it complete this}]},
\par isos between different changes of base, etc.
\msk
\par Here's how to build the action on morphisms
\par of a change-of-base functor $g^*$
\par ($(g^*)_0$ comes from cartesian liftings):
%D diagram cleav-induces-cob
%D 2Dx 100 +5 +35
%D 2D 100 g^*R' -------> R'
%D 2D \ |
%D 2D \ |
%D 2D v v
%D 2D +25 g^*R ----> R
%D 2D
%D 2D +15 A
%D 2D
%D 2D +25 B -------> C
%D 2D
%D (( g^*R' R'
%D g^*R R
%D @ 0 @ 1 -> .plabel= a \ov{g}_{R'}
%D @ 0 @ 2 --> .plabel= l \sm{g^*r:=f'\\:=Ðp_{h'g'}f}
%D @ 0 @ 3 -> .plabel= m \phantom{o}h':=\ov{g}_{R'};r
%D @ 1 @ 3 -> .plabel= r r
%D @ 2 @ 3 -> .plabel= b g':=\ov{g}_{R}
%D ))
%D (( A .tex= A{:=}B
%D A B -> .plabel= l f:=\id_B
%D B C -> .plabel= b g
%D A C -> .plabel= a h:=g
%D ))
%D enddiagram
%D
$$\diag{cleav-induces-cob}$$
% --------------------
% «adjs-to-change-of-base» (to ".adjs-to-change-of-base")
% (s "Adjoints to change-of-base" "adjs-to-change-of-base")
\myslide {Adjoints to change-of-base} {adjs-to-change-of-base}
% (find-LATEX "2009unilog-dnc.tex" "dn-arch-hyperdoctrine")
\par In the archetypal case, $p = \Cod: \CanSub(\Set) \to \Set$,
\par {\sl every change-of-base functor $f^*$ has both a left and a right adjoint.}
\par In some cases these adjoints have simple forms.
\msk
\par Some terminology...
\par a map $\pi:A×B \to A$ is a ``projection'',
\par and the correspondent $\pi^*: \bbE_A \to \bbE_{A×B}$ is a ``weakening functor'';
\par a map $\pi:A×B \to A×B×B$ is a ``diagonal'',
\par and the correspondent $\dd^*: \bbE_{A×B×B} \to \bbE_{A×B}$ is a ``contraction functor''.
\par A $\pi^*$ ``introduces a dummy variable'',
\par a $\dd^*$ ``collapses two variables''.
%D diagram adjs-to-change-of-base-set
%D 2Dx 100 +60 +35 +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 +15 a0 |--> a1 b0 |--> b1 c0 |--> c1
%D 2D
%D (( A0 .tex= \ssst{a,b}{P(a,b)} A1 .tex= \ssst{a}{Îb.P(a,b)}
%D A2 .tex= \ssst{a,b}{Q(a)} A3 .tex= \ssst{a}{Q(a)}
%D A4 .tex= \ssst{a,b}{R(a,b)} A5 .tex= \ssst{a}{ýb.P(a,b)}
%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 -> .plabel= a \pi
%D ))
%D (( B0 .tex= P B1 .tex= Î_fP
%D B2 .tex= f^*Q B3 .tex= Q
%D B4 .tex= R B5 .tex= ý_fR
%D b0 .tex= A b1 .tex= 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 -> .plabel= a f
%D ))
%D enddiagram
%D
$$\diag{adjs-to-change-of-base-set}$$
\msk
%D diagram adjs-to-change-of-base-dnc
%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 +15 a0 |--> a1 b0 |--> b1 c0 |--> c1
%D 2D
%D (( A0 .tex= Pab A1 .tex= Îb.Pab
%D A2 .tex= Qa A3 .tex= Qa
%D A4 .tex= Rab A5 .tex= ýb.Rab
%D a0 .tex= a,b a1 .tex= a
%D A0 A1 =>
%D A0 A2 |-> A1 A3 |-> A0 A3 harrownodes nil 20 nil <->
%D A2 A3 <=
%D A2 A4 |-> A3 A5 |-> A2 A5 harrownodes nil 20 nil <->
%D A4 A5 =>
%D a0 a1 |->
%D ))
%D (( B0 .tex= Pab B1 .tex= b{=}b'{∧}Pabb
%D B2 .tex= Qabb B3 .tex= Qabb'
%D B4 .tex= Rab B5 .tex= b{=}b'{⊃}Rab
%D b0 .tex= a,b b1 .tex= a,b,b'
%D B0 B1 =>
%D B0 B2 |-> B1 B3 |-> B0 B3 harrownodes nil 20 nil <->
%D B2 B3 <=
%D B2 B4 |-> B3 B5 |-> B2 B5 harrownodes nil 20 nil <->
%D B4 B5 =>
%D b0 b1 |->
%D ))
%D (( C0 .tex= Pa C1 .tex= Îa.a{=}fb{∧}Pa
%D C2 .tex= Qfa C3 .tex= Qb
%D C4 .tex= Ra C5 .tex= ýa.a{=}fb{⊃}Pa
%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-dnc}$$
% --------------------
% «nd-in-pred-set-quants» (to ".nd-in-pred-set-quants")
% (s "Semantics for ND in Pred(Set): quantifiers" "nd-in-pred-set-quants")
\myslide {Semantics for ND in Pred(Set): quantifiers} {nd-in-pred-set-quants}
%D diagram semantics-for-quants-1
%D 2Dx 100 +25 +35 +25
%D 2D 100 P' ===> ÆP'
%D 2D - -
%D 2D | |-> |
%D 2D v v
%D 2D +30 P0 P ====> ÆP LRQ0
%D 2D - - - -
%D 2D | | |-> | |
%D 2D | | <-| | |
%D 2D v v v v
%D 2D +30 RLP0 Q* <=== Q Q0
%D 2D - -
%D 2D | <-| |
%D 2D v v
%D 2D +30 LRR1 Q'* <== Q' Q1
%D 2D - - - -
%D 2D | | <-| | |
%D 2D | | |-> | |
%D 2D v v v v
%D 2D +30 R1 R ====> åR RLQ1
%D 2D - -
%D 2D | |-> |
%D 2D v v
%D 2D +30 R' ===> åR'
%D 2D
%D 2D +20 b |---> a
%D 2D
%D (( P' .tex= P'xy ÆP' .tex= Îy.P'xy =>
%D P .tex= Pxy ÆP .tex= Îy.Pab =>
%D Q* .tex= Qx Q .tex= Qx <=
%D Q'* .tex= Q'x Q' .tex= Q'x <=
%D R .tex= Rxy åR .tex= ýy.Rxy =>
%D R' .tex= R'xy åR' .tex= ýy.R'xy =>
%D
%D P0 .tex= Pxy LRQ0 .tex= Îy.Qx
%D RLP0 .tex= Îy'.Pxy' Q0 .tex= Qx
%D LRR1 .tex= ýy'.Rxy' Q1 .tex= Qx
%D R1 .tex= Rxy RLQ1 .tex= ýy.Qx
%D
%D b .tex= x,y a .tex= x
%D ))
%D (( P' P |->
%D ÆP' ÆP |->
%D P' ÆP harrownodes nil 20 nil |-> .plabel= a Î_
%D
%D P0 RLP0 |-> .plabel= l \eta_{Î_}
%D P Q* |->
%D ÆP Q |->
%D P Q harrownodes nil 20 nil |-> sl^ .plabel= a Î_\pi^\flat
%D P Q harrownodes nil 20 nil <-| sl_ .plabel= b Î_\pi^\sharp
%D LRQ0 Q0 |-> .plabel= r _{Î_}
%D
%D Q* Q'* |->
%D Q Q' |->
%D Q* Q' harrownodes nil 20 nil <-| .plabel= a \phantom{o}\pi^*
%D
%D LRR1 R1 |-> .plabel= l _{ý_}
%D Q'* R |->
%D Q' åR |->
%D Q'* åR harrownodes nil 20 nil <-| sl^ .plabel= a ý_\pi^\flat
%D Q'* åR harrownodes nil 20 nil |-> sl_ .plabel= b ý_\pi^\sharp
%D Q1 RLQ1 |-> .plabel= r \eta_{ý_}
%D
%D R R' |->
%D åR åR' |->
%D R åR' harrownodes nil 20 nil |-> .plabel= a ý_\pi
%D
%D b a -> .plabel= a \pi
%D ))
%D enddiagram
%D
%D diagram semantics-for-quants-2
%D 2Dx 100 +20 +30 +20
%D 2D 100 P' ===> ÆP'
%D 2D - -
%D 2D | |-> |
%D 2D v v
%D 2D +30 P0 P ====> ÆP LRQ0
%D 2D - - - -
%D 2D | | |-> | |
%D 2D | | <-| | |
%D 2D v v v v
%D 2D +30 RLP0 Q* <=== Q Q0
%D 2D - -
%D 2D | <-| |
%D 2D v v
%D 2D +30 LRR1 Q'* <== Q' Q1
%D 2D - - - -
%D 2D | | <-| | |
%D 2D | | |-> | |
%D 2D v v v v
%D 2D +30 R1 R ====> åR RLQ1
%D 2D - -
%D 2D | |-> |
%D 2D v v
%D 2D +30 R' ===> åR'
%D 2D
%D 2D +20 b |---> a
%D 2D
%D (( P' .tex= \sm{0000\\0001} ÆP' .tex= \sm{0001} =>
%D P .tex= \sm{0001\\0011} ÆP .tex= \sm{0011} =>
%D Q* .tex= \sm{0111\\0111} Q .tex= \sm{0111} <=
%D Q'* .tex= \sm{0001\\0001} Q' .tex= \sm{0001} <=
%D R .tex= \sm{0011\\0111} åR .tex= \sm{0011} =>
%D R' .tex= \sm{0111\\1111} åR' .tex= \sm{0111} =>
%D
%D P0 .tex= \sm{0001\\0011} LRQ0 .tex= \sm{0111}
%D RLP0 .tex= \sm{0011\\0011} Q0 .tex= \sm{0111}
%D LRR1 .tex= \sm{0011\\0011} Q1 .tex= \sm{0001}
%D R1 .tex= \sm{0011\\0111} RLQ1 .tex= \sm{0001}
%D
%D b .tex= x,y a .tex= x
%D ))
%D (( P' P |->
%D ÆP' ÆP |->
%D P' ÆP harrownodes nil 20 nil |->
%D
%D P0 RLP0 |->
%D P Q* |->
%D ÆP Q |->
%D P Q harrownodes nil 20 nil |-> sl^
%D P Q harrownodes nil 20 nil <-| sl_
%D LRQ0 Q0 |->
%D
%D Q* Q'* |-->
%D Q Q' |-->
%D Q* Q' harrownodes nil 20 nil <-|
%D
%D LRR1 R1 |->
%D Q'* R |->
%D Q' åR |->
%D Q'* åR harrownodes nil 20 nil <-| sl^
%D Q'* åR harrownodes nil 20 nil |-> sl_
%D Q1 RLQ1 |->
%D
%D R R' |->
%D åR åR' |->
%D R åR' harrownodes nil 20 nil |->
%D
%D b a -> .plabel= a \pi
%D ))
%D enddiagram
%D
$$\diag{semantics-for-quants-1}
\qquad
\diag{semantics-for-quants-2}
$$
% --------------------
% «rules-quantifiers» (to ".rules-quantifiers")
% (s "Rules for the quantifiers" "rules-quantifiers")
\myslide {Rules for the quantifiers} {rules-quantifiers}
\par Now our task is to understand why, and in which sense,
\par the adjoints to change-of-base that were just mentioned
\par are ``admissible''.
\msk
\par In Natural Deduction we have six rules:
\par $ÎI$, $ÎE$, $ýI$, $ýE$, ${=}I$, ${=}E$
\par (a package with all six will be called `$Îý{=}IE$')
\par and some of them only started to make sense to me (years ago!)
\par when I saw how to translate them to a sequent-calculus like form,
\par and how to interpret sequents as inclusions between subsets ---
\par so we will see each of them in its ND form, in the corresponding SC form,
\par and in a ``set-like'' form, involving functions, sets and subsets.
\msk
\par An important idea:
\par {\sl any subtree} of a derivation in natural deduction
\par ``has semantics'', i.e., can be interpreted as an inclusion
\par between subsets.
\msk
\par The rules are:
$$\begin{array}{cc|cc}
\ded{r-exI-nd} &&& \ded{r-exE-nd} \\
&&& \\
\hline &&& \\
\ded{r-faI-nd} &&& \ded{r-faE-nd} \\
&&& \\
\hline &&& \\
\ded{r-eqI-nd} &&& \ded{r-eqE-nd} \\
&&& \\
\end{array}
$$
\par but each of these (apparently) small trees
\par packs a {\sl huge} amount of information.
% --------------------
% «rules-quantifiers-2» (to ".rules-quantifiers-2")
% (s "Rules for the quantifiers (2)" "rules-quantifiers-2")
\myslide {Rules for the quantifiers (2)} {rules-quantifiers-2}
Here are the translations...
\def\sstinc#1#2#3{\sst{#1}{#2} \subseteq \sst{#1}{#3}}
\def\sstinc#1#2#3{\sst{#1}{#2} \ito \sst{#1}{#3}}
\widemtos
%:*=*{=}*
%:
%: Qa
%: :::
%: Rab \bb ýb.Rab
%: ------ýI -----------ýE
%: ýb.Rab Ra\bb
%:
%: ^r-faI-nd ^r-faE-nd
%:
%: \sstinc{a,b}{Qa}{Rab} (a|->\bb):A->B \ssst{a,b}{Rab}
%: ----------------------ýI -----------------------------ýE
%: \sstinc{a}{Qa}{ýb.Rab} \sstinc{a}{ýb.Rab}{Ra\bb}
%:
%: ^r-faI-st ^r-faE-st
%:
%: a,b;Qa|-Rab a|->\bb \ssst{a,b}{Rab}
%: -----------ýI --------------------------ýE
%: a;Qa|-ýb.Rab a;ýb.Rab|-Ra\bb
%:
%: ^r-faI-sc ^r-faE-sc
%:
%:
%:
%:
%:
%: [Pab]^1 Qa
%: ::::::
%: Pa\bb Îb.Pab Ra
%: ------ÎI ----------------ÎE
%: Îb.Pab Ra
%:
%: ^r-exI-nd ^r-exE-nd
%:
%: (a|->\bb):A->B \ssst{a,b}{Pab} \sstinc{a,b}{Pab∧Qa}{Ra}
%: -------------------------------ÎI ---------------------------ÎE
%: \sstinc{a}{Pa\bb}{Îb.Pab} \sstinc{a}{(Îb.Pab)∧Qa}{Ra}
%:
%: ^r-exI-st ^r-exE-st
%:
%: a|-\bb \ssst{a,b}{Pab} a,b;Pab,Qa|-Ra
%: -----------------------ÎI ---------------ÎE
%: a;Pa\bb|-Îb.Pab a;Îb.Pab,Qa|-Ra
%:
%: ^r-exI-sc ^r-exE-sc
%:
%:
%: b=b' Pabb
%: ---=I ----------=E
%: b=b Pabb'
%:
%: ^r-eqI-nd ^r-eqE-nd
%:
%: B \ssst{a,b,b'}{Pabb}
%: ------------------=I ---------------------------------=E
%: \sstinc{b}{§}{b=b} \sstinc{a,b,b'}{b=b'∧Pabb}{Pabb'}
%:
%: ^r-eqI-st ^r-eqE-st
%:
%: B \ssst{a,b,b'}{Pabb'}
%: --------=I -----------------------=E
%: b;§|-b=b a,b,b';b=b',Pabb|-Pabb'
%:
%: ^r-eqI-sc ^r-eqE-sc
%:
%:
%:
$$\begin{array}{c|c}
\ded{r-exI-nd} & \ded{r-exE-nd} \\ \\
\ded{r-exI-st} & \ded{r-exE-st} \\ \\
\ded{r-exI-sc} & \ded{r-exE-sc} \\ \\
\hline \\
\ded{r-faI-nd} & \ded{r-faE-nd} \\ \\
\ded{r-faI-st} & \ded{r-faE-st} \\ \\
\ded{r-faI-sc} & \ded{r-faE-sc} \\ \\
\hline \\
\ded{r-eqI-nd} & \ded{r-eqE-nd} \\ \\
\ded{r-eqI-st} & \ded{r-eqE-st} \\ \\
\ded{r-eqI-sc} & \ded{r-eqE-sc} \\
\end{array}
$$
% ****************
% ****************
% ****************
% ****************
% ****************
% ****************
% ****************
% Add: figures for quantification
% create figures for eq
% The typing of each of the rules
% --------------------
% «rules-equality» (to ".rules-equality")
% (s "Rules for equality" "rules-equality")
\myslide {Rules for equality} {rules-equality}
%:*⊃*⊃*
The three primitive rules for equality in Natural Deduction are:
%:
%: [Pabb']^1
%: :::::::
%: b=b' Pabb Pabb Qabb'
%: ---=I ----------=E -------------¯{subst};1
%: b=b Pabb' Qabb
%:
%: ^peq-=I ^peq-=E ^peq-subst
%:
$$\ded{peq-=I} \qquad \ded{peq-=E} \qquad \ded{peq-subst}$$
The four derived rules below deserve proper names.
Expensive ND systems come with them built-in,
but in cheap ND system we have to build them ourselves.
%:
%: ===¯{refl} ---=I
%: b=b := b=b
%:
%: ^refl-short ^refl-long
%:
%: ---=I
%: b=b' b=b' b=b
%: ====¯{sym} ---------=E
%: b'=b := b'=b
%:
%: ^sym-short ^sym-long
%:
%: b=b' b'=b'' b'=b'' b=b'
%: =======¯{trans} ------------=E
%: b=b'' := b=b''
%:
%: ^trans-short ^trans-long
%:
%: [Qabb]^1
%: ---------1
%: b=b' Qabb⊃Qabb
%: ---------------=E
%: b=b' Qabb' Qabb' Qabb'⊃Qabb
%: ==========="=E' -------------------
%: Qabb := Qabb
%:
%: ^=E'-short ^=E'-long
%:
$$\begin{array}{rcl}
\ded{refl-short} &:=& \ded{refl-long} \\ \\
\ded{sym-short} &:=& \ded{sym-long} \\ \\
\ded{trans-short} &:=& \ded{trans-long} \\
\ded{=E'-short} &:=& \ded{=E'-long} \\
\end{array}
$$
% --------------------
% «adjs-to-cob-quants» (to ".adjs-to-cob-quants")
% (s "Adjoints to change-of-base: quantifiers" "adjs-to-cob-quants")
\myslide {Adjoints to change-of-base: quantifiers} {adjs-to-cob-quants}
% (find-dn4 "experimental.lua" "addlayer")
%L abbrevs = addlayer(abbrevs)
%L -- abbrevs = removelayer(abbrevs)
%:*=*{=}*
%:*∧*{∧}*
%:*⊃*{⊃}*
\def\pcded#1{\left(\cded{#1}\right)}
\def\dzhbox#1{\hbox to 0pt{$#1$}}
\def\lpcded#1{\dzhbox{\hss\pcded{#1}}}
\def\rpcded#1{\dzhbox{\pcded{#1}\hss}}
%D diagram adjs-to-pi*-dnc
%D 2Dx 100 +35
%D 2D 100 100 P' ===> ÆP'
%D 2D - -
%D 2D | |-> |
%D 2D v v
%D 2D +50 +30 P ====> ÆP
%D 2D - -
%D 2D | |-> |
%D 2D | <-| |
%D 2D v v
%D 2D +40 +30 Q* <=== Q
%D 2D - -
%D 2D | <-| |
%D 2D | |-> |
%D 2D v v
%D 2D +40 +30 R ====> åR
%D 2D - -
%D 2D | |-> |
%D 2D v v
%D 2D +50 +30 R' ===> åR'
%D 2D
%D 2D +20 +20 b |---> a
%D 2D
%D (( P' .tex= P'ab ÆP' .tex= Îb.P'ab =>
%D P .tex= Pab ÆP .tex= Îb.Pab =>
%D Q* .tex= Qa Q .tex= Qa <=
%D R .tex= Rab åR .tex= ýb.Rab =>
%D R' .tex= R'ab åR' .tex= ýb.R'ab =>
%D b .tex= a,b a .tex= a
%D ))
%D (( P' P |-> .plabel= l p
%D ÆP' ÆP |-> .plabel= r Æ_p\;:=
%D P' ÆP harrownodes nil 20 nil |->
%D ÆP' ÆP midpoint x+= 20 .TeX= \rpcded{Sigma-pi-dnc} place
%D
%D P Q* |-> .PLABEL= _(0.42) g
%D P Q* |-> .PLABEL= _(0.58) =:\;f^\sharp
%D ÆP Q |-> .PLABEL= ^(0.41) g^\flat\;:=
%D ÆP Q |-> .PLABEL= ^(0.59) f
%D P Q harrownodes nil 20 nil |-> sl^
%D P Q harrownodes nil 20 nil <-| sl_
%D P Q* midpoint x+= -20 .TeX= \lpcded{Sigma-pi-sharp-dnc} place
%D ÆP Q midpoint x+= 20 .TeX= \rpcded{Sigma-pi-flat-dnc} place
%D
%D Q* R |-> .PLABEL= _(0.42) =:\;k^\flat
%D Q* R |-> .PLABEL= _(0.58) h
%D Q åR |-> .PLABEL= ^(0.43) k
%D Q åR |-> .PLABEL= ^(0.57) h^\sharp\;:=
%D Q* åR harrownodes nil 20 nil <-| sl^
%D Q* åR harrownodes nil 20 nil |-> sl_
%D Q* R midpoint x+= -20 .TeX= \lpcded{Pi-pi-flat-dnc} place
%D Q åR midpoint x+= 20 .TeX= \rpcded{Pi-pi-sharp-dnc} place
%D
%D R R' |-> .plabel= l r
%D åR åR' |-> .plabel= r å_r\;:=
%D R åR' harrownodes nil 20 nil |->
%D åR åR' midpoint x+= 20 .TeX= \rpcded{Pi-pi-dnc} place
%D
%D b a -> .plabel= a \pi
%D ))
%D enddiagram
%D
$$\diag{adjs-to-pi*-dnc}$$
%:
%: [P'ab]^1
%: :::p
%: Pab
%: ------ÎI
%: Îb.P'ab Îb.Pab
%: ----------------ÎE
%: Îb.Pab
%:
%: ^Sigma-pi-dnc
%:
%: Pab [Pab]^1
%: ------ÎI :::::g
%: Îb.Pab Îb.Pab Qa
%: ::::::f ------------ÎE
%: Qa Qa
%:
%: ^Sigma-pi-sharp-dnc ^Sigma-pi-flat-dnc
%:
%: Qa Qa
%: ::k ::h
%: b ýb.Rab Rab
%: ---------ýE ---ýI
%: Rab ýb.Rab
%:
%: ^Pi-pi-flat-dnc ^Pi-pi-sharp-dnc
%:
%: b ýb.Rab
%: -----ýE
%: Rab
%: ::r
%: R'ab
%: ---ýI
%: ýb.R'ab
%:
%: ^Pi-pi-dnc
%:
% $$\diag{adjs-to-pi*-dnc}
% \qquad
% \begin{array}{ccc}
% & \ded{Sigma-pi-dnc} \\ \\
% \ded{Sigma-pi-sharp-dnc} & \ded{Sigma-pi-flat-dnc} \\ \\
% \ded{Pi-pi-flat-dnc} & \ded{Pi-pi-sharp-dnc} \\ \\
% & \ded{Pi-pi-dnc} \\ \\
% \end{array}
% $$
% --------------------
% «adjs-to-cob-equality» (to ".adjs-to-cob-equality")
% (s "Adjoints to change-of-base: equality" "adjs-to-cob-equality")
\myslide {Adjoints to change-of-base: equality} {adjs-to-cob-equality}
%D diagram adjs-to-delta*-dnc
%D 2Dx 100 +40
%D 2D 100 100 P' ===> ÆP'
%D 2D - -
%D 2D | |-> |
%D 2D v v
%D 2D +50 +30 P ====> ÆP
%D 2D - -
%D 2D | |-> |
%D 2D | <-| |
%D 2D v v
%D 2D +50 +30 Q* <=== Q
%D 2D - -
%D 2D | <-| |
%D 2D | |-> |
%D 2D v v
%D 2D +50 +30 R ====> åR
%D 2D - -
%D 2D | |-> |
%D 2D v v
%D 2D +50 +30 R' ===> åR'
%D 2D
%D 2D +20 +20 b |---> a
%D 2D
%D (( P' .tex= P'ab ÆP' .tex= b{=}b'{∧}P'ab =>
%D P .tex= Pab ÆP .tex= b{=}b'{∧}Pab =>
%D Q* .tex= Qabb Q .tex= Qabb' <=
%D R .tex= Rab åR .tex= b{=}b'{⊃}Rab =>
%D R' .tex= R'ab åR' .tex= b{=}b'{⊃}R'ab =>
%D b .tex= a,b a .tex= a,b,b'
%D ))
%D (( P' P |-> .plabel= l p
%D ÆP' ÆP |-> .plabel= r Æ_p\;:=
%D P' ÆP harrownodes nil 20 nil |->
%D ÆP' ÆP midpoint x+= 20 .TeX= \rpcded{Sigma-delta-dnc} place
%D
%D P Q* |-> .PLABEL= _(0.42) g
%D P Q* |-> .PLABEL= _(0.58) =:\;f^\sharp
%D ÆP Q |-> .PLABEL= ^(0.41) g^\flat\;:=
%D ÆP Q |-> .PLABEL= ^(0.59) f
%D P Q harrownodes nil 20 nil |-> sl^
%D P Q harrownodes nil 20 nil <-| sl_
%D P Q* midpoint x+= -20 .TeX= \lpcded{Sigma-delta-sharp-dnc} place
%D ÆP Q midpoint x+= 20 .TeX= \rpcded{Sigma-delta-flat-dnc} place
%D
%D Q* R |-> .PLABEL= _(0.42) =:\;k^\flat
%D Q* R |-> .PLABEL= _(0.58) h
%D Q åR |-> .PLABEL= ^(0.43) k
%D Q åR |-> .PLABEL= ^(0.57) h^\sharp\;:=
%D Q* åR harrownodes nil 20 nil <-| sl^
%D Q* åR harrownodes nil 20 nil |-> sl_
%D Q* R midpoint x+= -20 .TeX= \lpcded{Pi-delta-flat-dnc} place
%D Q åR midpoint x+= 20 .TeX= \rpcded{Pi-delta-sharp-dnc} place
%D
%D R R' |-> .plabel= l r
%D åR åR' |-> .plabel= r å_r\;:=
%D R åR' harrownodes nil 20 nil |->
%D åR åR' midpoint x+= 20 .TeX= \rpcded{Pi-delta-dnc} place
%D
%D b a -> .plabel= a \dd
%D ))
%D enddiagram
%D
$$\diag{adjs-to-delta*-dnc}$$
% $$\diag{adjs-to-delta*-dnc}
% \qquad
% \begin{array}{ccc}
% & \ded{Sigma-delta-dnc} \\ \\
% \ded{Sigma-delta-sharp-dnc} & \ded{Sigma-delta-flat-dnc} \\ \\
% \ded{Pi-delta-flat-dnc} & \ded{Pi-delta-sharp-dnc} \\ \\
% & \ded{Pi-delta-dnc} \\ \\
% \end{array}
% $$
%:
%:
%: b=b'∧P'ab
%: ---------
%: b=b'∧P'ab P'ab
%: --------- :::p
%: b=b' Pab
%: ------------
%: b=b'∧Pab
%:
%: ^Sigma-delta-dnc
%:
%: b=b'∧Pab
%: ---------
%: [b=b'∧Pab]^1 b=b'∧Pab Pab
%: :::::f -------- ::::g
%: b=b∧Pab Qabb' b=b' Qabb
%: --------------¯{subst};1 --------------=E
%: Qabb Qabb'
%:
%: ^Sigma-delta-sharp-dnc ^Sigma-delta-flat-dnc
%:
%: [Qabb']^1 [b=b']^1 Qabb'
%: ::::::::k ----------=E'
%: Qabb b=b'⊃Rab Qabb
%: ---=I ---------------¯{subst};1 ::::h
%: b=b b=b⊃Rab Rab
%: ------------------ --------1
%: Rab b=b'⊃Rab
%:
%: ^Pi-delta-flat-dnc ^Pi-delta-sharp-dnc
%:
%: [b=b']^1 b=b'⊃Rab
%: ----------------
%: Rab
%: :::r
%: R'ab
%: ---------1
%: b=b'⊃R'ab
%:
%: ^Pi-delta-dnc
%:
% --------------------
% «adjs-to-cob-generic» (to ".adjs-to-cob-generic")
% (s "Adjoints to change-of-base: generic" "adjs-to-cob-generic")
\myslide {Adjoints to change-of-base: generic} {adjs-to-cob-generic}
%:*=*{=}*
%:*∧*{∧}*
%:*⊃*{⊃}*
%D diagram adjs-to-f*-dnc
%D 2Dx 100 +40
%D 2D 100 100 P' ===> ÆP'
%D 2D - -
%D 2D | |-> |
%D 2D v v
%D 2D +70 +30 P ====> ÆP
%D 2D - -
%D 2D | |-> |
%D 2D | <-| |
%D 2D v v
%D 2D +70 +30 Q* <=== Q
%D 2D - -
%D 2D | <-| |
%D 2D | |-> |
%D 2D v v
%D 2D +70 +30 R ====> åR
%D 2D - -
%D 2D | |-> |
%D 2D v v
%D 2D +70 +30 R' ===> åR'
%D 2D
%D 2D +20 +20 b |---> a
%D 2D
%D (( P' .tex= P'x ÆP' .tex= Îx.tx=y∧P'x =>
%D P .tex= Px ÆP .tex= Îx.tx=y∧Px =>
%D Q* .tex= Qtx Q .tex= Qy <=
%D R .tex= Rx åR .tex= ýx.tx=y⊃Rx =>
%D R' .tex= R'x åR' .tex= ýx.tx=y⊃R'x =>
%D b .tex= x a .tex= y
%D ))
%D (( P' P |-> .plabel= l p
%D ÆP' ÆP |-> .plabel= r Æ_fp\;:=
%D P' ÆP harrownodes nil 20 nil |->
%D ÆP' ÆP midpoint x+= 20 .TeX= \rpcded{Sigma-t-dnc} place
%D
%D P Q* |-> .PLABEL= _(0.42) g
%D P Q* |-> .PLABEL= _(0.58) =:\;f^\sharp
%D ÆP Q |-> .PLABEL= ^(0.41) g^\flat\;:=
%D ÆP Q |-> .PLABEL= ^(0.59) f
%D P Q harrownodes nil 20 nil |-> sl^
%D P Q harrownodes nil 20 nil <-| sl_
%D P Q* midpoint x+= -20 .TeX= \lpcded{Sigma-t-sharp-dnc} place
%D ÆP Q midpoint x+= 20 .TeX= \rpcded{Sigma-t-flat-dnc} place
%D
%D Q* R |-> .PLABEL= _(0.42) =:\;k^\flat
%D Q* R |-> .PLABEL= _(0.58) h
%D Q åR |-> .PLABEL= ^(0.43) k
%D Q åR |-> .PLABEL= ^(0.57) h^\sharp\;:=
%D Q* åR harrownodes nil 20 nil <-| sl^
%D Q* åR harrownodes nil 20 nil |-> sl_
%D Q* R midpoint x+= -20 .TeX= \lpcded{Pi-t-flat-dnc} place
%D Q åR midpoint x+= 20 .TeX= \rpcded{Pi-t-sharp-dnc} place
%D
%D R R' |-> .plabel= l r
%D åR åR' |-> .plabel= r å_fr\;:=
%D R åR' harrownodes nil 20 nil |->
%D åR åR' midpoint x+= 20 .TeX= \rpcded{Pi-t-dnc} place
%D
%D b a -> .plabel= a \dd
%D ))
%D enddiagram
%D
$$\diag{adjs-to-f*-dnc}$$
%:
%:
%: [tx=y∧P'x]^1
%: ------------
%: [tx=y∧P'x]^1 P'x
%: ------------ ::p
%: tx=y Px
%: ----------------
%: tx=y∧Px
%: ------------ÎI
%: tx=y∧P'x Îx.tx=y∧Px
%: ---------------------ÎE
%: Îx.tx=y∧Px
%:
%: ^Sigma-t-dnc
%:
%: [tx=y∧Px]^1
%: ----------
%: § [tx=y∧Px]^1 [tx=y∧Px]^1 Px
%: ::t^*¯{refl} -----------ÎI ----------- :::g
%: tx=tx Px Îx.tx=y∧Px tx=y Qtx
%: ---------------- ::f =============
%: tx=tx∧Px Qy Îx.tx=y∧Px Qy
%: -------------------¯{subst};1 -------------------ÎE;1
%: Qtx Qy
%:
%: ^Sigma-t-sharp-dnc ^Sigma-t-flat-dnc
%:
%: [tx=y]^1
%: --------¯{sym}
%: y=tx Qy
%: ----------------¯{sub}'
%: Qfx Qtx
%: :::::::::::::t^*k :::h
%: § x ýx'.tx'=tx⊃Rx Rx
%: :t^*¯{refl} ----------------ýE -------1
%: tx=tx tx=tx⊃Rx tx=y⊃Rx
%: ----------------------- ----------ýI
%: Rx ýx.tx=y⊃Rx
%:
%: ^Pi-t-flat-dnc ^Pi-t-sharp-dnc
%:
%: x ýx.tx=y⊃Rx
%: -------------ýE
%: [tx=y]^1 tx=y⊃Rx
%: --------------------
%: Rx
%: ::r
%: R'x
%: --------1
%: tx=y⊃R'x
%: -----------ýI
%: ýx.tx=y⊃R'x
%:
%: ^Pi-t-dnc
%:
%:
% --------------------
% «adjs-to-cob-candidates» (to ".adjs-to-cob-candidates")
% (s "Adjoints to change-of-base: candidates" "adjs-to-cob-candidates")
\myslide {Adjoints to change-of-base: candidates} {adjs-to-cob-candidates}
\def\Eq{\operatorname{Eq}}
\def\EqDB{\Eq_{\DD_B}\!\!\!§\!_B}
\par Remember that:
\par $\DD_B := \ang{\id_B,\id_B} : B \to B×B$,
\par $\dd_{AB} := \ang{\id_{A×B},'_{AB}} : A×B \to (A×B)×B$.
\bsk
\par If $f:A \to B$ and $PÝ\bbE_A$ then we can define
\par $Î_fP := Î_{\pi_{BA}}((\id_B×f)^*\EqDB∧\pi^{\prime*}_{BA}P)$:
%:
%:
%: A->^fB B
%: -------- -----------------
%: B×A->B×B \ssst{b,b'}{b{=}b'} \ssst{a}{Pa}
%: ----------------------------- ------------
%: \ssst{b,a}{b{=}fa} \ssst{b,a}{Pa}
%: -------------------------------------------
%: \ssst{b,a}{b{=}fa∧Pa}
%: ----------------------
%: \ssst{b}{Îa.b{=}fa∧Pa}
%:
%: ^foo
%:
%: f B
%: ------- -----
%: \id_B×f \EqDB P
%: ---------------- -------------------
%: (\id_B×f)^*\EqDB \pi^{\prime*}_{BA}P
%: --------------------------------------
%: (\id_B×f)^*\EqDB∧\pi^{\prime*}_{BA}P
%: ------------------------------------------------
%: Î_{\pi_{BA}}((\id_B×f)^*\EqDB∧\pi^{\prime*}_{BA}P)
%:
%: ^bar
%:
$$\ded{foo} \qquad \ded{bar}$$
\msk
\par If $PÝ\bbE_{A×B}$ then we can define
\par $\Eq_{\dd_{AB}} P := (\pi'_{AB}×\id_B)^*\EqDB∧_{(A×B)B}^*P$:
%:
%:
%: B B
%: ----------------- -----
%: \ssst{b,b'}{b{=}b'} \ssst{a,b}{Pab} \EqDB P
%: ----------------------- -------------------- ------------------------ -------------
%: \ssst{(a,b),b'}{b{=}b'} \ssst{(a,b),b'}{Pab} (\pi'_{AB}×\id_B)^*\EqDB _{(A×B)B}^*P
%: ---------------------------------------------- ---------------------------------------
%: \ssst{(a,b),b'}{b{=}b'∧Pab} (\pi'_{AB}×\id_B)^*\EqDB∧_{(A×B)B}^*P
%:
%: ^foo-abb' ^bar-abb'
%:
$$\ded{foo-abb'} \qquad \ded{bar-abb'}$$
%%%%%
%
% «hyps» (to ".hyps")
%
%%%%%
\def\foo#1{
$$\diag{#1-std}$$
$$\begin{array}{rcl}
\ded{#1nat-short-std} &:=& \ded{#1nat-std} \\ \\
\ded{#1-std} && \\
\end{array}
$$
}
\def\foowide#1{
$$\diag{#1-std}$$
$$\begin{array}{l}
\ded{#1nat-short-std} \qquad := \\
\qquad \ded{#1nat-std} \\ \\
\ded{#1-std} \\
\end{array}
$$
}
% --------------------
% «Pand» (to ".Pand")
% (s "Preservation of `and'" "Pand")
\myslide {Preservation of `and'} {Pand}
\foo{Pand}
% --------------------
% «Pand-2» (to ".Pand-2")
% (s "Preservation of `and' (2)" "Pand-2")
\myslide {Preservation of `and' (2)} {Pand-2}
In the archetypal model, $\CanSub(\Set)$,
the arrows $\Pandnat$ and $\Pand$ exist for trivial reasons:
$f^*P∧f^*Q = \ssst{a}{Pfa∧Qfa} = \ssst{a}{P(f(a))∧Q(f(a))}$ \quad and
$f^*(P∧Q) = \ssst{a}{Pfa∧Qfa} = \ssst{a}{P(f(a))∧Q(f(a))}$
are the {\sl same subobject}.
%D diagram Pand-archetyp
%D 2Dx 100 +70 +70
%D 2D 100 A0 <============ A1
%D 2D ^ ^ ^
%D 2D | \ <-| |
%D 2D - - -
%D 2D +20 A2 <--| A3 <==== A4
%D 2D - - -
%D 2D | / <-| |
%D 2D v v v
%D 2D +20 A5 <============ A6
%D 2D
%D 2D +15 aa |-----------> ab
%D 2D
%D (( A0 .tex= \ssst{a}{Pfa} A1 .tex= \ssst{b}{Pb}
%D A2 .tex= \ssst{a}{Pfa∧Qfa} A3 .tex= \ssst{a}{Pfa∧Qfa} A4 .tex= \ssst{b}{Pb∧Qb}
%D A5 .tex= \ssst{a}{Pfa} A6 .tex= \ssst{b}{Qb}
%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 \Pand 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{Pand-archetyp}$$
\msk
The same will happen for $\Ptrue$ and $\Pimp$,
and for {\sl some forms} of $\Frob$, $\BCCL$ and $\BCCR$
(the details for $\Frob$, $\BCCL$ and $\BCCR$ are in [Seely83])
% --------------------
% «Ptrue» (to ".Ptrue")
% (s "Preservation of `true'" "Ptrue")
\myslide {Preservation of `true'} {Ptrue}
\foo{Ptrue}
% --------------------
% «Pimp» (to ".Pimp")
% (s "Preservation of `implies'" "Pimp")
\myslide {Preservation of `implies'} {Pimp}
\foowide{Pimp}
% --------------------
% «BCCL» (to ".BCCL")
% (s "Beck-Chevalley for the left adjoint" "BCCL")
\myslide {Beck-Chevalley for the left adjoint} {BCCL}
\foo{BCCL}
% --------------------
% «BCCR» (to ".BCCR")
% (s "Beck-Chevalley for the right adjoint" "BCCR")
\myslide {Beck-Chevalley for the right adjoint} {BCCR}
\foo{BCCR}
% --------------------
% «Frobenius» (to ".Frobenius")
% (s "Frobenius" "Frobenius")
\myslide {Frobenius} {Frobenius}
\foo{Frob}
%:
%: f:A->B f:A->B
%: ===========\Ptruenat -----------\Ptrue
%: f^*§_B|-§_A §_A|-f^*§_B
%:
%: ^Ptruenat-short-std ^Ptrue-std
%:
%: f P Q f P Q
%: ===================\Pandnat -------------------\Pand
%: f^*(P∧Q)|-f^*P∧f^*Q f^*P∧f^*Q|-f^*(P∧Q)
%:
%: ^Pandnat-short-std ^Pand-std
%:
%: f Q R f Q R
%: ===================\Pimpnat -------------------\Pimp
%: f^*P∧f^*Q|-f^*(Q⊃R) f^*(Q⊃R)|-f^*P⊃f^*Q
%:
%: ^Pimpnat-short-std ^Pimp-std
%:
%D diagram Ptrue-std
%D 2Dx 100 +30
%D 2D 100 T0 <==== T1
%D 2D -
%D 2D |
%D 2D v
%D 2D +20 T2
%D 2D
%D 2D +15 ta |---> tb
%D 2D
%D (( T0 .tex= f^*§_B T1 .tex= §_B
%D T2 .tex= §_A
%D ta .tex= A tb .tex= B
%D T0 T1 <-|
%D T0 T2 -> sl_ .plabel= l \Ptruenat
%D T0 T2 <- sl^ .plabel= r \Ptrue
%D ta tb -> .plabel= a f
%D ))
%D enddiagram
%:
%: B
%: ---§
%: f §_B
%: ------·^*
%: f^*§_B
%: -----------!
%: f^*§_B|-§_A
%:
%: ^Ptruenat-std
%D diagram Pand-std
%D 2Dx 100 +45 +45
%D 2D 100 A0 <============ A1
%D 2D ^ ^ ^
%D 2D | \ <-| |
%D 2D - - -
%D 2D +20 A2 <--| A3 <==== A4
%D 2D - - -
%D 2D | / <-| |
%D 2D v v v
%D 2D +20 A5 <============ A6
%D 2D
%D 2D +15 aa |-----------> ab
%D 2D
%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 \Pand 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
%:
%: P Q P Q
%: ------ -----'
%: f P∧Q|-P P∧Q|-Q
%: -------------·^* -------------·^*
%: f^*(P∧Q)|-f^*P f^*(P∧Q)|-f^*Q
%: ----------------------------------\ang{,}
%: f^*(P∧Q)|-f^*P∧f^*Q
%:
%: ^Pandnat-std
%D diagram Pimp-std
%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 ((
% (fooi "Q" "R" "P" "Q")
%D B0 .tex= f^*(Q⊃R)&f^*Q B0' .tex= f^*((Q⊃R)&Q) B1 .tex= (Q⊃R)&Q
%D B2 .tex= f^*R B3 .tex= R
%D B4 .tex= f^*(Q⊃R) B5 .tex= Q⊃R
%D B6 .tex= f^*Q⊃f^*R B7 .tex= Q⊃R
%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
%:
%: Q R
%: ----⊃
%: Q⊃R
%: ---\id
%: Q R Q⊃R|-Q⊃R
%: -----⊃ --------\uncur
%: f Q⊃R Q f (Q⊃R)∧Q|-R
%: ---------------------------\Pand ------------·^*
%: f^*(Q⊃R)∧f^*Q|-f^*((Q⊃R)∧Q) f^*((Q⊃R)∧Q)|-f^*R
%: ------------------------------------------------------;
%: f^*(Q⊃R)∧f^*Q|-f^*R
%: -------------------\cur
%: f^*(Q⊃R)|-f^*Q⊃f^*R
%:
%: ^Pimpnat-std
%:
%:
%%%%%
%
% «bcc» (to ".bcc")
%
%%%%%
%:
%: c f c' f' P c f c' f' P
%: ===========================\BCCLnat ---------------------------\BCCL
%: Î_{c'}f^{\prime*}P|-f^*Î_cP f^*Î_cP|-Î_{c'}f^{\prime*}P
%:
%: ^BCCLnat-short-std ^BCCL-std
%:
%: c f c' f' P c f c' f' P
%: ===========================\BCCRnat ---------------------------\BCCR
%: f^*ý_cP|-ý_{c'}f^{\prime*}P ý_{c'}f^{\prime*}P|-f^*ý_cP
%:
%: ^BCCRnat-short-std ^BCCR-std
%:
%D diagram BCCL-std
%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^{\prime*}P B1 .tex= P
%D B2 .tex= c^{\prime*}f^*Î_cP B2' .tex= f^{\prime*}c^*Î_cP B3 .tex= c^*Î_cP
%D B4 .tex= Î_{c'}f^{\prime*}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 \BCCL
%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}C b1 .tex= 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
%D diagram BCCR-std
%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^{\prime*}f^*ý_cP B0' .tex= f^{\prime*}c^*ý_cP B1 .tex= c^*ý_cP
%D B2 .tex= f^{\prime*}P B3 .tex= P
%D B4 .tex= f^*ý_cP B5 .tex= ý_cP
%D B6 .tex= ý_{c'}f^{\prime*}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 \BCCR
%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}C b1 .tex= 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
%:
%: P c
%: ----Î_0
%: Î_cP
%: ----\id
%: Î_cP|-Î_cP
%: ----------Î^\sharp
%: f' P|-c^*Î_cP (f';c)=(c';f) Î_cP
%: --------------------------------·^* ======================================
%: f^{\prime*}P|-f^{\prime*}c^*Î_cP f^{\prime*}c^*Î_cP|-c^{\prime*}f^*Î_cP
%: ---------------------------------------------------------------------------;
%: f^{\prime*}P|-c^{\prime*}f^*Î_cP
%: --------------------------------Î^\flat
%: Î_{c'}f^{\prime*}P|-f^*Î_cP
%:
%: ^BCCLnat-std
%:
%: P c
%: ----ý_0
%: ý_cP
%: ----\id
%: ý_cP|-ý_cP
%: ----------ý^\flat
%: (f';c)=(c';f) ý_cP f' c^*ý_cP|-P
%: ====================================== --------------------------------·^*
%: c^{\prime*}f^*ý_cP|-f^{\prime*}c^*ý_cP f^{\prime*}c^*ý_cP|-f^{\prime*}P
%: ------------------------------------------------------------------------;
%: c^{\prime*}f^*ý_cP|-f^{\prime*}P
%: --------------------------------ý^\sharp
%: f^*ý_cP|-ý_{c'}f^{\prime*}P
%:
%: ^BCCRnat-std
%:
%%%%%
%
% «frobenius» (to ".frobenius")
%
%%%%%
%:
%: f P Q f P Q
%: =====================\Frobnat ---------------------\Frob
%: Î_f(P∧f^*Q)|-(Î_fP)∧Q Î_f(P∧f^*Q)|-(Î_fP)∧Q
%:
%: ^Frobnat-short-std ^Frob-std
%:
%D diagram Frob-std
%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= Î_fP
%D B2 .tex= P&f^*Q B3 .tex= Î_f(P&f^*Q) B3' .tex= (Î_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
%:
%: f Q f Q
%: ---·^* ----·^*
%: P f^*Q P f^*Q
%: --------- ------------'
%: P∧f^*Q|-P f P∧f^*Q|-f^*Q
%: -----------------Î_f --------------{Î_f}^\flat
%: Î_f(P∧f^*Q)|-Î_fP Î_f(P∧f^*Q)|-Q
%: -------------------------------------\ang{,}
%: Î_f(P∧f^*Q)|-(Î_fP)∧Q
%:
%: ^Frobnat-std
%:
% --------------------
% «cheap-hyps» (to ".cheap-hyps")
% (s "Cheap hyperdoctrines" "cheap-hyps")
\myslide {Cheap hyperdoctrines} {cheap-hyps}
A {\sl cheap hyperdoctrine} is a structure like this:
$$\def\lside{\bbH=(}
\def\lphantom{\phantom{\lside}}
%
\begin{array}{l}
\lside \bbB, ×, 1, \to, \\
\lphantom \bbE, ∧, §, ⊃, \\
\lphantom p, Ð{cleavage}, \\
\lphantom \Pand, \Ptrue, \Pimp, \\
\lphantom Î_ \dashv * \dashv ý_p, \\
\lphantom \Eq_\DD \dashv \DD^*, \\
\lphantom \BCCex_\pi, \BCCfa_\pi) \\
\end{array}
$$
Note that $\Frob$ does not appear,
and that $\BCCL$ and $\BCCR$ are stated only for
very special cases --- $\BCCex$, $\BCCfa$, $\BCCeq$
(details soon!)
% --------------------
% «pimp-implies-frob» (to ".pimp-implies-frob")
% (s "Pimp implies Frob" "pimp-implies-frob")
\myslide {Pimp implies Frob} {pimp-implies-frob}
\par {\sl Fact:} we can reconstruct $\Frob$ from $\Pimp$.
\par (Note: this is a yellow-belt categorical proof,
\par but for some reason I find it difficult)
\par First we need a derived rule:
%:
%: Î_f(P∧f^*Q)|-R
%: ------------Î^\sharp
%: P∧f^*Q|-f^*R
%: ------------⊃^\sharp
%: P|-f^*Q⊃f^*R
%: ===========;\Pimp
%: P|-f^*(Q⊃R)
%: ---------Î^\flat
%: Î_f(P∧f^*Q)|-R Î_fP|-Q⊃R
%: ==============\Pimp' ---------⊃^\flat
%: Î_fP∧Q|-R := Î_fP∧Q|-R
%:
%: ^frob-from-pimp-1 ^frob-from-pimp-2
%:
$$\ded{frob-from-pimp-1} \quad := \quad \ded{frob-from-pimp-2}$$
%
\par where `$;\Pimp$' is composition with `$\Pimp$', as below.
\par Note that all the bars in the derivation at the right above
\par are bijections; the inverse of `$;\Pimp$' is `$;\Pimpnat$'.
%:
%:
%: f Q R
%: -------------------\Pimp
%: P|-f^*Q⊃f^*R P|-f^*Q⊃f^*R f^*Q⊃f^*R|-f^*(Q⊃R)
%: ===========;\Pimp -----------------------------------;
%: P|-f^*(Q⊃R) := P|-f^*(Q⊃R)
%:
%: ^;Pimp1 ^;Pimp2
%:
%:
%: f Q R
%: ===================\Pimpnat
%: P|-f^*(Q⊃R) P|-f^*(Q⊃R) f^*(Q⊃R)|-f^*Q⊃f^*R
%: ===========;\Pimpnat -----------------------------------;
%: P|-f^*Q⊃f^*R := P|-f^*Q⊃f^*R
%:
%: ^;Pimpnat1 ^;Pimpnat2
%:
$$\ded{;Pimp1} \quad := \quad \ded{;Pimp2}$$
$$\ded{;Pimpnat1} \quad := \quad \ded{;Pimpnat2}$$
\msk
\par Now make $R := Î_f(P∧f^*Q)$.
\par We get the tree at the right, below,
\par that becomes our definition of $\Frob$
\par as a derived rule (involving $\Pimp$).
%:
%: f P Q
%: ===========
%: Î_f(P∧f^*Q)
%: ------------------------\id
%: f P Q Î_f(P∧f^*Q)|-Î_f(P∧f^*Q)
%: ===================\Frob ========================\Pimp'
%: Î_fP∧Q|-Î_f(P∧f^*Q) := Î_fP∧Q|-Î_f(P∧f^*Q)
%:
%: ^frob-from-pimp-3 ^frob-from-pimp-4
%:
$$\ded{frob-from-pimp-3} \quad := \quad \ded{frob-from-pimp-4}$$
% --------------------
% «pimp-implies-frob-2» (to ".pimp-implies-frob-2")
% (s "Pimp implies Frob (2)" "pimp-implies-frob-2")
\myslide {Pimp implies Frob (2)} {pimp-implies-frob-2}
\msk
% (find-angg ".emacs.papers" "lawvere")
% (find-lawvere70page 6 "Substitutivity of equality")
% {\sl Remark:} $\Pimp \funto \Frob$ is $(2)\funto(1)$ in p.6 of [Lawvere70].
\par Here is the construction as a diagram.
\par We start with $R:=Î_f(P∧f^*Q)$ and with the arrow marked `$(\id)$',
\par and we build the arrow $Î_fP∧Q \vdash R = Î_f(P∧f^*Q)$, that is `$\Frob$'.
%D diagram frob-and-pimp
%D 2Dx 100 +40 +35 +40
%D 2D 100 Î_fP∧Q <--------| Î_fP # 0 1
%D 2D ^ | \ ^ \ # 8 2 3
%D 2D | | \ | \ #
%D 2D | v v | v # 4 5 9
%D 2D +25 Î_f(P∧f^*Q) -> R |----------> Q⊃R # 6 7
%D 2D ^ - | -
%D 2D | | | |
%D 2D - | - v
%D 2D +35 P∧f^*Q <---|----| P --> f^*(Q⊃R)
%D 2D \ | \ ^ -
%D 2D \ | \ | |
%D 2D v v v | v
%D 2D +25 f^*R |-------> f^*Q⊃f^*R
%D 2D
%D (( Î_fP∧Q Î_fP
%D R Q⊃R
%D P∧f^*Q P
%D f^*R f^*Q⊃f^*R
%D
%D Î_f(P∧f^*Q)
%D f^*(Q⊃R)
%D @ 0 @ 1 <-|
%D @ 0 @ 8 -> sl_ .plabel= l \Frob @ 0 @ 8 <- sl^ .plabel= r \nat
%D @ 0 @ 2 -> @ 1 @ 3 ->
%D @ 8 @ 2 -> .plabel= b (\id) @ 2 @ 3 |->
%D @ 8 @ 4 <-| @ 1 @ 5 <-|
%D @ 2 @ 6 |-> @ 3 @ 9 |->
%D @ 4 @ 5 <-| @ 5 @ 9 ->
%D @ 4 @ 6 -> @ 5 @ 7 ->
%D @ 9 @ 7 -> sl_ .plabel= l \nat @ 9 @ 7 <- sl^ .plabel= r \Pimp
%D @ 6 @ 7 |->
%D
%D @ 0 @ 3 harrownodes nil 20 4 <- sl^ .plabel= a ⊃^\flat
%D @ 0 @ 3 harrownodes 4 20 nil -> sl_ .plabel= b ⊃^\sharp
%D
%D @ 0 @ 6 varrownodes 6 20 nil <- sl_ .plabel= l Î^\flat
%D @ 0 @ 6 varrownodes 9 20 nil -> sl^ .plabel= r Î^\sharp
%D
%D @ 1 @ 7 varrownodes nil 20 4 <- sl_ .plabel= l Î^\flat
%D @ 1 @ 7 varrownodes nil 20 2 -> sl^ .plabel= r Î^\sharp
%D
%D @ 4 @ 7 harrownodes nil 20 4 <- sl^ .plabel= a ⊃^\flat
%D @ 4 @ 7 harrownodes 4 20 nil -> sl_ .plabel= b ⊃^\sharp
%D ))
%D enddiagram
%D
$$\diag{frob-and-pimp}$$
% --------------------
% «pimp-implies-frob-3» (to ".pimp-implies-frob-3")
% (s "Pimp implies Frob (3)" "pimp-implies-frob-3")
\myslide {Pimp implies Frob (3)} {pimp-implies-frob-3}
In the notation of [Lawvere70] (p.6), this is stated and proved as:
\bsk
{\sc Definition-Theorem.} {\sl In any eed, the following are equivalent:}
\ssk
(1) Frobenius Reciprocity holds,
(2) For any $f:X \to Y$, $\aa$, $\psi$ in $P(Y)$
\quad
$f·(\aa \funto \psi) \diagxyto/->/<200>^\approx f·\aa \funto f·\psi$
(3) For any $f:X \to Y$, $\psi \in P(X)$, $\aa \in P(Y)$
\quad
$((f·\aa) ∧ \phi)Æf \diagxyto/->/<200>^\approx \aa∧(\phiÆf)$
\msk
{\sc Proof.} The second conditions means that the diagram of functors
(**) commutes up to natural equivalence. Hence replacing each functor
by its left adjoint also yields a diagram which commutes up to
canonical natural equivalence: (*). But the latter is just the third
condition. Conversely if the third condition holds, we can replace the
functors in the latter diagram by their right adjoints, yielding the
second condition.
%
%D diagram frob-and-pimp-lawvere70
%D 2Dx 100 +40 +35 +40
%D 2D 100 Î_fP∧Q <--------| Î_fP # 0 1
%D 2D ^ | \ ^ \ # 8 2 3
%D 2D | | \ | \ #
%D 2D | v v | v # 4 5 9
%D 2D +25 Î_f(P∧f^*Q) -> R |----------> Q⊃R # 6 7
%D 2D ^ - | -
%D 2D | | | |
%D 2D - | - v
%D 2D +35 P∧f^*Q <---|----| P --> f^*(Q⊃R)
%D 2D \ | \ ^ -
%D 2D \ | \ | |
%D 2D v v v | v
%D 2D +25 f^*R |-------> f^*Q⊃f^*R
%D 2D
%D (( Î_fP∧Q Î_fP
%D R Q⊃R
%D P∧f^*Q P
%D f^*R f^*Q⊃f^*R
%D
%D Î_f(P∧f^*Q)
%D f^*(Q⊃R)
%D
%D R .tex= \psi
%D Q⊃R .tex= \aa=>\psi
%D f^*(Q⊃R) .tex= f·(\aa=>\psi)
%D f^*R .tex= f·\psi
%D f^*Q⊃f^*R .tex= f·\aa=>f·\psi
%D P .tex= \phi
%D P∧f^*Q .tex= (f·\aa)∧\phi
%D Î_f(P∧f^*Q) .tex= ((f·\aa)∧\phi)Æf
%D Î_fP .tex= \phiÆf
%D Î_fP∧Q .tex= \aa∧\phiÆf
%D
%D @ 0 @ 1 <-|
%D @ 0 @ 8 -> sl_ .plabel= l \Frob @ 0 @ 8 <- sl^ .plabel= r \nat
%D @ 0 @ 2 -> @ 1 @ 3 ->
%D @ 8 @ 2 -> .plabel= b (\id) @ 2 @ 3 |->
%D @ 8 @ 4 <-| @ 1 @ 5 <-|
%D @ 2 @ 6 |-> @ 3 @ 9 |->
%D @ 4 @ 5 <-| @ 5 @ 9 ->
%D @ 4 @ 6 -> @ 5 @ 7 ->
%D @ 9 @ 7 -> sl_ .plabel= l \nat @ 9 @ 7 <- sl^ .plabel= r \Pimp
%D @ 6 @ 7 |->
%D
%D @ 0 @ 3 harrownodes nil 20 4 <- sl^ .plabel= a =>^\flat
%D @ 0 @ 3 harrownodes 4 20 nil -> sl_ .plabel= b =>^\sharp
%D
%D @ 0 @ 6 varrownodes 6 20 nil <- sl_ .plabel= l Æ^\flat
%D @ 0 @ 6 varrownodes 9 20 nil -> sl^ .plabel= r Æ^\sharp
%D
%D @ 1 @ 7 varrownodes nil 20 4 <- sl_ .plabel= l Æ^\flat
%D @ 1 @ 7 varrownodes nil 20 2 -> sl^ .plabel= r Æ^\sharp
%D
%D @ 4 @ 7 harrownodes nil 20 4 <- sl^ .plabel= a =>^\flat
%D @ 4 @ 7 harrownodes 4 20 nil -> sl_ .plabel= b =>^\sharp
%D ))
%D enddiagram
%D
%D diagram frob-and-pimp-lawvere70-squares
%D 2Dx 100 +35 +25
%D 2D 100 A0 A1
%D 2D +15 (*)
%D 2D +15 A2 A3
%D 2D
%D 2D +20 B0 B1
%D 2D +15 (**)
%D 2D +15 B2 B3
%D 2D
%D (( A0 .tex= P(Y) A1 .tex= P(Y)
%D A2 .tex= P(X) A3 .tex= P(X)
%D A0 A1 <- .plabel= a \aa∧(\;)
%D A0 A2 <- .plabel= l (\;)Æf
%D A1 A3 <- .plabel= r (\;)Æf
%D A2 A3 <- .plabel= a (f·\aa)∧(\;)
%D (*) place
%D ))
%D (( B0 x+= 8
%D B1 x+= 8
%D B2 x+= 8
%D B3 x+= 8
%D (**) x+= 8
%D ))
%D (( B0 .tex= P(Y) B1 .tex= P(Y)
%D B2 .tex= P(X) B3 .tex= P(X)
%D B0 B1 -> .plabel= a \aa=>(\;)
%D B0 B2 -> .plabel= l f·(\;)
%D B1 B3 -> .plabel= r f·(\;)
%D B2 B3 -> .plabel= a (f·\aa)=>(\;)
%D (**) place
%D ))
%D enddiagram
%D
$$\diag{frob-and-pimp-lawvere70}
% \quad
\hskip -7pt
\diag{frob-and-pimp-lawvere70-squares}
$$
\bsk
\bsk
\par Note that he only draws the squares (*) and (**),
\par with the categories and the functors;
\par the cube with objects, morphisms, and `$\mto$'s for functors
\par is a kind of ``internal view'' of the categories and functors involved ---
\par and such ``internal views'' are only very rarely drawn
\par in the (standard?) Category Theory literature.
% --------------------
% «BCCL-implies-BCCR» (to ".BCCL-implies-BCCR")
% (s "BCCL implies BCCR" "BCCL-implies-BCCR")
\myslide {BCCL implies BCCR} {BCCL-implies-BCCR}
\par Also, $\BCCL$ implies $\BCCR$ (and vice-versa),
\par by an argument similar to the previous one.
\par Here are the diagrams; we won't get into the details.
%D diagram BCCL-implies-BCCR-0
%D 2Dx 100 +25
%D 2D 100 X Y
%D 2D
%D 2D +25 Z W
%D 2D
%D (( X Y -> .plabel= a a
%D X Z -> .plabel= l l
%D Y W -> .plabel= r r
%D Z W -> .plabel= b b
%D X relplace 7 7 \pbsymbol{7}
%D ))
%D enddiagram
%D
%D diagram BCCL-implies-BCCR
%D 2Dx 100 +40 +35 +40
%D 2D 100 l^*Q |------> ý_al^*Q # 0 1
%D 2D ^ ^ ^ | ^ # 2 3 8
%D 2D / | /BCCR| | #
%D 2D / | / v | # 9 4 5
%D 2D +25 a^*P <--------| P --> r^*ý_bQ # 6 7
%D 2D - | - ^
%D 2D | | | |
%D 2D v - | -
%D 2D +35 Î_la^*P --> Q |---|----> ý_bQ
%D 2D | ^ ^ | ^
%D 2D nat| |BCCL/ | /
%D 2D v | / v /
%D 2D +25 b^*Î_rP <------| Î_rP
%D 2D
%D (( l^*Q ý_al^*Q
%D a^*P P
%D Q ý_bQ
%D b^*Î_rP Î_rP
%D
%D r^*ý_bQ
%D Î_la^*P
%D @ 4 @ 0 |-> @ 0 @ 1 |->
%D @ 4 @ 5 |-> @ 5 @ 8 |->
%D @ 3 @ 2 |-> @ 2 @ 9 |->
%D @ 3 @ 7 |-> @ 7 @ 6 |->
%D @ 2 @ 0 -> @ 3 @ 1 -> .plabel= l (\id)
%D @ 6 @ 4 -> @ 7 @ 5 ->
%D @ 3 @ 8 -> @ 9 @ 4 ->
%D @ 9 @ 6 -> sl_ .plabel= l \nat @ 9 @ 6 <- sl^ .PLABEL= ^(0.34) \BCCL
%D @ 1 @ 8 -> sl_ .PLABEL= _(0.65) \BCCR @ 1 @ 8 <- sl^ .plabel= r \nat
%D
%D @ 0 @ 3 harrownodes 4 20 nil -> sl^ .plabel= a ý^\sharp
%D @ 0 @ 3 harrownodes nil 20 4 <- sl_ .plabel= b ý^\flat
%D
%D @ 0 @ 6 varrownodes nil 20 6 -> sl_ .plabel= l Î^\flat
%D @ 0 @ 6 varrownodes nil 20 9 <- sl^ .plabel= r Î^\sharp
%D
%D @ 1 @ 7 varrownodes 4 20 nil -> sl_ .plabel= l Î^\flat
%D @ 1 @ 7 varrownodes 2 20 nil <- sl^ .plabel= r Î^\sharp
%D
%D @ 4 @ 7 harrownodes 4 20 nil -> sl^ .plabel= a ý^\sharp
%D @ 4 @ 7 harrownodes nil 20 4 <- sl_ .plabel= b ý^\flat
%D ))
%D enddiagram
%D
$$\diag{BCCL-implies-BCCR-0}
\qquad
\diag{BCCL-implies-BCCR}
$$
% --------------------
% «equality-lemmas» (to ".equality-lemmas")
% (s "Lemmas about equality" "equality-lemmas")
\myslide {Lemmas about equality} {equality-lemmas}
%:*∧*∧*
%D diagram frob-lemma-0
%D 2Dx 100 +45 +45 +20
%D 2D 100 E0 E1
%D 2D +20 E2 E3 E4
%D 2D +20 E5 E6 E7
%D 2D +15 B0 B1 B2
%D 2D
%D (( E0 .tex= P E1 .tex= Æ_fP
%D E2 .tex= P∧f^*Q E3 .tex= Æ_f(P∧f^*Q) E4 .tex= Æ_fP∧Q
%D E5 .tex= f^*Q E6 .tex= Q E7 .tex= E7
%D B0 .tex= A B1 .tex= B B2 .tex= B2
%D E0 E1 |->
%D E2 E0 -> E3 E1 -> E4 E1 ->
%D E2 E3 |-> E3 E4 <->
%D E2 E5 -> E3 E6 -> E4 E6 ->
%D E5 E6 <-| # E6 E7 <-|
%D B0 B1 -> .plabel= a f # B1 B2 -> .plabel= a g
%D # B0 B2 -> sl__ .plabel= b \id
%D ))
%D enddiagram
%D diagram frob-lemma-1
%D 2Dx 100 +35 +40 +20
%D 2D 100 E0 E1
%D 2D +20 E2 E3 E4
%D 2D +20 E5 E6 E7
%D 2D +15 B0 B1 B2
%D 2D
%D (( E0 .tex= P E1 .tex= Æ_fP
%D E2 .tex= P∧R E3 .tex= Æ_f(P∧R) E4 .tex= Æ_fP∧R
%D E5 .tex= R E6 .tex= g^*R E7 .tex= R
%D B0 .tex= A B1 .tex= B B2 .tex= A
%D E0 E1 |->
%D E2 E0 -> E3 E1 -> E4 E1 ->
%D E2 E3 |-> E3 E4 <->
%D E2 E5 -> E3 E6 -> E4 E6 ->
%D E5 E6 <-| E6 E7 <-|
%D B0 B1 -> .plabel= a f B1 B2 -> .plabel= a g
%D B0 B2 -> sl__ .plabel= b \id
%D ))
%D enddiagram
%D diagram frob-lemma-2
%D 2Dx 100 +45 +40 +20
%D 2D 100 E0 E1
%D 2D +20 E2 E3 E4
%D 2D +20 E5 E6 E7
%D 2D +15 B0 B1 B2
%D 2D
%D (( E0 .tex= § E1 .tex= Æ_f§
%D E2 .tex= f^*Q E3 .tex= Æ_ff^*Q E4 .tex= Æ_f§∧Q
%D E5 .tex= f^*Q E6 .tex= Q E7 .tex= E7
%D B0 .tex= A B1 .tex= B B2 .tex= B2
%D E0 E1 |->
%D E2 E0 -> E3 E1 -> E4 E1 ->
%D E2 E3 |-> E3 E4 <->
%D E2 E5 -> E3 E6 -> E4 E6 ->
%D E5 E6 <-| # E6 E7 <-|
%D B0 B1 -> .plabel= a f # B1 B2 -> .plabel= a g
%D # B0 B2 -> sl__ .plabel= b \id
%D ))
%D enddiagram
%D diagram frob-lemma-3
%D 2Dx 100 +35 +40 +20
%D 2D 100 E0 E1
%D 2D +20 E2 E3 E4
%D 2D +20 E5 E6 E7
%D 2D +15 B0 B1 B2
%D 2D
%D (( E0 .tex= § E1 .tex= Æ_f§
%D E2 .tex= R E3 .tex= Æ_fR E4 .tex= Æ_f§∧R
%D E5 .tex= R E6 .tex= g^*R E7 .tex= R
%D B0 .tex= A B1 .tex= B B2 .tex= A
%D E0 E1 |->
%D E2 E0 -> E3 E1 -> E4 E1 ->
%D E2 E3 |-> E3 E4 <->
%D E2 E5 -> E3 E6 -> E4 E6 ->
%D E5 E6 <-| E6 E7 <-|
%D B0 B1 -> .plabel= a f B1 B2 -> .plabel= a g
%D B0 B2 -> sl__ .plabel= b \id
%D ))
%D enddiagram
%D diagram frob-lemma-5
%D 2Dx 100 +30 +45 +30
%D 2D 100 E0 E1
%D 2D +20 E2 E3 E4
%D 2D +20 E5 E6 E7
%D 2D +15 B0 B1 B2
%D 2D
%D (( E0 .tex= § E1 .tex= Æ_f§
%D E2 .tex= f^*Q E3 .tex= Æ_ff^*Q E4 .tex= Æ_f§∧g^*f^*Q
%D E5 .tex= f^*Q E6 .tex= g^*f^*Q E7 .tex= f^*Q
%D B0 .tex= A B1 .tex= B B2 .tex= A
%D E0 E1 |->
%D E2 E0 -> E3 E1 -> E4 E1 ->
%D E2 E3 |-> E3 E4 <->
%D E2 E5 -> E3 E6 -> E4 E6 ->
%D E5 E6 <-| E6 E7 <-|
%D B0 B1 -> .plabel= a f B1 B2 -> .plabel= a g
%D B0 B2 -> sl__ .plabel= b \id
%D ))
%D enddiagram
%D diagram frob-lemmas
%D 2Dx 100 +125
%D 2D 100 Frob0 Frob1
%D 2D +80 Frob2 Frob3
%D 2D +80 Frob5
%D 2D
%D (( Frob0 .tex= \diag{frob-lemma-0} BOX
%D Frob1 .tex= \diag{frob-lemma-1} BOX
%D Frob2 .tex= \diag{frob-lemma-2} BOX
%D Frob3 .tex= \diag{frob-lemma-3} BOX
%D Frob5 .tex= \diag{frob-lemma-5} BOX
%D
%D Frob0 x+= 0 y+= -3.5 place Frob1 x+= 0 place
%D Frob2 x+= 3 y+= -3.5 place Frob3 x+= 3 place
%D Frob5 x+= 8 place
%D
%D ))
%D enddiagram
%D
$$\diag{frob-lemmas}$$
%D diagram frob-lemmas-substs
%D 2Dx 100 +65
%D 2D 100 Frob0 Frob1
%D 2D
%D 2D +35 Frob2 Frob3
%D 2D
%D 2D +35 Frob5
%D 2D
%D (( Frob0 .tex= Ð{Frob0}
%D Frob1 .tex= Ð{Frob1}
%D Frob2 .tex= Ð{Frob2}
%D Frob3 .tex= Ð{Frob3}
%D Frob5 .tex= Ð{Frob5}
%D Frob0 Frob1 -> .plabel= b \flbox{Q}{g^*R}{f^*g^*R}{R}
%D Frob0 Frob2 -> .plabel= l \flbox{P}{§}{§∧f^*Q}{f^*Q}
%D Frob1 Frob3 -> .plabel= r \flbox{P}{§}{§∧f^*Q}{f^*Q}
%D Frob2 Frob3 -> .plabel= b \flbox{Q}{g^*R}{f^*g^*R}{R}
%D Frob3 Frob5 -> .plabel= r \flbox{R}{f^*Q}{f^*g^*f^*Q}{f^*Q}
%D ))
%D enddiagram
%D
$$\def\flbox#1#2#3#4{\begin{array}{c} #1 := #2 \\ #3 :\cong #4 \end{array}}
\diag{frob-lemmas-substs}
$$
%:*∧*{∧}*
% --------------------
% «lambda-calc-in-a-hyp» (to ".lambda-calc-in-a-hyp")
% (s "$ð$-calculus in a hyperdoctrine" "lambda-calc-in-a-hyp")
\myslide {$ð$-calculus in a hyperdoctrine} {lambda-calc-in-a-hyp}
\par As the base category $\bbB$ of a hyperdoctrine is a CCC
\par we can interpret $ð$-calculus in it.
\par In diagrams:
%D diagram CCC-HL1
%D 2Dx 100 +30 +30 +25 +30 +30
%D 2D 100 P0 T0 E0 E1
%D 2D
%D 2D +30 P1 P2 P3 T1 E2 E3
%D 2D
%D (( P0 .tex= A P1 .tex= B P2 .tex= B×C P3 .tex= C
%D P0 P1 -> .plabel= a f
%D P0 P2 -> .plabel= m \ang{f,g}
%D P0 P3 -> .plabel= a g
%D P1 P2 <- .plabel= b \pi
%D P2 P3 -> .plabel= b \pi'
%D ))
%D (( T0 .tex= A T1 .tex= 1 -> .plabel= l !
%D ))
%D (( E0 .tex= A×B E1 .tex= A
%D E2 .tex= C E3 .tex= B{->}C
%D E0 E1 <-|
%D E0 E2 -> .PLABEL= _(0.43) \uncur"g
%D E0 E2 -> .PLABEL= _(0.57) f
%D E1 E3 -> .PLABEL= ^(0.43) g
%D E1 E3 -> .PLABEL= ^(0.57) \cur"f
%D E0 E3 harrownodes nil 20 nil <-| sl^
%D E0 E3 harrownodes nil 20 nil |-> sl_
%D E2 E3 |->
%D ))
%D enddiagram
%D
$$\diag{CCC-HL1}$$
%D diagram CCC-HL2
%D 2Dx 100 +30 +30 +25 +30 +30 +35
%D 2D 100 P0 T0 E0 E1 E0'
%D 2D
%D 2D +30 P1 P2 P3 T1 E2 E3 E2'
%D 2D
%D (( P0 .tex= A P1 .tex= B P2 .tex= B{×}C P3 .tex= C
%D P0 P1 -> .plabel= a a|-b
%D P0 P2 -> .plabel= m a|-\ang{b,c}
%D P0 P3 -> .plabel= a a|-c
%D P1 P2 <- .plabel= b p|-b
%D P2 P3 -> .plabel= b p|-b'
%D ))
%D (( T0 .tex= A T1 .tex= 1 -> .plabel= l a|-*
%D ))
% %D (( E0' .tex= (B{->}C){×}B E2' .tex= C
% %D E0' E2' -> .plabel= c \ev_{BC}
% %D ))
%D (( E0 .tex= A×B E1 .tex= A
%D E2 .tex= C E3 .tex= B{->}C
%D E0 E1 <-|
%D E0 E2 -> .PLABEL= _(0.43) a,b|-fb
%D E0 E2 -> .PLABEL= _(0.57) a,b|-c
%D E1 E3 -> .PLABEL= ^(0.43) a|-f
%D E1 E3 -> .PLABEL= ^(0.57) a|-ðb¨B.c
%D E0 E3 harrownodes nil 20 nil <-| sl^
%D E0 E3 harrownodes nil 20 nil |-> sl_
%D E2 E3 |->
%D ))
%D enddiagram
%D
$$\diag{CCC-HL2}$$
In a sequent-calculus-like form:
%:
%: B C a|-b a|-c B C B C
%: ----×_0 ------------\ang{,} ---- -----'
%: B×C a|-\ang{b,c} p|-p p|-'p
%:
%: ^HL-x0 ^HL-ang ^HL-pi ^HL-pi'
%:
%: A
%: -1 ----!
%: 1 a|-*
%:
%: ^HL-1 ^HL-!
%:
%: B C B C a,b|-c
%: ----{->}_0 ----\app ---------\cur
%: B{->}C b,f|-fb a|-ðb¨B.c
%:
%: ^HL-->0 ^HL-ev ^HL-cur
%:
$$\begin{array}{cccc}
\ded{HL-x0} & \ded{HL-ang} & \ded{HL-pi} & \ded{HL-pi'} \\ \\
\ded{HL-1} & \ded{HL-!} \\ \\
\ded{HL-->0} & \ded{HL-ev} & \ded{HL-cur} \\
\end{array}
$$
% (find-LATEXfile "proof.sty" "\\def\\DeduceSym")
\makeatletter
\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
\vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
\vbox{\hbox{.}\hbox{.}}\hbox{.}}}
\makeatother
In natural deduction form (in downcased notation):
%:
%: a a
%: : :
%: b c b,c b,c
%: ----\ang{,} --- ---'
%: b,c b c
%:
%: ^HLD-1 ^HLD-2 ^HLD-3
%:
%: a
%: -!
%: *
%:
%: ^HLD-4
%:
%: a a a [b]^1
%: : : ::::
%: b b|->c c
%: ---------\app -----ð;1
%: c b|->c
%:
%: ^HLD-5 ^HLD-6
%:
$$\begin{array}{cccc}
\ded{HLD-1} & \ded{HLD-2} & \ded{HLD-3} \\ \\
\ded{HLD-4} \\ \\
\ded{HLD-5} & \ded{HLD-6} \\
\end{array}
$$
% --------------------
% «prop-calc-in-a-hyp» (to ".prop-calc-in-a-hyp")
% (s "Propositional calculus in a hyperdoctrine" "prop-calc-in-a-hyp")
\myslide {Propositional calculus in a hyperdoctrine} {prop-calc-in-a-hyp}
\par As each fiber $\bbE_B$ of a hyperdoctrine is a CCC
\par we can interpret propositional calculus in it.
\par In diagrams:
%D diagram CCC-HP1
%D 2Dx 100 +30 +30 +25 +30 +30
%D 2D 100 P0 T0 E0 E1
%D 2D
%D 2D +30 P1 P2 P3 T1 E2 E3
%D 2D
%D (( P0 .tex= P P1 .tex= Q P2 .tex= Q∧R P3 .tex= R
%D P0 P1 -> # .plabel= a f
%D P0 P2 -> # .plabel= m \ang{f,g}
%D P0 P3 -> # .plabel= a g
%D P1 P2 <- # .plabel= b \pi
%D P2 P3 -> # .plabel= b \pi'
%D ))
%D (( T0 .tex= P T1 .tex= §_B -> # .plabel= l !
%D ))
%D (( E0 .tex= P∧Q E1 .tex= P
%D E2 .tex= R E3 .tex= Q⊃R
%D E0 E1 <-|
%D E0 E2 -> # .PLABEL= _(0.43) \uncur"g
%D E0 E2 -> # .PLABEL= _(0.57) f
%D E1 E3 -> # .PLABEL= ^(0.43) g
%D E1 E3 -> # .PLABEL= ^(0.57) \cur"f
%D E0 E3 harrownodes nil 20 nil <-| sl^
%D E0 E3 harrownodes nil 20 nil |-> sl_
%D E2 E3 |->
%D ))
%D enddiagram
%D
$$\diag{CCC-HP1}$$
%D diagram CCC-HP2
%D 2Dx 100 +30 +30 +25 +30 +30 +35
%D 2D 100 P0 T0 E0 E1 E0'
%D 2D
%D 2D +30 P1 P2 P3 T1 E2 E3 E2'
%D 2D
%D (( P0 .tex= A P1 .tex= B P2 .tex= B{×}C P3 .tex= C
%D P0 P1 -> .plabel= a a|-b
%D P0 P2 -> .plabel= m a|-\ang{b,c}
%D P0 P3 -> .plabel= a a|-c
%D P1 P2 <- .plabel= b p|-b
%D P2 P3 -> .plabel= b p|-b'
%D ))
%D (( T0 .tex= A T1 .tex= 1 -> .plabel= l a|-*
%D ))
% %D (( E0' .tex= (B{->}C){×}B E2' .tex= C
% %D E0' E2' -> .plabel= c \ev_{BC}
% %D ))
%D (( E0 .tex= A×B E1 .tex= A
%D E2 .tex= C E3 .tex= B{->}C
%D E0 E1 <-|
%D E0 E2 -> .PLABEL= _(0.43) a,b|-fb
%D E0 E2 -> .PLABEL= _(0.57) a,b|-c
%D E1 E3 -> .PLABEL= ^(0.43) a|-f
%D E1 E3 -> .PLABEL= ^(0.57) a|-ðb¨B.c
%D E0 E3 harrownodes nil 20 nil <-| sl^
%D E0 E3 harrownodes nil 20 nil |-> sl_
%D E2 E3 |->
%D ))
%D enddiagram
%D
% $$\diag{CCC-HP2}$$
In a sequent-calculus-like form:
%:
%: Q R P|-Q P|-R Q R Q R
%: ----∧ ----------∧I ----∧E_1 -----∧E_2
%: Q∧R P|-Q∧R Q∧R|-Q Q∧R|-R
%:
%: ^HP-x0 ^HP-ang ^HP-pi ^HP-pi'
%:
%: P
%: -1 ----§I
%: §_B P|-§_B
%:
%: ^HP-1 ^HP-!
%:
%: Q R Q R P,Q|-R
%: ----⊃ ----\ev ---------⊃I
%: Q⊃R (Q⊃R)∧Q|-R P|-Q⊃R
%:
%: ^HP-->0 ^HP-ev ^HP-cur
%:
$$\begin{array}{cccc}
\ded{HP-x0} & \ded{HP-ang} & \ded{HP-pi} & \ded{HP-pi'} \\ \\
\ded{HP-1} & \ded{HP-!} \\ \\
\ded{HP-->0} & \ded{HP-ev} & \ded{HP-cur} \\
\end{array}
$$
% (find-LATEXfile "proof.sty" "\\def\\DeduceSym")
\makeatletter
\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
\vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
\vbox{\hbox{.}\hbox{.}}\hbox{.}}}
\makeatother
In natural deduction form (in downcased notation):
%:
%: P P
%: : :
%: Q R Q∧R Q∧R
%: ----∧I ---∧E_1 ---∧E_2
%: Q∧R Q R
%:
%: ^HPD-1 ^HPD-2 ^HPD-3
%:
%: P
%: -§I
%: §_B
%:
%: ^HPD-4
%:
%: P P P [Q]^1
%: : : ::::
%: Q Q⊃R R
%: ---------⊃E -----⊃I;1
%: R Q⊃R
%:
%: ^HPD-5 ^HPD-6
%:
$$\begin{array}{cccc}
\ded{HPD-1} & \ded{HPD-2} & \ded{HPD-3} \\ \\
\ded{HPD-4} \\ \\
\ded{HPD-5} & \ded{HPD-6} \\
\end{array}
$$
% --------------------
% «fa-I-in-a-hyp» (to ".fa-I-in-a-hyp")
% (s "Interpreting `$ýI$' in a hyperdoctrine" "fa-I-in-a-hyp")
\myslide {Interpreting `$ýI$' in a hyperdoctrine} {fa-I-in-a-hyp}
%D diagram fa-I-std
%D 2Dx 100 +25
%D 2D 100 ^*Q <--| Q
%D 2D | |
%D 2D | |-> |
%D 2D v v
%D 2D +25 R |--> ý_R
%D 2D
%D 2D +15 A×B ----> A
%D 2D
%D (( ^*Q Q
%D R ý_R
%D @ 0 @ 1 <-|
%D @ 0 @ 2 -> @ 1 @ 3 ->
%D @ 2 @ 3 |->
%D @ 0 @ 3 harrownodes nil 20 nil |->
%D A×B .tex= A{×}B A -> .plabel= a \pi
%D ))
%D enddiagram
%D
% $$\diag{fa-I-std}$$
%D diagram fa-I-dnc
%D 2Dx 100 +30
%D 2D 100 ^*Q <--| Q
%D 2D | |
%D 2D | |-> |
%D 2D v v
%D 2D +25 R |--> ý_R
%D 2D
%D 2D +15 A×B ----> A
%D 2D
%D (( ^*Q .tex= Qa Q .tex= Qa
%D R .tex= Rab ý_R .tex= ýb.Rab
%D @ 0 @ 1 <=
%D @ 0 @ 2 |-> @ 1 @ 3 |->
%D @ 2 @ 3 =>
%D @ 0 @ 3 harrownodes nil 20 nil |->
%D A×B .tex= a,b A .tex= a |-> .plabel= a \pi
%D ))
%D enddiagram
%D
% $$\diag{fa-I-dnc}$$
%:
%: ^*Q|-R
%: -------ýI
%: Q|-ý_R
%:
%: ^fa-I-std-seq
%:
%: Qa
%: :
%: Rab a,b;Qa|-Rab
%: ------ýI ----------ýI
%: ýb.Rab a;Qa|-ýb.Rab
%:
%: ^fa-I-dnc-dn ^fa-I-dnc-seq
%:
%:
% $$\ded{fa-I-std-seq}$$
% $$\ded{fa-I-dnc-dn} \qquad \ded{fa-I-dnc-seq}$$
%D diagram fa-I-all
%D 2Dx 100 +55 +60
%D 2D 100 stq-seq std
%D 2D
%D 2D +60 dnc-dn dnc-seq dnc
%D 2D
%D (( stq-seq .tex= \ded{fa-I-std-seq} y+= 5 place
%D dnc-dn .tex= \ded{fa-I-dnc-dn} y+= 5 place
%D dnc-seq .tex= \ded{fa-I-dnc-seq} y+= 5 place
%D std .tex= \diag{fa-I-std} BOX place
%D dnc .tex= \diag{fa-I-dnc} BOX x+= 2 place
%D
%D ))
%D enddiagram
%D
$$\diag{fa-I-all}$$
% --------------------
% «fa-E-in-a-hyp» (to ".fa-E-in-a-hyp")
% (s "Interpreting `$ýE$' in a hyperdoctrine" "fa-E-in-a-hyp")
\myslide {Interpreting `$ýE$' in a hyperdoctrine} {fa-E-in-a-hyp}
%D diagram fa-E-std
%D 2Dx 100 +35 +30
%D 2D 100 Q0
%D 2D ^
%D 2D |
%D 2D v
%D 2D +25 Q1 <--| Q2 <--| Q3
%D 2D | | |
%D 2D | <-| | <-| |
%D 2D v v v
%D 2D +25 R1 <--| R2 |--> R3
%D 2D
%D 2D <id,f> \pi
%D 2D +15 A |--> A×B |--> A{}
%D 2D |-----id---->
%D 2D
%D (( Q0 .tex= Q
%D Q1 .tex= \ang{\id,f}^*^*Q Q2 .tex= ^*Q Q3 .tex= Q
%D R1 .tex= \ang{\id,f}^*R R2 .tex= R R3 .tex= ý_R
%D Q0 Q1 <->
%D Q1 Q2 <-| Q2 Q3 <-|
%D Q1 R1 -> Q2 R2 -> Q3 R3 ->
%D R1 R2 <-| R2 R3 |->
%D Q1 R2 harrownodes nil 20 nil <-|
%D Q2 R3 harrownodes nil 20 nil <-|
%D ))
%D (( A A×B A{}
%D @ 0 @ 1 -> .plabel= a \ang{\id,f}
%D @ 1 @ 2 -> .plabel= a \pi
%D @ 0 @ 2 -> .plabel= b \id .slide= -7pt
%D ))
%D enddiagram
%D
% $$\diag{fa-E-std}$$
%D diagram fa-E-dnc
%D 2Dx 100 +35 +30
%D 2D 100 Q0
%D 2D ^
%D 2D |
%D 2D v
%D 2D +25 Q1 <--| Q2 <--| Q3
%D 2D | | |
%D 2D | <-| | <-| |
%D 2D v v v
%D 2D +25 R1 <--| R2 |--> R3
%D 2D
%D 2D <id,f> \pi
%D 2D +15 A |--> A×B |--> A{}
%D 2D |-----id---->
%D 2D
%D (( Q0 .tex= Qa
%D Q1 .tex= Qa Q2 .tex= Qa Q3 .tex= Qa
%D R1 .tex= Rab' R2 .tex= Rab R3 .tex= ýb.Rab
%D Q0 Q1 <->
%D Q1 Q2 <= Q2 Q3 <=
%D Q1 R1 |-> Q2 R2 |-> Q3 R3 |->
%D R1 R2 <= R2 R3 =>
%D Q1 R2 harrownodes nil 20 nil <-|
%D Q2 R3 harrownodes nil 20 nil <-|
%D ))
%D (( A .tex= a A×B .tex= a,b A{} .tex= a
%D @ 0 @ 1 |-> .plabel= a \ang{\id,f}
%D @ 1 @ 2 |-> .plabel= a \pi
%D @ 0 @ 2 |-> .plabel= b \id .slide= -7pt
%D ))
%D enddiagram
%D
% $$\diag{fa-E-dnc}$$
%:
%: f Q|-ý_R
%: ------------ýE
%: Q|-\ang{\id,f}^*R
%:
%: ^fa-E-std-seq
%:
%: Qa
%: :
%: a|-b' ýb.Rab a|-b' a;Qa|-ýb.Rab
%: -------------ýE -----------------ýE
%: Rab' a;Qa|-Rab'
%:
%: ^fa-E-dnc-dn ^fa-E-dnc-seq
%:
%:
% $$\ded{fa-E-std-seq}$$
% $$\ded{fa-E-dnc-dn} \qquad \ded{fa-E-dnc-seq}$$
%D diagram fa-E-all
%D 2Dx 100 +78 +80
%D 2D 100 stq-seq std
%D 2D
%D 2D +85 dnc-dn dnc-seq dnc
%D 2D
%D (( stq-seq .tex= \ded{fa-E-std-seq} y+= 5 place
%D dnc-dn .tex= \ded{fa-E-dnc-dn} y+= 5 place
%D dnc-seq .tex= \ded{fa-E-dnc-seq} y+= 5 place
%D std .tex= \diag{fa-E-std} BOX place
%D dnc .tex= \diag{fa-E-dnc} BOX x+= 8 place
%D
%D ))
%D enddiagram
%D
$$\diag{fa-E-all}$$
% --------------------
% «ex-I-in-a-hyp» (to ".ex-I-in-a-hyp")
% (s "Interpreting `$ÎI$' in a hyperdoctrine" "ex-I-in-a-hyp")
\myslide {Interpreting `$ÎI$' in a hyperdoctrine} {ex-I-in-a-hyp}
%D diagram ex-I-std
%D 2Dx 100 +45 +30
%D 2D 100 P0 <--| P1 <--| P2
%D 2D | | |
%D 2D | <-| | <-| |id
%D 2D v v v
%D 2D +25 P3 <--| P4 <--| P5
%D 2D
%D 2D +15 A ----> A×B --> A{}
%D 2D
%D (( P0 .tex= \ang{\id,f}^*P P1 .tex= P P2 .tex= Î_P
%D P3 .tex= \ang{\id,f}^*^*Î_P P4 .tex= ^*Î_P P5 .tex= Î_P
%D P0 P1 <-| P1 P2 <-|
%D P0 P3 -> P1 P4 -> P2 P5 -> .plabel= r \id
%D P3 P4 <-| P4 P5 |->
%D @ 0 @ 4 harrownodes nil 20 nil <-|
%D @ 1 @ 5 harrownodes nil 20 nil <-|
%D ))
%D (( A A×B .tex= A{×}B A{}
%D @ 0 @ 1 -> .plabel= a \ang{\id,f}
%D @ 1 @ 2 -> .plabel= a \pi
%D @ 0 @ 2 -> sl__ .plabel= b \id
%D ))
%D enddiagram
%D
% $$\diag{ex-I-std}$$
%D diagram ex-I-dnc
%D 2Dx 100 +35 +35
%D 2D 100 P0 <--| P1 <--| P2
%D 2D | | |
%D 2D | <-| | <-| |id
%D 2D v v v
%D 2D +25 P3 <--| P4 <--| P5
%D 2D
%D 2D +15 A ----> A×B --> A{}
%D 2D
%D (( P0 .tex= Pab' P1 .tex= Pab P2 .tex= Îb.Pab
%D P3 .tex= Îb.Pab P4 .tex= Îb.Pab P5 .tex= Îb.Pab
%D P0 P1 <= P1 P2 <=
%D P0 P3 |-> P1 P4 |-> P2 P5 |-> .plabel= r \id
%D P3 P4 <= P4 P5 =>
%D @ 0 @ 4 harrownodes nil 20 nil <-|
%D @ 1 @ 5 harrownodes nil 20 nil <-|
%D ))
%D (( A .tex= a A×B .tex= a,b A{} .tex= a
%D @ 0 @ 1 |-> .plabel= a \ang{\id,f}
%D @ 1 @ 2 |-> .plabel= a \pi
%D @ 0 @ 2 |-> sl__ .plabel= b \id
%D ))
%D enddiagram
%D
% $$\diag{ex-I-dnc}$$
%:
%: f P
%: --------------------ýI
%: \ang{\id,f}^*P|-Î_P
%:
%: ^ex-I-std-seq
%:
%:
%:
%: Pab' a|-b' \ssst{a,b}{Pab}
%: ------ÎI ----------------------ÎI
%: Îb.Pab a;Pab'|-Îb.Pab
%:
%: ^ex-I-dnc-dn ^ex-I-dnc-seq
%:
%:
% $$\ded{ex-I-std-seq}$$
% $$\ded{ex-I-dnc-dn} \qquad \ded{ex-I-dnc-seq}$$
%D diagram ex-I-all
%D 2Dx 100 +60 +95
%D 2D 100 stq-seq std
%D 2D
%D 2D +60 dnc-dn dnc-seq dnc
%D 2D
%D (( stq-seq .tex= \ded{ex-I-std-seq} y+= 5 place
%D dnc-dn .tex= \ded{ex-I-dnc-dn} y+= 5 place
%D dnc-seq .tex= \ded{ex-I-dnc-seq} y+= 5 place
%D std .tex= \diag{ex-I-std} BOX place
%D dnc .tex= \diag{ex-I-dnc} BOX x+= 2 place
%D
%D ))
%D enddiagram
%D
$$\diag{ex-I-all}$$
% --------------------
% «ex-E-in-a-hyp» (to ".ex-E-in-a-hyp")
% (s "Interpreting `$ÎE$' in a hyperdoctrine" "ex-E-in-a-hyp")
\myslide {Interpreting `$ÎE$' in a hyperdoctrine} {ex-E-in-a-hyp}
%D diagram exE-std
%D 2Dx 100 +40 +45 +25 +40
%D 2D 100 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 <--> B6' <============ B7
%D 2D
%D 2D +0 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +35 b2 |--------------------> b3
%D 2D
%D (( B0 .tex= P∧^*Q B1 .tex= Î_P∧Q
%D B2 .tex= ^*R B3 .tex= R
%D B4 .tex= P B5 .tex= Î_P
%D B6 .tex= ^*Q⊃^*R B6' .tex= ^*(Q⊃R) B7 .tex= Q⊃R
%D B0 B2 ->
%D B1 B3 -> B2 B3 <-|
%D B0 B4 <-| B2 B6 |->
%D B1 B5 <-| B3 B7 |->
%D B4 B5 <-| B5 B7 -> B6' B7 <-|
%D B4 B6 ->
%D B4 B6' ->
%D B6 B6' <- sl^ .plabel= a \nat
%D B6 B6' -> sl_ .plabel= b \Pimp
%D B4 B6' midpoint B5 B7 midpoint harrownodes nil 20 nil |->
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 15 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 15 nil <-|
%D ))
%D (( b0 b2 midpoint .TeX= A×B b1 b3 midpoint .TeX= A -> .plabel= a \pi
%D ))
%D enddiagram
$$\diag{exE-std}$$
%D diagram exE-dnc
%D 2Dx 100 +40 +45 +25 +40
%D 2D 100 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 <--> B6' <============ B7
%D 2D
%D 2D +0 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +35 b2 |--------------------> b3
%D 2D
%D (( B0 .tex= Pab∧Qa B1 .tex= (Îb.Pab)∧Qa
%D B2 .tex= Ra B3 .tex= Ra
%D B4 .tex= Pab B5 .tex= Îb.Pab
%D B6 .tex= Qa⊃Ra B6' .tex= Qa⊃Ra B7 .tex= Qa⊃Ra
%D B0 B2 |->
%D B1 B3 |-> B2 B3 <=
%D B0 B4 <= B2 B6 =>
%D B1 B5 <= B3 B7 =>
%D B4 B5 <= B5 B7 |-> B6' B7 <=
%D B4 B6 |->
%D B4 B6' |->
%D B6 B6' <-| sl^ .plabel= a \nat
%D B6 B6' |-> sl_ .plabel= b \Pimp
%D B4 B6' midpoint B5 B7 midpoint harrownodes nil 20 nil |->
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 15 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 15 nil <-|
%D ))
%D (( b0 b2 midpoint .TeX= a,b b1 b3 midpoint .TeX= a |->
%D ))
%D enddiagram
$$\diag{exE-dnc}$$
\bsk
%:
%: P∧^*Q|-^*R
%: ------------ÎE
%: Î_P∧Q|-R
%:
%: ^ex-I-std-seq
%:
%: [Pab]^1 Qa
%: :::::
%: Îb.Pab Ra a,b;Pab,Qa|-Ra
%: ------------ÎE;1 ---------------ÎE
%: Ra a;Îb.Pab,Qa|-Ra
%:
%: ^ex-E-dnc-dn ^ex-E-dnc-seq
%:
$$\begin{array}{ccc}
&& \ded{ex-I-std-seq} \\
\ded{ex-E-dnc-dn} && \ded{ex-E-dnc-seq} \\
\end{array}
$$
% --------------------
% «equality-hofmann95» (to ".equality-hofmann95")
% (s "Equality types: Hofmann 1995" "equality-hofmann95")
\myslide {Equality types: Hofmann 1995} {equality-hofmann95}
\par A diagram for the rules Id-Intro and Id-Elim-J
\par as they appear in Martin Hofmann's PhD thesis (p.21):
\par (Note: my the diagram is for a slightly weaker Id-Elim-J...
\par in the rule the type $ $ may depend on the value of $p$)
% (find-angg ".emacs.papers" "hofmann")
% (find-hofmannthesispage (+ 12 21) "Id-Intro")
% (find-hofmannthesispage (+ 12 21) "Id-Elim-J")
%D diagram hofmann95-equality
%D 2Dx 100 +45 +50
%D 2D 100 A0 |-> A1
%D 2D | |
%D 2D | |-> |
%D 2D v v
%D 2D +30 A2 <-| A3
%D 2D
%D 2D +10 B0 <---------| B1
%D 2D | |
%D 2D | <-| |
%D 2D v v
%D 2D +30 B2 <---------| B3
%D 2D
%D 2D +10 C0 <--| C1 <-| C2
%D 2D | | |
%D 2D | <-| | <-| |
%D 2D v v v
%D 2D +30 C3 <--| C4 |-> C5
%D 2D
%D 2D +15 D0 --> D1
%D 2D +10 D2 ----------> D3
%D 2D +10 D4 ---> D5 --> D6
%D 2D
%D (( A0 .tex= 1 A1 .tex= ¯{Id}_(x,y)
%D A2 .tex= [y:=x] A3 .tex=
%D B0 .tex= ¯{Id}_(N_1,N_2) B1 .tex= ¯{Id}_(x,y)
%D B2 .tex= \mysubst B3 .tex=
%D C0 .tex= 1 C1 .tex= 1 C2 .tex= ¯{Id}_(x,y)
%D C3 .tex= ¯{Id}_(M,M) C4 .tex= ¯{Id}_(x,x) C5 .tex= ¯{Id}_(x,y)
%D D0 .tex= (\vagx) D1 .tex= (\vagxy)
%D D2 .tex= (\vag) D3 .tex= (\vagxy)
%D D4 .tex= (\vag) D5 .tex= (\vagx) D6 .tex= (\vagxy)
%D ))
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l \va,x,y;p|-M
%D A1 A3 -> .plabel= r \va,x,y;p|-¯J_{, }(M,x,y,p)
%D A2 A3 <-|
%D A0 A3 harrownodes nil 20 nil |-> sl^ .plabel= a Æ^\flat
%D
%D B0 B1 <-|
%D B0 B2 -> .plabel= l \text{(Id-Elim-J)}"\quad"\va|-¯J_{, }(M,N_1,N_2,P)
%D B1 B3 ->
%D B1 B3 -> .plabel= r \va,x,y;p|-¯J_{, }(M,x,y,p)
%D B2 B3 <-|
%D B0 B3 harrownodes nil 20 nil <-| sl_
%D B0 B3 harrownodes nil 20 nil <-| sl_ .plabel= a *
%D
%D C0 C1 <-| C1 C2 <-|
%D C0 C3 -> .plabel= l \text{(Id-Intro)}"\quad"\va|-¯{Refl}_(M)
%D C1 C4 ->
%D C2 C5 -> .plabel= r \va,x,y;p|-p
%D C3 C4 <-| C4 C5 |->
%D C0 C4 harrownodes nil 20 nil <-| .plabel= b *
%D C1 C5 harrownodes nil 20 nil <-| .plabel= b Æ^\sharp
%D
%D D0 D1 -> .plabel= a y:=x
%D D2 D3 -> .plabel= m x:=N_1,y:=N_2
%D D4 D5 -> .plabel= b x:=M
%D D5 D6 -> .plabel= b y:=x
%D ))
%D enddiagram
%D
$$\def\mysubst{[x:=N1][y:=N2][p:=P]}
\def\va{\vec a}
\def\vag{\va¨\GG}
\def\vagx{\va¨\GG,x¨}
\def\vagxy{\va¨\GG,x¨,y¨}
\diag{hofmann95-equality}
$$
%*
\end{document}
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: