|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2020seelyhyp.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020seelyhyp.tex" :end))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2020seelyhyp.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020seelyhyp.pdf"))
% (defun e () (interactive) (find-LATEX "2020seelyhyp.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020seelyhyp"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-pdf-page "~/LATEX/2020seelyhyp.pdf")
% (find-sh0 "cp -v ~/LATEX/2020seelyhyp.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2020seelyhyp.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2020seelyhyp.pdf
% file:///tmp/2020seelyhyp.pdf
% file:///tmp/pen/2020seelyhyp.pdf
% http://angg.twu.net/LATEX/2020seelyhyp.pdf
% (find-LATEX "2019.mk")
% «.title» (to "title")
% «.my-introduction» (to "my-introduction")
% «.motivation-adjs» (to "motivation-adjs")
% «.adjoints-quants» (to "adjoints-quants")
% «.adjoints-equality» (to "adjoints-equality")
% «.adjoints-subst» (to "adjoints-subst")
% «.exists-examples» (to "exists-examples")
% «.exists-examples-2» (to "exists-examples-2")
% «.exists-cat-rules-to-ND» (to "exists-cat-rules-to-ND")
% «.exists-elim-to-cats» (to "exists-elim-to-cats")
% «.exists-intro-to-cats» (to "exists-intro-to-cats")
% «.exists-ND-rules-to-cats» (to "exists-ND-rules-to-cats")
% «.bounded-quantifiers» (to "bounded-quantifiers")
% «.ND-in-hyps» (to "ND-in-hyps")
% «.sec-4» (to "sec-4")
% «.page-513» (to "page-513")
% «.3._hyperdoctrines» (to "3._hyperdoctrines")
% «.BCC-def» (to "BCC-def")
% «.frobenius» (to "frobenius")
% «.5._hyp-to-LPCE» (to "5._hyp-to-LPCE")
% «.page-523» (to "page-523")
% «.page-523-equality» (to "page-523-equality")
% «.page-523-eq-sub» (to "page-523-eq-sub")
% «.thanks» (to "thanks")
% «.elisp» (to "elisp")
\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,urlcolor=DarkRed,citecolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{tocloft} % (find-es "tex" "tocloft")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{colorweb} % (find-es "tex" "colorweb")
%\usepackage{tikz}
\usepackage{MnSymbol} % (find-es "tex" "lhookdownarrow")
%
% (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof} % For derivation trees ("%:" lines)
\input diagxy % For 2D diagrams ("%D" lines)
\xyoption{curve} % For the ".curve=" feature in 2D diagrams
\usepackage{bussproofs}
%
\usepackage{edrx15} % (find-LATEX "edrx15.sty")
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
\input edrx20limp.tex % (find-LATEX "edrx20limp.tex")
\catcode`⊸=13 \def⊸{\limp}
%
\usepackage[backend=biber,
style=alphabetic]{biblatex} % (find-es "tex" "biber")
\addbibresource{catsem-slides.bib} % (find-LATEX "catsem-slides.bib")
%
% (find-es "tex" "geometry")
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
\long\def\ColorRed #1{{\color{Red1}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorViolet#1{{\color{Violet!50!black}#1}}
\long\def\ColorGreen #1{{\color{SpringDarkHard}#1}}
\long\def\ColorGreen #1{{\color{SpringGreen4}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#1}}
\long\def\ColorGray #1{{\color{GrayLight}#1}}
\long\def\ColorGray #1{{\color{black!30!white}#1}}
\def\pded#1{\left(\cded{#1}\right)}
\def\pdedscale#1#2{\scalebox{#1}{$\pded{#2}$}}
\def\frown{=(}
\def\calL{\mathcal{L}}
\def\CodSS{\Cod: \Set^\dnito → \Set}
\def\dnito{\lhookdownarrow}
\def\psmi #1#2{ \psm {#1 \\ \dnito \\ #2}}
\def\pmati #1#2{ \pmat{#1 \\ \dnito \\ #2}}
\def\Frob {\text{Frob}}
\def\PresExp{\text{PresExp}}
% (find-books "__cats/__cats.el" "lambek86")
% (find-books "__cats/__cats.el" "lncs0242")
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% «title» (to ".title")
{\setlength{\parindent}{0em}
\footnotesize
Notes on [Seely83], a.k.a.:
``Hyperdoctrines, Natural Deduction and The Beck Condition'', available at:
\url{http://www.math.mcgill.ca/rags/ZML/ZML.PDF}
\ssk
These notes are at:
\url{http://angg.twu.net/LATEX/2020seelyhyp.pdf}
\ssk
See:
\url{http://angg.twu.net/LATEX/2020favorite-conventions.pdf}
\url{http://angg.twu.net/math-b.html\#favorite-conventions}
I wrote these notes mostly to test if the conventions above
are good enough.
}
% (find-es "tex" "tocloft")
% \renewcommand{\cfttoctitlefont}{\bfseries}
% \setlength{\cftbeforesecskip}{2.5pt}
% \tableofcontents
\bsk
\bsk
% __ __ _ _
% | \/ |_ _ (_)_ __ | |_ _ __ ___
% | |\/| | | | | | | '_ \| __| '__/ _ \
% | | | | |_| | | | | | | |_| | | (_) |
% |_| |_|\__, | |_|_| |_|\__|_| \___/
% |___/
%
% «my-introduction» (to ".my-introduction")
\cite{SeelyBeck} was one of the first papers that made me think:
``wow, this is really beautiful but it's written in the {\sl wrong
language!} It shows how to generalize {\sl something}, but it
doesn't show in a way that is clear enough what this `something' is,
and I find the translation between the original and the generalization
{\sl very hard} to follow... {\sl I need a version `for children' of
this!!!}''...
My current favorite way of creating a version ``for children'' of the
constructions in \cite{SeelyBeck} takes two steps: in the first we
draw the ``missing diagrams'' following the conventions in
\cite{FavC}, and in the second we draw diagrams with the same shapes
as these, but in the ``archetypal case'' (\cite[sec.16]{IDARCT}). The
{\sl archetypal hyperdoctrine} is the fibration of subsets:
%
% (find-angg ".emacs" "idarct-preprint")
% (find-idarctpage 23 "16. Archetypal Models")
% (find-idarcttext 23 "16. Archetypal Models")
%
%D diagram arch-fib-0
%D 2Dx 100 +30 +60 +70
%D 2D 100 A0 B0 C0 D0
%D 2D
%D 2D +25 A1 B1 C1 D1
%D 2D
%D ren A0 A1 ==> \Set^\dnito \Set
%D ren B0 B1 ==> \pmati{A}{B} B
%D ren C0 C1 ==> \pmati{\setofst{(c,d)∈C{×}D}{Q(c,d)}}{C{×}D} C{×}D
%D ren D0 D1 ==> \pmat{Q(c,d)\\(c,d)∈C{×}D} C{×}D
%D
%D (( A0 A1 -> .plabel= l \Cod
%D B0 B1 |->
%D # C0 place C1 place
%D # D0 place D1 place
%D # C0 D0 =
%D # C1 D1 =
%D ))
%D enddiagram
%D
$$\pu
\diag{arch-fib-0}
$$
%
We usually don't draw the vertical `$↦$'s --- we just draw $\psmi AB$
above $B$.
We abbreviate subsets defined by propositions as this:
%
$$\pmati{\setofst{b∈B}{P(b)}}{B} \quad ≡ \quad \cmat{P(b) \\ b∈B} $$
Most of the time we will just write the `$P(b)$' above the `$B$',
omitting the `$b∈$' and pretending that the `$b∈$' part is obvious to
reconstruct.
In this paper Seely uses indexed categories instead of fibrations. The
translation between indexed categories and fibrations is nicely
explained in \cite[p.107]{Jacobs}; one of the directions of the
translation is the Grothendieck Construction, that takes an index
category $Ψ:\bbB^\op→\Cat$ and produces an fibration $∫Ψ → \catB$, and
in the notation for defining new categories diagrammatically in
\cite[sec.7.1]{FavC} the Grothendieck Construction is this:
%
% (find-books "__cats/__cats.el" "jacobs")
% (find-jacobspage (+ 19 107) "1.10. Indexed categories")
% (favp 34 "comma-categories")
% (fav "comma-categories")
%
%D diagram gro-jac-1
%D 2Dx 100 +10 +15 +20 +30 +20 +20
%D 2D 100 B0 D0
%D 2D +10 A0 | C0 -->
%D 2D +10 ^ B2 - B3 | D2
%D 2D | v
%D 2D +15 A1 A2 B4 - B5 C1 D4 - D5
%D 2D
%D ren A0 A1 A2 ==> \Cat \bbB^\op \bbB
%D ren B0 B2 B3 B4 B5 ==> X u^*Y Y I J
%D ren C0 C1 ==> ∫Ψ \bbB
%D ren D0 D2 D4 D5 ==> (I,X) (J,Y) I J
%D
%D (( A0 A1 <- .plabel= r Ψ
%D A2 place
%D B0 B2 -> .plabel= r f
%D B2 B3 <-|
%D B4 B5 -> .plabel= a u
%D C0 C1 ->
%D D0 D2 -> .plabel= r (u,f)
%D D4 D5 -> .plabel= a u
%D ))
%D enddiagram
%D
$$\pu
\diag{gro-jac-1}
$$
% _ _ _
% / \ __| |(_)___
% / _ \ / _` || / __|
% / ___ \ (_| || \__ \
% /_/ \_\__,_|/ |___/
% |__/
%
% «motivation-adjs» (to ".motivation-adjs")
\subsection*{Motivation: some adjunctions}
It is easy to see --- in the sense of {\sl visualize} --- that the
functor that adds a dummy variable to the context,
%
$$\cmat{Q(x)\\(x,y)∈X{×}Y}
\diagxyto/<-|/<200>
\cmat{Q(x)\\x∈X}
$$
%
is ``adjoint to the quantifiers'':
%D diagram ??
%D 2Dx 100 +60
%D 2D 100 A0 A1
%D 2D
%D 2D +35 A2 A3
%D 2D
%D 2D +35 A4 A5
%D 2D
%D 2D +25 B0 B1
%D 2D
%D 2D +15 C0 C1
%D 2D
%D ren A0 A1 ==> \cmat{P(x,y)\\(x,y)∈X{×}Y} \cmat{∃y∈Y.\,P(x,y)\\x∈X}
%D ren A2 A3 ==> \cmat{Q(x)\\(x,y)∈X{×}Y} \cmat{Q(x)\\x∈X}
%D ren A4 A5 ==> \cmat{R(x,y)\\(x,y)∈X{×}Y} \cmat{∀y∈Y.\,R(x,y)\\x∈X}
%D ren B0 B1 ==> 𝐛P(X{×}Y) 𝐛P(X)
%D ren C0 C1 ==> X{×}Y X
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l P(x,y)⊢Q(x)
%D A1 A3 -> .plabel= r ∃y∈Y.P(x,y)⊢Q(x)
%D A0 A3 harrownodes nil 20 nil <->
%D A2 A3 <-|
%D A2 A4 -> .plabel= l Q(x)⊢R(x,y)
%D A3 A5 -> .plabel= r Q(x)⊢∀y∈Y.R(x,y)
%D A2 A5 harrownodes nil 20 nil <->
%D A4 A5 |->
%D
%D B0 B1 -> sl^^ .plabel= a ∃_y
%D B0 B1 <- .plabel= m π^*
%D B0 B1 -> sl__ .plabel= b ∀_y
%D
%D C0 C1 -> .plabel= a π
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
See the big figure in section 13 of \cite{IDARCT}.
\newpage
The `$\diagxyto/<->/<175>$' in the middle of the top square in the
diagram above can also be interpreted as: {\sl if we have an
intuitionistic proof of $P(x,y)⊢Q(x)$ then we can produce from it an
intuitionistic proof of $∃y∈Y.P(x,y)⊢Q(x)$, and vice-versa} --- and
the same for the `$\diagxyto/<->/<175>$' in the middle of the lower
square. Here is how, in details, and showing also the actions of the
three functors on morphisms:
% «adjoints-quants» (to ".adjoints-quants")
\bsk
%:
%: [\Pxy]^1
%: ::::::α
%: \Qxy
%: --------
%: \Exy\Pxy \Exy\Qxy
%: ----------------------1
%: \Exy\Qxy
%:
%: ^Sigmapi-F
%:
%:
%: \Qxy [\Qxy]^1
%: -------- :::f
%: \Exy\Qxy \Exy\Qxy \Rx
%: ::: ---------------1
%: \Rx \Rx
%:
%: ^Sigmapi-transposeleft ^Sigmapi-transposeright
%:
%:
%: \Rx
%: :::β
%: \Sx
%:
%: ^pistar-F
%:
%:
%: \Sx [\Sx]^1
%: ::::::::k ::::
%: \Fay\Txy \Sx \Txy
%: -------- ---------
%: \Txy \Fay\Txy
%:
%: ^Pipi-transposeleft ^Pipi-transposeright
%:
%:
%: \Fay\Txy [\Txy]^1
%: -------- ::::γ
%: \Txy \Uxy
%: ----------------
%: \Fay\Uxy
%:
%: ^Pipi-F
%:
\def\Pxy{Pxy}
\def\Qxy{Qxy}
\def\Rx {Rx}
\def\Sx {Sx}
\def\Txy{Txy}
\def\Uxy{Uxy}
\def\Exy{∃y.}
\def\Fay{∀y.}
%D diagram adjs-pi*
%D 2Dx 100 +40
%D 2D 100 A0 |-> A1
%D 2D | |
%D 2D | |-> |
%D 2D | |
%D 2D +25 A2 |-> A3
%D 2D | |
%D 2D | <-> |
%D 2D | |
%D 2D +25 B0 <-| B1
%D 2D | |
%D 2D | <-| |
%D 2D | |
%D 2D +25 B2 <-| B3
%D 2D | |
%D 2D | <-> |
%D 2D | |
%D 2D +25 C0 |-> C1
%D 2D | |
%D 2D | |-> |
%D 2D | |
%D 2D +25 C2 |-> C3
%D 2D
%D 2D +20 D0 <=> D1
%D 2D
%D 2D +20 E0 |-> E1
%D 2D +10 E2 --> E3
%D 2D
%D ren A0 A1 ==> \Pxy \Exy\Pxy
%D ren A2 A3 ==> \Qxy \Exy\Qxy
%D ren B0 B1 ==> \Rx \Rx
%D ren B2 B3 ==> \Sx \Sx
%D ren C0 C1 ==> \Txy \Fay\Txy
%D ren C2 C3 ==> \Uxy \Fay\Uxy
%D ren D0 D1 ==> 𝐛P(X{×}Y) 𝐛P(X)
%D ren E0 E1 ==> (x,y) x
%D ren E2 E3 ==> X{×}Y X
%D
%D (( A0 A1 |->
%D A2 A3 |->
%D B0 B1 <-|
%D B2 B3 <-|
%D C0 C1 |->
%D C2 C3 |->
%D A0 A3 harrownodes nil 20 nil |->
%D A2 B1 harrownodes nil 20 nil |-> sl^
%D A2 B1 harrownodes nil 20 nil <-| sl_
%D B0 B3 harrownodes nil 20 nil <-|
%D B2 C1 harrownodes nil 20 nil <-| sl^
%D B2 C1 harrownodes nil 20 nil |-> sl_
%D C0 C3 harrownodes nil 20 nil |->
%D A0 A2 -> .plabel= l α
%D A1 A3 -> .plabel= r Σ_πα
%D A2 B0 -> .plabel= l \sm{f\\(Σ_π^♯)g}
%D A3 B1 -> .plabel= r \sm{(Σ_π^♭)f\\g}
%D B0 B2 -> .plabel= l π^*β
%D B1 B3 -> .plabel= r β
%D B2 C0 -> .plabel= l \sm{(Π_π^♭)h\\k}
%D B3 C1 -> .plabel= r \sm{h\\(Π_π^♯)k}
%D C0 C2 -> .plabel= l γ
%D C1 C3 -> .plabel= r Π_πγ
%D D0 D1 -> sl^^ .plabel= a Σ_π
%D D0 D1 <- .plabel= m π^*
%D D0 D1 -> sl__ .plabel= b Π_π
%D E0 E1 |->
%D E2 E3 -> .plabel= a π
%D
%D A1 A3 midpoint relplace 55 0 Σ_πα:=\pdedscale{0.55}{Sigmapi-F}
%D A3 B1 midpoint relplace 55 0 (Σ_π^♭)f:=\pdedscale{0.55}{Sigmapi-transposeright}
%D A2 B0 midpoint relplace -50 0 (Σ_π^♯)g:=\pdedscale{0.45}{Sigmapi-transposeleft}
%D B0 B2 midpoint relplace -50 0 π^*β:=\pdedscale{0.55}{pistar-F}
%D B2 C0 midpoint relplace -50 0 (Π_π^♭)h:=\pdedscale{0.40}{Pipi-transposeleft}
%D B3 C1 midpoint relplace 50 0 (Π_π^♯)k:=\pdedscale{0.40}{Pipi-transposeright}
%D C1 C3 midpoint relplace 55 0 Π_πγ:=\pdedscale{0.55}{Pipi-F}
%D ))
%D enddiagram
%D
\pu
\phantom{a}
\hspace{-20pt}
$
\diag{adjs-pi*}
$
\bsk
Not everybody who knows Natural Deduction for Propositional Calculus
knows how to use quantifiers in ND... some of the rules for
introduction and elimination of quantifiers have restrictions that are
(or: that I found) hard to understand. Seely uses a system of ND that
is equivalent to the one in \cite{Prawitz65}, but that only allows
discarding hypotheses in subtrees ``with a single hypothesis''; I find
that system much easier to understand than the one in
\cite{Prawitz65}.
\newpage
% «adjoints-equality» (to ".adjoints-equality")
...so, the diagram in the previous page can be used to learn and to
teach Natural Deduction with quantifiers --- and we can use the
adjoints to the functor
%
$$\cmat{R(x,x)\\x∈X}
\diagxyto/<-|/<200>
\cmat{R(x,x')\\(x,x')∈X{×}X}
$$
%
to learn how to use the rules for equality in ND:
\bsk
\def\exx {x{=}x}
\def\exxp{x{=}x'}
\def\Px {Px}
\def\Qx {Qx}
\def\Rxx {Rxx}
\def\Rxxp{Rxx'}
\def\Sxx {Sxx}
\def\Sxxp{Sxx'}
\def\Tx {Tx}
\def\Ux {Ux}
%:
%:
%:
%:
%: \exxp∧\Px
%: ---------
%: \exxp∧\Px \Px
%: --------- :::α
%: \exxp \Qx
%: ----------------
%: \exxp∧\Qx
%:
%: ^SigmaD-F
%:
%: \exxp∧\Qx
%: ---- ---------
%: \exx \Qx [\exxp∧\Qx]^1 \exxp∧\Qx \Qx
%: ---------- :::::::::::g --------- ::::f
%: \exx∧\Qx \Rxxp \exxp \Rxx
%: --------------------[x':=x];1 -----------------
%: \Rxx \Rxxp
%:
%: ^SigmaD-transposeleft ^SigmaD-transposeright
%:
%:
%: [\Rxxp]^1
%: :::::::::β
%: \Rxx \Sxxp
%: ------------[x':=x];1
%: \Sxx
%:
%: ^Dstar-F
%: [\Sxx]^1
%: ::::::::k
%: \Tx
%: --------1
%: [\Sxxp]^1 [\exxp]^2 \Sxx⊸\Tx
%: :::::::::h --------------------
%: \Sxx \exxp⊸\Tx \Sxxp \Sxxp⊸\Tx
%: ---- ----------------[x':=x];1 ------------------
%: \exx \exx⊸\Tx \Tx
%: ---------------- ---------2
%: \Tx \exxp⊸\Tx
%:
%: ^PiD-transposeleft ^PiD-transposeright
%:
%:
%: [\exxp]^1 \exxp⊸\Tx
%: ---------------------
%: \Tx
%: :::γ
%: \Ux
%: ---------1
%: \exxp⊸\Ux
%:
%: ^PiD-F
%D diagram adjs-Delta*
%D 2Dx 100 +40
%D 2D 100 A0 |-> A1
%D 2D | |
%D 2D | |-> |
%D 2D | |
%D 2D +25 A2 |-> A3
%D 2D | |
%D 2D | <-> |
%D 2D | |
%D 2D +25 B0 <-| B1
%D 2D | |
%D 2D | <-| |
%D 2D | |
%D 2D +25 B2 <-| B3
%D 2D | |
%D 2D | <-> |
%D 2D | |
%D 2D +25 C0 |-> C1
%D 2D | |
%D 2D | |-> |
%D 2D | |
%D 2D +25 C2 |-> C3
%D 2D
%D 2D +20 D0 <=> D1
%D 2D
%D 2D +20 E0 |-> E1
%D 2D +10 E2 --> E3
%D 2D
%D ren A0 A1 ==> \Px \exxp∧\Px
%D ren A2 A3 ==> \Qx \exxp∧\Qx
%D ren B0 B1 ==> \Rxx \Rxxp
%D ren B2 B3 ==> \Sxx \Sxxp
%D ren C0 C1 ==> \Tx \exxp⊸\Tx
%D ren C2 C3 ==> \Ux \exxp⊸\Ux
%D ren D0 D1 ==> 𝐛P(X) 𝐛P(X{×}X)
%D ren E0 E1 ==> x (x,x')
%D ren E2 E3 ==> X X{×}X
%D
%D (( A0 A1 |->
%D A2 A3 |->
%D B0 B1 <-|
%D B2 B3 <-|
%D C0 C1 |->
%D C2 C3 |->
%D A0 A3 harrownodes nil 20 nil |->
%D A2 B1 harrownodes nil 20 nil |-> sl^
%D A2 B1 harrownodes nil 20 nil <-| sl_
%D B0 B3 harrownodes nil 20 nil <-|
%D B2 C1 harrownodes nil 20 nil <-| sl^
%D B2 C1 harrownodes nil 20 nil |-> sl_
%D C0 C3 harrownodes nil 20 nil |->
%D A0 A2 -> .plabel= l α
%D A1 A3 -> .plabel= r Σ_Δα
%D A2 B0 -> .plabel= l \sm{f\\(Σ_Δ^♯)g}
%D A3 B1 -> .plabel= r \sm{(Σ_Δ^♭)f\\g}
%D B0 B2 -> .plabel= l Δ^*β
%D B1 B3 -> .plabel= r β
%D B2 C0 -> .plabel= l \sm{(Π_Δ^♭)h\\k}
%D B3 C1 -> .plabel= r \sm{h\\(Π_Δ^♯)k}
%D C0 C2 -> .plabel= l γ
%D C1 C3 -> .plabel= r Π_Δγ
%D D0 D1 -> sl^^ .plabel= a Σ_Δ
%D D0 D1 <- .plabel= m Δ^*
%D D0 D1 -> sl__ .plabel= b Π_Δ
%D E0 E1 |->
%D E2 E3 -> .plabel= a Δ
%D
%D A1 A3 midpoint relplace 65 0 Σ_Δα:=\pdedscale{0.55}{SigmaD-F}
%D A3 B1 midpoint relplace 65 0 (Σ_Δ^♭)f:=\pdedscale{0.55}{SigmaD-transposeright}
%D A2 B0 midpoint relplace -65 0 (Σ_Δ^♯)g:=\pdedscale{0.45}{SigmaD-transposeleft}
%D B0 B2 midpoint relplace -65 0 Δ^*β:=\pdedscale{0.55}{Dstar-F}
%D B2 C0 midpoint relplace -65 0 (Π_Δ^♭)h:=\pdedscale{0.40}{PiD-transposeleft}
%D B3 C1 midpoint relplace 65 0 (Π_Δ^♯)k:=\pdedscale{0.40}{PiD-transposeright}
%D C1 C3 midpoint relplace 65 0 Π_Δγ:=\pdedscale{0.55}{PiD-F}
%D ))
%D enddiagram
%D
\pu
\phantom{a}
\hspace{-70pt}
$
\diag{adjs-Delta*}
$
\newpage
% «adjoints-subst» (to ".adjoints-subst")
We also have adjoints to this functor,
%
$$\cmat{R(f(x))\\x∈X}
\diagxyto/<-|/<200>
\cmat{R(y)\\y∈Y}
$$
%
and they are a bit harder to build than the ones in the previous page
--- and they force us to learn how to handle functions in ND.
\def\Px{Px}
\def\Qx{Qx}
\def\Ry{Ry}
\def\Sy{Sy}
\def\Rfx{Rfx}
\def\Sfx{Sfx}
\def\Tx{Txy}
\def\Ux{Uxy}
\def\Exx{∃x.}
\def\Fax{∃x.}
\def\fxy{fx{=}y}
\def\fxfx{fx{=}fx}
\def\Pxy{Pxy}
\def\Qxy{Qxy}
\def\Rx {Rx}
\def\Sx {Sx}
\def\Tx {Tx}
\def\Ux {Ux}
\def\Exy{∃y.}
\def\Fay{∀y.}
\bsk
%:
%:
%:
%: [\fxy∧\Px]^1
%: ------------
%: [\fxy∧\Px]^1 \Px
%: ------------ :::α
%: \fxy \Qx
%: -----------------
%: \fxy∧\Qx
%: ------------
%: \Exx\fxy∧\Px \Exx\fxy∧\Qx
%: ----------------------------1
%: \Exx\fxy∧\Qx
%:
%: ^Sigmaf-F
%:
%:
%:
%:
%:
%: [\fxy∧\Qx]^1
%: ------------
%: [\fxy∧\Qx]^1 \Exx\fxy∧\Qx
%: ----- ------------ :::
%: \fxfx \Qx \fxy \Ry
%: ---------- -------------------
%: \fxfx∧\Qx \Rfx
%: -----------------[y:=fx];1
%: \Rfx
%:
%: ^Sigmaf-transposeleft
%:
%: [\fxy∧\Qx]^1
%: ------------
%: [\fxy∧\Qx]^1 \Qx
%: ------------ ::::f
%: \fxy \Rfx
%: --------------
%: \Exx\fxy∧\Qx \Ry
%: ---------------------1
%: \Ry
%:
%: ^Sigmaf-transposeright
%:
%:
%:
%: [\Ry]^1
%: :::::β
%: \Rfx \Sy
%: ----------[y:=fx]^1
%: \Sfx
%:
%: ^fstar-F
%:
%:
%: [\Sy]^1
%: ::::::::::::h
%: \Fay\fxy⊸\Tx
%: ------------
%: \Sfx \fxy⊸\Tx
%: ----- ------------------[y:=fx];1
%: \fxfx \fxfx⊸\Tx
%: ---------------------
%: \Tx
%:
%: ^Pif-transposeleft
%:
%:
%: [\fxy]^1 [\Sy]^2
%: ----------------
%: Sfx
%: :::
%: Tx
%: --------1
%: \Sy \fxy⊸\Tx
%: -------------2
%: \Fax\fxy⊸\Tx
%:
%: ^Pif-transposeright
%:
%:
%: [\fxy]^1 [\fxy⊸\Tx]^2
%: ----------------------
%: \Tx
%: :::γ
%: \Ux
%: --------1
%: \Fax\fxy⊸\Tx \fxy⊸\Ux
%: -----------------------2
%: \Fax\fxy⊸\Ux
%:
%: ^Pif-F
%:
%D diagram adjs-f*
%D 2Dx 100 +40
%D 2D 100 A0 |-> A1
%D 2D | |
%D 2D | |-> |
%D 2D | |
%D 2D +25 A2 |-> A3
%D 2D | |
%D 2D | <-> |
%D 2D | |
%D 2D +25 B0 <-| B1
%D 2D | |
%D 2D | <-| |
%D 2D | |
%D 2D +25 B2 <-| B3
%D 2D | |
%D 2D | <-> |
%D 2D | |
%D 2D +25 C0 |-> C1
%D 2D | |
%D 2D | |-> |
%D 2D | |
%D 2D +25 C2 |-> C3
%D 2D
%D 2D +20 D0 <=> D1
%D 2D
%D 2D +20 E0 |-> E1
%D 2D +10 E2 --> E3
%D 2D
%D ren A0 A1 ==> \Px \Exx\fxy∧\Px
%D ren A2 A3 ==> \Qx \Exx\fxy∧\Qx
%D ren B0 B1 ==> \Rfx \Ry
%D ren B2 B3 ==> \Sfx \Sy
%D ren C0 C1 ==> \Tx \Exx\fxy⊸\Tx
%D ren C2 C3 ==> \Ux \Exx\fxy⊸\Ux
%D ren D0 D1 ==> 𝐛P(X) 𝐛P(Y)
%D ren E0 E1 ==> x fx
%D ren E2 E3 ==> X Y
%D
%D (( A0 A1 |->
%D A2 A3 |->
%D B0 B1 <-|
%D B2 B3 <-|
%D C0 C1 |->
%D C2 C3 |->
%D A0 A3 harrownodes nil 20 nil |->
%D A2 B1 harrownodes nil 20 nil |-> sl^
%D A2 B1 harrownodes nil 20 nil <-| sl_
%D B0 B3 harrownodes nil 20 nil <-|
%D B2 C1 harrownodes nil 20 nil <-| sl^
%D B2 C1 harrownodes nil 20 nil |-> sl_
%D C0 C3 harrownodes nil 20 nil |->
%D A0 A2 -> .plabel= l α
%D A1 A3 -> .plabel= r Σ_πα
%D A2 B0 -> .plabel= l \sm{f\\(Σ_π^♯)g}
%D A3 B1 -> .plabel= r \sm{(Σ_π^♭)f\\g}
%D B0 B2 -> .plabel= l π^*β
%D B1 B3 -> .plabel= r β
%D B2 C0 -> .plabel= l \sm{(Π_π^♭)h\\k}
%D B3 C1 -> .plabel= r \sm{h\\(Π_π^♯)k}
%D C0 C2 -> .plabel= l γ
%D C1 C3 -> .plabel= r Π_πγ
%D D0 D1 -> sl^^ .plabel= a Σ_f
%D D0 D1 <- .plabel= m f^*
%D D0 D1 -> sl__ .plabel= b Π_f
%D E0 E1 |->
%D E2 E3 -> .plabel= a π
%D
%D A1 A3 midpoint relplace 70 0 Σ_πα:=\pdedscale{0.40}{Sigmaf-F}
%D A3 B1 midpoint relplace 70 0 (Σ_π^♭)f:=\pdedscale{0.40}{Sigmaf-transposeright}
%D A2 B0 midpoint relplace -70 0 (Σ_π^♯)g:=\pdedscale{0.40}{Sigmaf-transposeleft}
%D B0 B2 midpoint relplace -50 0 π^*β:=\pdedscale{0.55}{fstar-F}
%D B2 C0 midpoint relplace -60 0 (Π_π^♭)h:=\pdedscale{0.40}{Pif-transposeleft}
%D B3 C1 midpoint relplace 55 0 (Π_π^♯)k:=\pdedscale{0.40}{Pif-transposeright}
%D C1 C3 midpoint relplace 70 0 Π_πγ:=\pdedscale{0.40}{Pif-F}
%D ))
%D enddiagram
%D
\pu
\phantom{a}
\hspace{-75pt}
$
\diag{adjs-f*}
$
\bsk
All this {\sl suggests} that it should be possible to interpret
first-order logic in categories in which all functors of the form
$f^*$ have both adjoints... but it turns out that we need Frobenius,
Beck-Chevalley, and lots of other technicalities.
% (find-idarctpage 15 "13. Hyperdoctrines")
% (find-idarcttext 15 "13. Hyperdoctrines")
\newpage
% «exists-examples» (to ".exists-examples")
% (shyp 6 "exists-examples")
% (shy "exists-examples")
\subsection*{The adjunction $∃⊣π^*$ for children}
The main diagram:
%D diagram adjunction-exists-motivation-1
%D 2Dx 100 +50
%D 2D 100 A0 A1
%D 2D
%D 2D +35 A2 A3
%D 2D
%D 2D +0 A4 A5
%D 2D
%D 2D +20 B0 B1
%D 2D
%D 2D +15 C0 C1
%D 2D
%D ren A0 A1 ==> P(x,y) ∃y{∈}Y.\,P(x,y)
%D ren A2 A3 ==> Q(x) Q(x)
%D ren A4 A5 ==> R(x,y) ∀y{∈}Y.\,R(x,y)
%D ren B0 B1 ==> 𝐛P(X{×}Y) 𝐛P(X)
%D ren C0 C1 ==> X{×}Y X
%D
%D (( A0 A1 |-> .plabel= a (∃F)
%D A0 A2 -> .plabel= l \sm{f\\x,y|P(x,y)⊢Q(x)\\(∃L)g}
%D A1 A3 -> .plabel= r \sm{(∃R)f\\x|∃y∈Y.P(x,y)⊢Q(x)\\g}
%D A0 A3 harrownodes nil 20 nil |-> sl^^ .plabel= a (∃R)
%D A0 A3 harrownodes nil 20 nil <->
%D A0 A3 harrownodes nil 20 nil <-| sl__ .plabel= b (∃L)
%D A2 A3 <-| .plabel= b π^*
%D # A2 A4 -> .plabel= l Q(x)⊢R(x,y)
%D # A3 A5 -> .plabel= r Q(x)⊢∀y∈Y.R(x,y)
%D # A2 A5 harrownodes nil 20 nil <->
%D # A4 A5 |->
%D
%D B0 B1 -> sl^ .plabel= a (∃F)
%D B0 B1 <- sl_ .plabel= b π^*
%D
%D C0 C1 -> .plabel= a π
%D ))
%D enddiagram
%D
\pu
$$\diag{adjunction-exists-motivation-1}
$$
The `$↔$' in the middle of the square says that $x,y|P(x,y)⊢Q(x)$ is
true if and only if $x|∃y∈Y.P(x,y)⊢Q(x)$ is true. The operation $(∃R)$
receives an inclusion morphism
%
$$f: \;\; \cmat{P(x,y)\\(x,y)∈X×Y} → \cmat{∃y∈Y.P(x,y)\\x∈X}$$
%
and returns an inclusion morphism
%
$$(∃R)f: \;\; \cmat{∃y∈Y.P(x,y)\\x∈X} → \cmat{P(x,y)\\(x,y)∈X×Y};$$
%
The operation $(∃L)$ does the reverse.
\bsk
\bsk
The `$↔$' is usually represented as bidirectional rule, and there's a
similar bidirectional rule for the universal. Here they are (see
\cite[p.230]{Jacobs} and \cite[p.67]{NegriVonPlato}):
%:
%:
%: x∈Y,y∈Y|P(x,y)⊢Q(x)
%: ====================(∃\text{-mate})
%: x∈Y|∃y∈Y.P(x,y)⊢Q(x)
%:
%: ^Ex-mate
%:
%: x∈Y,y∈Y|Q(x)⊢R(x,y)
%: ====================(∀\text{-mate})
%: x∈Y|Q(x)⊢∀y∈Y.R(x,y)
%:
%: ^Fa-mate
%:
\pu
$$\ded{Ex-mate}
\qquad
\ded{Fa-mate}
$$
%
% (find-books "__cats/__cats.el" "jacobs")
% (find-jacobspage (+ 19 230) "mate")
%
% (find-books "__logic/__logic.el" "negri-vonplato")
% (find-negrivpspfpage (+ 19 64) "Quantifiers in natural deduction")
% (find-negrivpspfpage (+ 19 67) "G3i" "restriction")
% (find-negrivpspftext (+ 19 67) "G3i" "restriction")
% (find-negrivpspfpage (+ 19 98) "5.2. Sequent calculi in natural deduction style")
%
% (find-books "__logic/__logic.el" "van_dalen")
% (find-vdlspage (+ 12 91) "2.8 Natural Deduction")
% (find-vdlspage (+ 12 96) "2.9 Adding the Existential Quantifier")
%
For a discussion of the problems that appear if we allow $Q(x)$ to
depend on $y$, see \cite[pp.91--99]{VanDalen}.
\newpage
% «exists-examples-2» (to ".exists-examples-2")
% (shyp 7 "exists-examples-2")
% (shy "exists-examples-2")
\subsection*{The adjunction $∃⊣π^*$ for children (2)}
Let's write $A \diagxyto/->/^{\frown} B$ for ``there are no morphisms
from $A$ to $B$'', i.e., $\Hom(A,B)=∅$. Let $X=\{0,1,2,3,4\}$ and
$Y=\{0,1\}$. Let $Q(x) = (x≥3)$, and let's compare what happens for
two different choices of $P$; in the left we have $P(x,y)=(x-y≥3)$, and in
the right we have $P(x,y)=(x-y≥1)$.
%D diagram adjunction-exists-example-1
%D 2Dx 100 +35
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +0 B0 B1
%D 2D
%D 2D +15 C0 C1
%D 2D
%D ren A0 A1 ==> \sm{00001\\00011} \sm{00011}
%D ren A2 A3 ==> \sm{00111\\00111} \sm{00111}
%D ren C0 C1 ==> \sm{•••••\\•••••} \sm{•••••}
%D
%D (( A0 A1 |-> .plabel= a (∃F)
%D A0 A2 -> .plabel= l !
%D A1 A3 -> .plabel= r !
%D A0 A3 harrownodes nil 20 nil <->
%D A2 A3 <-| .plabel= b π^*
%D
%D C0 C1 -> .plabel= a π
%D ))
%D enddiagram
%D
%D diagram adjunction-exists-example-2
%D 2Dx 100 +35
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +0 B0 B1
%D 2D
%D 2D +15 C0 C1
%D 2D
%D ren A0 A1 ==> \sm{00111\\01111} \sm{01111}
%D ren A2 A3 ==> \sm{00111\\00111} \sm{00111}
%D ren C0 C1 ==> \sm{•••••\\•••••} \sm{•••••}
%D
%D (( A0 A1 |-> .plabel= a (∃F)
%D A0 A2 -> .plabel= l \frown
%D A1 A3 -> .plabel= r \frown
%D A0 A3 harrownodes nil 20 nil <->
%D A2 A3 <-| .plabel= b π^*
%D
%D C0 C1 -> .plabel= a π
%D ))
%D enddiagram
%D
$$\pu
\diag{adjunction-exists-example-1}
\qquad
\diag{adjunction-exists-example-2}
$$
\bsk
%D diagram adjunction-exists-example-1-abs
%D 2Dx 100 +60
%D 2D 100 A0 A1
%D 2D
%D 2D +35 A2 A3
%D 2D
%D 2D +20 C0 C1
%D 2D
%D ren A0 A1 ==> \cmat{x-y≥3\\(x,y){∈}X{×}Y} \cmat{∃y{∈}Y.\;x-y≥3\\x∈X}
%D ren A2 A3 ==> \cmat{x≥2\\(x,y){∈}X{×}Y} \cmat{x≥2\\x∈X}
%D ren C0 C1 ==> X×Y X
%D
%D (( A0 A1 |-> .plabel= a (∃F)
%D A0 A2 -> .plabel= l !
%D A1 A3 -> .plabel= r !
%D A0 A3 harrownodes nil 20 nil <->
%D A2 A3 <-| .plabel= b π^*
%D
%D C0 C1 -> .plabel= a π
%D ))
%D enddiagram
%D
%D diagram adjunction-exists-example-2-abs
%D 2Dx 100 +60
%D 2D 100 A0 A1
%D 2D
%D 2D +35 A2 A3
%D 2D
%D 2D +20 C0 C1
%D 2D
%D ren A0 A1 ==> \cmat{x-y≥1\\(x,y){∈}X{×}Y} \cmat{∃y{∈}Y.\;x-y≥1\\x∈X}
%D ren A2 A3 ==> \cmat{x≥2\\(x,y){∈}X{×}Y} \cmat{x≥2\\x∈X}
%D ren C0 C1 ==> X×Y X
%D
%D (( A0 A1 |-> .plabel= a (∃F)
%D A0 A2 -> .plabel= l \frown
%D A1 A3 -> .plabel= r \frown
%D A0 A3 harrownodes nil 20 nil <->
%D A2 A3 <-| .plabel= b π^*
%D
%D C0 C1 -> .plabel= a π
%D ))
%D enddiagram
%D
$$\pu
\diag{adjunction-exists-example-1-abs}
\qquad
\diag{adjunction-exists-example-2-abs}
$$
\newpage
% «exists-cat-rules-to-ND» (to ".exists-cat-rules-to-ND")
% (shyp 7 "exists-cat-rules-to-ND")
% (shy "exists-cat-rules-to-ND")
\subsection*{Translating the categorical rules for `exists'}
The main diagram, again:
$$\diag{adjunction-exists-motivation-1}
$$
Here's how to translate the categorical rules $(∃R)$ and $(∃L)$ (the
``transpositions'') to Natural Deduction:
%:
%:
%: [Pxy]^1
%: :f
%: x,y|Pxy⊢Qx f ∃x.Pxy Qx
%: -----------(∃R) -----(∃R) (∃R)f := ------------(∃E);1
%: x|∃y.Pxy⊢Qx (∃R)f Qx
%:
%: ^ExR-1 ^ExR-2 ^ExR-3
%:
%:
%: Pxy
%: ------(∃I)
%: x|∃y.Pxy⊢Qx g ∃y.Pxy
%: -----------(∃L) -----(∃L) (∃L)g := ::::::g
%: x,y|Pxy⊢Qx (∃L)g Qx
%:
%: ^ExL-1 ^ExL-2 ^ExL-3
%:
%:
%:
$$\pu
\begin{array}{ccc}
\cded{ExR-1} & \cded{ExR-2} & (∃R)f := \pded{ExR-3} \\ \\
\cded{ExL-1} & \cded{ExL-2} & (∃L)g := \pded{ExL-3} \\
\end{array}
$$
\newpage
% «exists-elim-to-cats» (to ".exists-elim-to-cats")
% (shyp 8 "exists-elim-to-cats")
% (shy "exists-elim-to-cats")
\subsection*{Translating the rule $(∃E)$ from ND to categories}
The main diagram, again:
$$\diag{adjunction-exists-motivation-1}
$$
Here's how to translate an application of the rule $(∃E)$ from Natural
Deduction to a series of steps that are easy to interpret
categorically. The rules $(⊸I)$ and $(⊸E)$ are transpositions of
another adjunction. TODO: the categorical drawings (the ``missing
diagrams''), and the translation of $(∃I)$.
%:
%: x,y|Pxy,Qx,Rx⊢Sx
%: ----------------(⊸I)
%: x,y|Pxy,Qx⊢Rx⊸Sx
%: ------------------(⊸I)
%: x,y|Pxy⊢Qx⊸(Rx⊸Sx)
%: -------------------(∃R)
%: x|∃y.Pxy⊢Qx⊸(Rx⊸Sx)
%: -------------------(⊸E)
%: x,y|Pxy,Qx,Rx⊢Sx x|∃y.Pxy,Qx⊢Rx⊸Sx
%: -----------------(∃E) -----------------(⊸E)
%: x|∃y.Pxy,Qx,Rx⊢Sx x|∃y.Pxy,Qx,Rx⊢Sx
%:
%: ^ExE-1 ^ExE-2
%:
%:
%:
%: [Pxy]^3 [Qx]^2 [Rx]^1
%: :::::::::::::::::::::::
%: Sx
%: -----(⊸I);1
%: Rx⊸Sx
%: ----------(⊸I);2
%: ∃y.Pxy Qx⊸(Rx⊸Sx)
%: ---------------------(∃R);3
%: [Pxy]^1 Qx Rx Qx Qx⊸(Rx⊸Sx)
%: ::::::::::::::: ------------------(⊸E)
%: ∃y.Pxy Sx Rx Rx⊸Sx
%: -----------------(∃E);1 -----------(⊸E)
%: Sx Sx
%:
%: ^ExE-1-ND ^ExE-2-ND
%:
%:
%:
\pu
$$\ded{ExE-1-ND} \quad ⇒ \quad \ded{ExE-2-ND}$$
$$\ded{ExE-1} \quad ⇒ \quad \ded{ExE-2}$$
\newpage
% «exists-intro-to-cats» (to ".exists-intro-to-cats")
% (shyp 9 "exists-intro-to-cats")
% (shy "exists-intro-to-cats")
\subsection*{Translating the rule $(∃I)$ from ND to categories}
Let's divide $(∃I)$ in two cases...
%:
%: -------------------\id
%: P(x,y) ∃y.P(x,y)⊢∃y.P(x,y)
%: ---------(∃I) -------------------(∃L)
%: ∃y.P(x,y) P(x,y)⊢∃y.P(x,y)
%:
%: ^exI-1 ^exI-2
%:
%:
%: -------------------\id
%: ∃y.P(x,y)⊢∃y.P(x,y)
%: -------------------(∃L)
%: P(x,b(x)) P(x,y)⊢∃y.P(x,y)
%: ---------(∃I) -------------------y:=b(x)
%: ∃y.P(x,y) P(x,b(x))⊢∃y.P(x,y)
%:
%: ^exI-3 ^exI-4
%:
%:
%:
\pu
$$\ded{exI-1} \qquad \ded{exI-2}$$
$$\ded{exI-3} \qquad \ded{exI-4}$$
\bsk
A categorical diagram (for the two cases):
%D diagram ??
%D 2Dx 100 +50 +50
%D 2D 100 A0 A1 A2
%D 2D
%D 2D +30 A3 A4 A5
%D 2D
%D 2D +20 B0 B1 B2
%D 2D
%D 2D +10 C0 C1 C2
%D 2D
%D ren A0 A1 A2 ==> P(x,b(x)) P(x,y) ∃y{∈}Y.P(x,y)
%D ren A3 A4 A5 ==> ∃y{∈}Y.P(x,y) ∃y{∈}Y.P(x,y) ∃y{∈}Y.P(x,y)
%D ren B0 B1 B2 ==> x (x,b(x)) x
%D ren C0 C1 C2 ==> X X{×}Y Y
%D
%D (( A0 A1 <-| A1 A2 |->
%D A0 A3 -> .plabel= l 〈\id,b〉^*(∃L)\id
%D A1 A4 -> .plabel= m (∃L)\id
%D A2 A5 -> .plabel= r \id
%D A0 A4 harrownodes nil 20 nil <-| .plabel= a 〈\id,b〉^*
%D A1 A5 harrownodes nil 20 nil <-| .plabel= a (∃L)
%D A3 A4 <-|
%D A4 A5 <-|
%D
%D B0 B1 |->
%D B1 B2 |->
%D
%D C0 C1 -> .plabel= a 〈\id,b〉
%D C1 C2 -> .plabel= a π
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
\newpage
% «bounded-quantifiers» (to ".bounded-quantifiers")
% (shyp 10 "bounded-quantifiers")
% (shy "bounded-quantifiers")
\subsection*{Bounded quantifiers}
$\begin{array}{rcl}
∀y∈Y. Pxy &:=& ∀y.y∈Y→Pxy \\
∃y∈Y. Pxy &:=& ∃y.y∈Y∧Pxy \\
(!)y. Pxy &:=& Pxy∧Pxy'→y=y' \\
(!)y∈Y.Pxy &:=& y∈Y∧y'∈Y∧Pxy∧Pxy'→y=y' \\
∃!y. Pxy &:=& (∃y.Pxy)∧((!)y.Pxy) \\
∃!y∈Y. Pxy &:=& (∃y∈Y.Pxy)∧((!)y∈Y.Pxy) \\
\end{array}
$
\newpage
% «ND-in-hyps» (to ".ND-in-hyps")
% (shyp 11 "ND-in-hyps")
% (shy "ND-in-hyps")
\subsection*{Interpreting ND in hyperdoctrines}
% $$x:X,y:Y|P(x,y),Q(x,y)⊢R(x,y)$$ the ``$x:X,y:Y$'' is the {\sl type
% context} and the $P(x,y),Q(x,y)$ is the {\sl proposition context}.
% (find-books "__cats/__cats.el" "jacobs")
% (find-jacobspage (+ 19 225) "Rules for (many-typed) first order predicate logic")
\def\Cx .{x;\,}
\def\Cxy.{x,y;\,}
\def\fxy{fx{=}y}
See pages 223--225 of \cite{Jacobs}. We have:
%D diagram ??
%D 2Dx 100
%D 2D 100 A
%D 2D
%D 2D +30 B
%D 2D
%D ren A ==> \cmat{P(x,y)\\(x,y)∈X{×}Y}
%D ren B ==> \cmat{Q(y)\\(x,y)∈X{×}Y}
%D
%D (( A B -> .plabel= l f
%D A relplace 70 0 =\;\;x:X,y:Y⊢P(x,y):𝐬{Prop}
%D A B midpoint
%D relplace 70 0 =\;\;x:X,y:Y\;|\;P(x,y)⊢Qy
%D B relplace 70 0 =\;\;x:X,y:Y⊢Q(y):𝐬{Prop}
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
Two examples of translations (to sequents à là Jacobs):
%:
%: [\Pxy]^1
%: ::::::α
%: \Qxy
%: --------
%: \Exy\Pxy \Exy\Qxy
%: ----------------------1
%: \Exy\Qxy
%:
%: ^Sigmapi-F
%:
%:
%: \Cxy.Pxy⊢Qxy
%: ----------------
%: \Cxy.Pxy⊢∃y∈Y.Qxy
%: ---------------------
%: \Cx.∃y∈Y.Pxy⊢∃y∈Y.Qxy
%:
%: ^Sigmapi-F-tocat
%:
%:
%: [\fxy∧\Px]^1
%: ------------
%: [\fxy∧\Px]^1 \Px
%: ------------ :::α
%: \fxy \Qx
%: -----------------
%: \fxy∧\Qx
%: ------------
%: \Exx\fxy∧\Px \Exx\fxy∧\Qx
%: ----------------------------1
%: \Exx\fxy∧\Qx
%:
%: ^Sigmaf-F
%:
%:
%:
%:
%: \Cx.\Px⊢\Qx
%: ----------------- ------------
%: \Cxy.\fxy∧\Px⊢\Px \Cxy.\Px⊢\Qx
%: --------------------------------
%: \Cxy.\fxy∧\Px⊢\Qx
%: ------------------ --------------------
%: \Cxy.\fxy∧\Px⊢\fxy \Cxy.\fxy∧\Px⊢\Qx
%: --------------------------------------
%: \Cxy.\fxy∧\Px⊢\fxy∧\Qx
%: ----------------------
%: \Cxy.\fxy∧\Px⊢∃y.\fxy∧\Qx
%: ----------------------
%: \Cx.∃y.\fxy∧\Px⊢∃y.\fxy∧\Qx
%:
%: ^Sigmaf-F-tocat
%:
\pu
$$\ded{Sigmapi-F} \quad ⇒ \quad \ded{Sigmapi-F-tocat}$$
$$\ded{Sigmaf-F}$$
$$⇒ \qquad \ded{Sigmaf-F-tocat}$$
\newpage
% (find-seelyhyppage (+ -504 505) "1. First Order Logic")
% (find-seelyhyppage (+ -504 507) "equality rules")
% «sec-4» (to ".sec-4")
% (find-seelyhyppage (+ -504 512) "4. Construction 1: LPCE -> Hyperdoctrine")
% «page-513» (to ".page-513")
% (find-seelyhyppage (+ -504 513) "(5') (i)")
% (find-LATEX "2008hyp-utf8.tex" "adj-functors-as-ND-proofs-2")
{\bf Page 513 (5') (i):}
\def\tyx {tx{=}y}
\def\tyxi{tξ{=}y}
\def\fxy {f(x){=}y}
%D diagram p513
%D 2Dx 100 +25 +35 +45
%D 2D 100 A0 |-> A1 B0 |-> B1
%D 2D | | | |
%D 2D +25 A2 |-> A3 B2 |-> B3
%D 2D
%D 2D +20 X ---> Y
%D 2D
%D ren A0 A1 ==> γ Σ_tγ
%D ren A2 A3 ==> φ Σ_tφ
%D ren B0 B1 ==> γ(x) ∃ξ(\tyxi∧γ(ξ))
%D ren B2 B3 ==> φ(x) ∃ξ(\tyxi∧φ(ξ))
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l \ovl{P}
%D A1 A3 -> .plabel= r Σ_t\ovl{P}
%D A0 A3 harrownodes nil 20 nil |->
%D A2 A3 |->
%D
%D B0 B1 |->
%D B0 B2 -> .plabel= l \ovl{P}
%D B1 B3 -> .plabel= r Σ_t\ovl{P}
%D B0 B3 harrownodes nil 20 nil |->
%D B2 B3 |->
%D
%D X Y -> .plabel= a t
%D ))
%D enddiagram
%D
$$\pu
\diag{p513}
$$
%D diagram p513-my
%D 2Dx 100 +25 +35 +50
%D 2D 100 A0 |-> A1 B0 |-> B1
%D 2D | | | |
%D 2D +25 A2 |-> A3 B2 |-> B3
%D 2D
%D 2D +20 X ---> Y
%D 2D
%D ren A0 A1 ==> P Σ_fP
%D ren A2 A3 ==> Q Σ_fQ
%D ren B0 B1 ==> P(x) ∃x⠆X.(f(x){=}y∧P(x))
%D ren B2 B3 ==> Q(x) ∃x⠆X.(f(x){=}y∧Q(x))
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l g
%D A1 A3 -> .plabel= r Σ_fg
%D A0 A3 harrownodes nil 20 nil |->
%D A2 A3 |->
%D
%D B0 B1 |->
%D B0 B2 -> .plabel= l g
%D B1 B3 -> .plabel= r Σ_fg
%D B0 B3 harrownodes nil 20 nil |->
%D B2 B3 |->
%D
%D X Y -> .plabel= a f
%D ))
%D enddiagram
%D
%$$\pu
% \diag{p513-my}
%$$
%:
%: γ(x)
%: ....
%: P
%: ....
%: φ(x)
%:
%: ^p513-1
%:
%: \tyx∧γ(x)
%: ---------(∧E)
%: [γ(x)]
%: ......
%: P \tyx∧γ(x)
%: .... ---------(∧E)
%: φ(x) \tyx
%: ----------------(∧I)
%: \tyx∧φ(x)
%: --------------(∃I)
%: ∃ξ(\tyxi∧γ(ξ)) ∃ξ(\tyxi∧φ(ξ))
%: -----------------------------------(∃E)
%: ∃ξ(\tyxi∧φ(ξ))
%:
%: ^p513-2
%:
%:
%: [\fxy∧P(x)]^1
%: ---------(∧E)
%: P(x) [\fxy∧P(x)]^1
%: ::::g ---------(∧E)
%: Q(x) \fxy
%: ------------------(∧I)
%: \fxy∧Q(x)
%: --------------(∃I)
%: ∃x⠆X.(\fxy∧P(x)) ∃x⠆X.(\fxy∧Q(x))
%: -----------------------------------(∃E);1
%: ∃x⠆X.(\fxy∧Q(x))
%:
%: ^p513-2-my
%:
%:
\pu
\def\pded#1{\left(\cded{#1}\right)}
If $\ovl{P}$ is represented by a derivation $\pded{p513-1}$
\msk
then $Σ_t\ovl{P}$ i.r.\ by $\pded{p513-2}$
\bsk
In my notation:
%
$$\pu
\diag{p513-my}
$$
$$Σ_fg = \pded{p513-2-my}$$
\newpage
% _____ _ _
% |___ / | | | |_ _ _ __ ___
% |_ \ | |_| | | | | '_ \/ __|
% ___) | | _ | |_| | |_) \__ \
% |____(_) |_| |_|\__, | .__/|___/
% |___/|_|
%
% «3._hyperdoctrines» (to ".3._hyperdoctrines")
% (shyp 6 "3._hyperdoctrines")
% (shy "3._hyperdoctrines")
% (find-seelyhyppage (+ -504 510) "3. Hyperdoctrines")
% (find-LATEX "2008hyp-utf8.tex" "adj-functors-as-ND-proofs")
\section*{\S3. Hyperdoctrines}
(P.510):
%D diagram hyp-def
%D 2Dx 100 +20 +20 +35
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +20 A4 A5
%D 2D
%D 2D +20 L0 B0 B1
%D 2D
%D 2D +20 L1 L2 C0 C1
%D 2D
%D ren A0 A1 ==> χ Σ_tχ
%D ren A2 A3 ==> t^*φ φ
%D ren A4 A5 ==> ψ Π_tψ
%D ren B0 B1 ==> 𝐛P(X) 𝐛P(Y)
%D ren C0 C1 ==> X Y
%D ren L0 L1 L2 ==> \Cat 𝐛T^\op 𝐛T
%D
%D (( A0 A1 |->
%D A0 A2 ->
%D A1 A3 ->
%D A0 A3 harrownodes nil 20 nil <->
%D A2 A3 <-|
%D A2 A4 ->
%D A3 A5 ->
%D A2 A5 harrownodes nil 20 nil <->
%D A4 A5 |->
%D
%D B0 B1 <- sl^^ .plabel= a Σ_t
%D B0 B1 -> .plabel= m t^*
%D B0 B1 <- sl__ .plabel= b Π_t
%D
%D C0 C1 -> .plabel= a t
%D
%D L0 L1 <- .plabel= l 𝐛P
%D L2 place
%D ))
%D enddiagram
%D
$$\pu
\diag{hyp-def}
$$
\bsk
Main cases, in the archetypal model:
%D diagram ??
%D 2Dx 100 +40 +40 +40 +20 +20
%D 2D 100 A0 A1 B0 B1 C0 C1
%D 2D
%D 2D +20 A2 A3 B2 B3 C2 C3
%D 2D
%D 2D +20 A4 A5 B4 B5 C4 C5
%D 2D
%D 2D +15 A6 A7 B6 B7 C6 C7
%D 2D
%D ren A0 A1 ==> P(a,b) ∃b∈B.P(a,b)
%D ren A2 A3 ==> Q(a) Q(a)
%D ren A4 A5 ==> R(a,b) ∀b∈B.R(a,b)
%D ren A6 A7 ==> A{×}B A
%D
%D ren B0 B1 ==> P(c) c{=}c'∧P(c)
%D ren B2 B3 ==> Q(c,c) Q(c,c')
%D ren B4 B5 ==> R(c) c{=}c'⊸R(c)
%D ren B6 B7 ==> C C{×}C
%D
%D ren C6 C7 ==> D E
%D
%D (( A0 A1 |->
%D A0 A2 ->
%D A1 A3 ->
%D A0 A3 harrownodes nil 20 nil <->
%D A2 A3 <-|
%D A2 A4 ->
%D A3 A5 ->
%D A2 A5 harrownodes nil 20 nil <->
%D A4 A5 |->
%D A6 A7 -> .plabel= a π
%D
%D B0 B1 |->
%D B0 B2 ->
%D B1 B3 ->
%D B0 B3 harrownodes nil 20 nil <->
%D B2 B3 <-|
%D B2 B4 ->
%D B3 B5 ->
%D B2 B5 harrownodes nil 20 nil <->
%D B4 B5 |->
%D B6 B7 -> .plabel= a Δ
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
\bsk
%D diagram ??
%D 2Dx 100 +65
%D 2D 100 C0 C1
%D 2D
%D 2D +20 C2 C3
%D 2D
%D 2D +20 C4 C5
%D 2D
%D 2D +15 C6 C7
%D 2D
%D ren C0 C1 ==> P(d) ∃d∈D.(f(d){=}e∧P(d))
%D ren C2 C3 ==> Q(f(d)) Q(e)
%D ren C4 C5 ==> R(d) ∀d∈D.(f(d){=}e⊸R(d))
%D ren C6 C7 ==> D E
%D
%D (( C0 C1 |->
%D C0 C2 ->
%D C1 C3 ->
%D C0 C3 harrownodes nil 20 nil <->
%D C2 C3 <-|
%D C2 C4 ->
%D C3 C5 ->
%D C2 C5 harrownodes nil 20 nil <->
%D C4 C5 |->
%D C6 C7 -> .plabel= a f
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
\newpage
The inverse image functor preserves products, coproducts, top, and
bottom:
%:
%:
%: \Hom_X(α,t^*(β∧γ))
%: ------------------≅
%: \Hom_Y(Σ_tα,β∧γ)
%: -----------------------------≅
%: \Hom_Y(Σ_tα,β)×\Hom_Y(Σ_tα,γ)
%: -----------------------------≅
%: \Hom_X(α,t^*β)×\Hom_Y(α,t^*γ)
%: -----------------------------≅
%: \Hom_X(α,t^*β∧t^*γ)
%:
%: ^hyp-cob-pres-and
%:
%:
%: \Hom_X(t^*(β∨γ),δ)
%: ------------------≅
%: \Hom_Y(β∨γ,Π_tδ)
%: -----------------------------≅
%: \Hom_Y(β,Π_tδ)×\Hom_Y(γ,Π_tδ)
%: -----------------------------≅
%: \Hom_X(t^*β,δ)×\Hom_Y(t^*γ,δ)
%: -----------------------------≅
%: \Hom_X(t^*β∨t^*γ,δ)
%:
%: ^hyp-cob-pres-or
%:
%:
%: \Hom_X(α,t^*⊤_Y)
%: ----------------≅
%: \Hom_Y(Σ_tα,⊤_Y)
%: ----------------≅
%: 1
%: -------------≅
%: \Hom_X(α,⊤_X)
%:
%: ^hyp-cob-pres-top
%:
%: \Hom_X(t^*⊥_Y,δ)
%: ----------------≅
%: \Hom_Y(⊥_Y,Π_tδ)
%: ----------------≅
%: 1
%: -------------≅
%: \Hom_X(⊥_X,δ)
%:
%: ^hyp-cob-pres-bot
%:
$$\pu
\begin{array}{ccc}
\ded{hyp-cob-pres-and}
& &
\ded{hyp-cob-pres-or}
\\ \\
t^*(β∧γ) ≅ t^*β∧t^*γ
& &
t^*(β∨γ) ≅ t^*β∨t^*γ
\\
\\
\ded{hyp-cob-pres-top}
& &
\ded{hyp-cob-pres-bot}
\\ \\
t^*⊤_Y ≅ ⊤_X
& &
t^*⊥_Y ≅ ⊥_X
\\
\end{array}
$$
\newpage
% ____ ____ ____ _ __
% | __ ) / ___/ ___| __| | ___ / _|
% | _ \| | | | / _` |/ _ \ |_
% | |_) | |__| |___ | (_| | __/ _|
% |____/ \____\____| \__,_|\___|_|
%
% «BCC-def» (to ".BCC-def")
% (shyp 7 "BCC-def")
% (shy "BCC-def")
% (find-seelyhyppage (+ -504 511) "Beck condition")
% (find-seelyhyppage (+ -504 511) "(5') (ii)")
\subsection*{3. (5') (ii): Beck-Chevalley}
(P.511):
Choose any commuting square in the base category. Name its objects and
morphisms like this:
%
%D diagram BCC-base-square
%D 2Dx 100 +20
%D 2D 100 A B
%D 2D
%D 2D +20 C D
%D 2D
%D ren A B C D ==> X Y X' Y'
%D
%D (( A B -> .plabel= a t
%D A C -> .plabel= l r
%D B D -> .plabel= r s
%D C D -> .plabel= a t'
%D ))
%D enddiagram
%D
$$\pu
\diag{BCC-base-square}
$$
Then for any object $φ∈|𝐛P(Y)|$ we can construct a map
%
$$(BCC→)_φ: Σ_rt^*φ → t^{\prime*}Σ_sφ.$$
%
Here's how:
%
%D diagram BCC-morphism
%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 ren B0 B1 ==> t^*φ φ
%D ren B2 B2' B3 ==> r^*t^{\prime*}Σ_sφ t^*s^*Σ_sφ s^*Σ_sφ
%D ren B4 B5 ==> Σ_rt^*φ Σ_sφ
%D ren B6 B7 ==> t^{\prime*}Σ_sφ Σ_sφ
%D ren b0 b1 ==> X Y
%D ren b2 b3 ==> X' Y'
%D ((
%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 -> .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 b1 -> .plabel= b t
%D b0 b2 -> .plabel= l r
%D b1 b3 -> .plabel= r s
%D b2 b3 -> .plabel= a t'
%D b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\pu
\diag{BCC-morphism}
$$
The Beck-Chevalley Condition says that when the base square is a
pullback then for any $φ∈|𝐛P(Y)|$ the map $(BCC→)_φ$ is an iso.
\newpage
% _____ _ _
% | ___| __ ___ | |__ ___ _ __ (_)_ _ ___
% | |_ | '__/ _ \| '_ \ / _ \ '_ \| | | | / __|
% | _|| | | (_) | |_) | __/ | | | | |_| \__ \
% |_| |_| \___/|_.__/ \___|_| |_|_|\__,_|___/
%
% «frobenius» (to ".frobenius")
% (shyp 99 "frobenius")
% (shy "frobenius")
\subsection*{3. (4') and (4''): Frobenius}
(P.511):
% (find-seelyhyppage (+ -504 511) "Note that we can replace (4) by:")
Note that we can replace (4) by:
(4') The ``inverse image'' functors $t^*$ preserve exponentiation.
(4'') for each $t:X→Y$ in $𝐛T$, $φ∈|𝐛P(X)|$, $ψ∈|𝐛P(Y)|$, the morphism
%
$$(\text{Frob}→): Σ_t(t^*ψ∧φ) → ψ∧Σ_tφ$$
%
is an isomorphism.
Condition (4') (or (4'')) is called {\sl Frobenius Reciprocity}.
% (hypp 11 "preservation-of-imp")
% (hyp "preservation-of-imp")
\msk
It is possible to prove that (4') implies (4'') and vice-versa. The
middle diagrams in the next page have the usual high-level proof. The
lower diagrams have a lower-level proof.
\newpage
%D diagram frob-1
%D 2Dx 100 +40 +45
%D 2D 100 A0 A2
%D 2D
%D 2D +20 A3 A4 A5
%D 2D
%D 2D +20 A6 A8
%D 2D
%D 2D +15 B0 B1
%D 2D
%D ren A0 A2 ==> α Σ_tα
%D ren A3 A4 A5 ==> α∧t^*β Σ_t(α∧t^*β) Σ_tα∧β
%D ren A6 A8 ==> t^*β β
%D ren B0 B1 ==> X Y
%D
%D (( A0 A2 |->
%D A0 A3 <- A2 A4 <- A2 A5 <-
%D A3 A4 |-> A4 A5 -> .plabel= a (\Frob→)
%D A3 A6 -> A4 A8 -> A5 A8 ->
%D A6 A8 <-
%D B0 B1 -> .plabel= a t
%D
%D A0 A3 midpoint A2 A4 midpoint harrownodes nil 20 nil |->
%D A3 A6 midpoint A4 A8 midpoint harrownodes nil 20 nil |->
%D ))
%D enddiagram
%D
%D diagram frob-upper-inner-0
%D 2Dx 100 +40
%D 2D 100 A0 A1
%D 2D
%D 2D +25 A3'
%D 2D +20 A2 A3
%D 2D
%D ren A0 A1 ==> α Σ_tα
%D ren A3' ==> Σ_tα∧β
%D ren A2 A3 ==> α∧t^*β Σ_t(α∧t^*β)
%D
%D (( A0 A1 |->
%D A0 A2 |-> A1 A3' |->
%D A3' A3 <- .plabel= l (\Frob→)
%D A2 A3 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{frob-1}
\qquad
\diag{frob-upper-inner-0}
$$
%D diagram frob-squares
%D 2Dx 100 +40 +40 +40
%D 2D 100 A0 A1 B0 B1
%D 2D
%D 2D +25 B3'
%D 2D +20 A2 A3 B2 B3
%D 2D
%D 2D +20 C0 C1 D0 D1
%D 2D +20 D0'
%D 2D
%D 2D +25 C2 C3 D2 D3
%D 2D
%D ren A0 A1 B0 B1 ==> 𝐛P(X) 𝐛P(Y) α Σ_tα
%D ren B3' ==> Σ_tα∧β
%D ren A2 A3 B2 B3 ==> 𝐛P(X) 𝐛P(Y) α∧t^*β Σ_t(α∧t^*β)
%D ren C0 C1 D0 D1 ==> 𝐛P(X) 𝐛P(Y) t^*(β⊸γ) β⊸γ
%D ren D0' ==> t^*β⊸t^*γ
%D ren C2 C3 D2 D3 ==> 𝐛P(X) 𝐛P(Y) t^*γ γ
%D
%D (( A0 A1 -> .plabel= a Σ_t
%D A0 A2 -> .plabel= l ∧t^*β
%D A1 A3 -> .plabel= r ∧β
%D A2 A3 -> .plabel= a Σ_t
%D
%D B0 B1 |->
%D B0 B2 |->
%D B1 B3' |->
%D B2 B3 |->
%D B3' B3 <-> .plabel= l (\Frob)
%D
%D C0 C1 <- .plabel= a t^*
%D C0 C2 <- .plabel= l t^*β⊸
%D C1 C3 <- .plabel= r ⊸β
%D C2 C3 <- .plabel= a t^*
%D
%D D0 D1 <-|
%D D0 D0' <-> .plabel= r (\PresExp)
%D D0' D2 <-|
%D D1 D3 <-|
%D D2 D3 <-|
%D ))
%D enddiagram
%D
$$\pu
\diag{frob-squares}
$$
%D diagram frob-hourglass
%D 2Dx 100 +35 +35 +25 +25 +30 +30
%D 2D 100 A0 A1 A2 A4 A5 A6
%D 2D
%D 2D +20 B0 B1 B3 B5 B6
%D 2D
%D 2D +20 C0 C1 C3 C5 C6
%D 2D
%D 2D +20 D0 D1 D2 D4 D5 D6
%D 2D
%D ren A0 A1 A2 A4 A5 A6 ==> α α∧t^*β Σ_t(α∧t^*β) Σ_tα∧β Σ_tα α
%D ren B0 B1 B3 B5 B6 ==> t^*β⊸t^*γ t^*γ γ β⊸γ t^*(β⊸γ)
%D ren C0 C1 C3 C5 C6 ==> Σ_t(α∧t^*β) α∧t^*β α Σ_tα Σ_tα∧β
%D ren D0 D1 D2 D4 D5 D6 ==> γ t^*γ t^*β⊸t^*γ t^*(β⊸γ) β⊸γ γ
%D
%D (( A0 B0 ->
%D A1 B1 ->
%D A2 A4 <-> .plabel= a (\Frob)
%D A2 B3 -> A4 B3 ->
%D A5 B5 ->
%D A6 B6 ->
%D
%D C0 D0 ->
%D C1 D1 ->
%D C3 D2 ->
%D C3 D4 ->
%D D2 D4 <-> .plabel= b (\PresExp)
%D C5 D5 ->
%D C6 D6 ->
%D
%D A0 B1 harrownodes nil 20 nil <->
%D A5 B6 harrownodes nil 20 nil <->
%D C0 D1 harrownodes nil 20 nil <->
%D C5 D6 harrownodes nil 20 nil <->
%D A1 B1 midpoint A2 B3 midpoint harrownodes nil 20 nil <->
%D A4 B3 midpoint A5 B5 midpoint harrownodes nil 20 nil <->
%D C1 D1 midpoint C3 D2 midpoint harrownodes nil 20 nil <->
%D C3 D4 midpoint C5 D5 midpoint harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
$$\pu
\diag{frob-hourglass}
$$
\newpage
% ____ _ _ __ _ ____ ____ _____
% | ___| | | | |_ _ _ __ \ \ | | | _ \ / ___| ____|
% |___ \ | |_| | | | | '_ \ _____\ \ | | | |_) | | | _|
% ___) | | _ | |_| | |_) | |_____/ / | |___| __/| |___| |___
% |____(_) |_| |_|\__, | .__/ /_/ |_____|_| \____|_____|
% |___/|_|
%
% «5._hyp-to-LPCE» (to ".5._hyp-to-LPCE")
% (find-seelyhyppage (+ -504 518) "5. Construction 2: Hyperdoctrine -> LPCE")
\section*{\S5. Construction 2: Hyperdoctrine $\to$ LPCE}
% «page-523» (to ".page-523")
% (find-seelyhyppage (+ -504 523) "We must now make sure")
% (find-LATEX "2008hyp-utf8.tex" "adj-functors-as-ND-proofs-2")
(P.523):
We must now make sure that all this is justified. (...) We must check
that the introduction and eleimination rules for $∃$ and $∀$ are
satisfied: for example, $(∃E)$ becomes the assertation...
\def\piY{{π_Y}}
\def\piY{{π_Y}}
%D diagram H->L-(ExE)
%D 2Dx 100 +25 +30 +40
%D 2D 100 A0 A1 B0 B1
%D 2D
%D 2D +20 A2 A3 B2 B3
%D 2D
%D 2D +20 A4 A5 B4 B5
%D 2D
%D ren A0 A1 A2 A3 ==> φ Σ_\piYφ π_Y^*φ' φ'
%D ren A4 A5 ==> X×Y Y
%D ren B0 B1 B2 B3 ==> P(x,y) ∃x⠆X.P(x,y) Q(y) Q(y)
%D ren B4 B5 ==> X×Y Y
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l α
%D A1 A3 -> .plabel= r β
%D A2 A3 <-|
%D A0 A3 harrownodes nil 20 nil |-> sl_ .plabel= a (∃E)
%D A4 A5 -> .plabel= a \piY
%D ))
%D (( B0 B1 |->
%D B0 B2 -> .plabel= l α
%D B1 B3 -> .plabel= r β
%D B2 B3 <-|
%D B0 B3 harrownodes nil 20 nil |-> sl_ .plabel= a (∃E)
%D B4 B5 -> .plabel= a \piY
%D ))
%D enddiagram
%D
%:
%: [P(x,y)]^1
%: ::::::::::α
%: ∃x⠆X.P(x,y) Q(y)
%: ---------------------(∃E);1
%: Q(y)
%:
%: ^H->L-(ExE)
%:
%:
$$\pu
\diag{H->L-(ExE)}
\qquad
\cded{H->L-(ExE)}
$$
%D diagram H->L-(ExI)
%D 2Dx 100 +35 +35 +50
%D 2D 100 A0 A1 B0 B1
%D 2D
%D 2D +20 A2 A3 B2 B3
%D 2D
%D 2D +20 A4 A5 B4 B5
%D 2D
%D ren A0 A1 A2 A3 ==> φ Σ_\piYφ π_Y^*Σ_\piYφ Σ_\piYφ
%D ren A4 A5 ==> X×Y Y
%D ren B0 B1 B2 B3 ==> P(x,y) ∃x⠆X.P(x,y) ∃x⠆X.P(x,y) ∃x⠆X.P(x,y)
%D ren B4 B5 ==> X×Y Y
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l η???
%D A1 A3 -> .plabel= r \id
%D A2 A3 <-|
%D A0 A3 harrownodes nil 20 nil <-| sl_ .plabel= a (∃I)
%D A4 A5 -> .plabel= a \piY
%D ))
%D (( B0 B1 |->
%D B0 B2 -> .plabel= l η???
%D B1 B3 -> .plabel= r \id
%D B2 B3 <-|
%D B0 B3 harrownodes nil 20 nil <-| sl_ .plabel= a (∃I)
%D B4 B5 -> .plabel= a \piY
%D ))
%D enddiagram
%D
%:
%: P(x,y)
%: -----------(∃I)
%: ∃x⠆X.P(x,y)
%:
%: ^H->L-(ExI)
%:
%:
$$\pu
\diag{H->L-(ExI)}
\qquad
\cded{H->L-(ExI)}
$$
%D diagram H->L-(ExI+)
%D 2Dx 100 +40 +30 +35 +45 +45
%D 2D 100 A0 A1 A2 C0 C1 C2
%D 2D
%D 2D +20 A3 A4 A5 C3 C4 C5
%D 2D
%D 2D +20 A6 C6
%D 2D
%D 2D +20 B0 B1 B2 D0 D1 D2
%D 2D
%D ren A0 A1 A2 ==> t^*φ φ Σ_\piYφ
%D ren A3 A4 A5 ==> π_t^*π_Y^*Σ_\piYφ π_Y^*Σ_\piYφ Σ_\piYφ
%D ren A6 ==> {π'_Y}^*Σ_\piYφ
%D ren B0 B1 B2 ==> Z×Y X×Y Y
%D
%D ren C0 C1 C2 ==> P(t'(z),y) P(x,y) ∃x⠆X.P(x,y)
%D ren C3 C4 C5 ==> ∃x⠆X.P(x,y) ∃x⠆X.P(x,y) ∃x⠆X.P(x,y)
%D ren C6 ==> ∃x⠆X.P(x,y)
%D ren D0 D1 D2 ==> Z×Y X×Y Y
%D
%D (( A0 A1 <-|
%D A1 A2 |->
%D A0 A3 ->
%D A1 A4 ->
%D A2 A5 -> .plabel= r \id
%D A0 A4 harrownodes nil 20 nil <-|
%D A1 A5 harrownodes nil 20 nil <-|
%D A3 A4 <-| A4 A5 <-|
%D A3 A6 <->
%D
%D B0 B1 -> .plabel= a t
%D B1 B2 -> .plabel= a π_Y
%D B0 B2 -> .slide= -10pt .plabel= b π'_Y
%D ))
%D (( C0 C1 <-|
%D C1 C2 |->
%D C0 C3 ->
%D C1 C4 ->
%D C2 C5 -> .plabel= r \id
%D C0 C4 harrownodes nil 20 nil <-|
%D C1 C5 harrownodes nil 20 nil <-|
%D C3 C4 <-| C4 C5 <-|
%D C3 C6 <->
%D
%D D0 D1 -> .plabel= a t
%D D1 D2 -> .plabel= a π_Y
%D D0 D2 -> .slide= -10pt .plabel= b π'_Y
%D ))
%D enddiagram
%D
%:
%: P(t'(z),y)
%: -----------(∃I)
%: ∃x⠆X.P(x,y)
%:
%: ^H->L-(ExI+)
%:
%:
$$\pu
\begin{array}{c}
\diag{H->L-(ExI+)}
\\ \\
\cded{H->L-(ExI+)}
\end{array}
$$
\newpage
% «page-523-equality» (to ".page-523-equality")
% (shyp 11 "page-523-equality")
% (shy "page-523-equality")
(P.523, equality rules):
\def\DX {{Δ_X}}
\def\DXs {{Δ_X^*}}
\def\SiDX{Σ_{Δ_X}}
\def\pis#1{π_#1^*}
% (find-seelyhyppage (+ -504 523) "The equality rules")
The equality rules follow as immediate consequences of our definition
of $E_X$ as $\SiDX⊤_X$: (R) asserts the existence of a morphism $⊤_X
\to \DXs\SiDX⊤_X$, which is the unit...
%D diagram page-523-R
%D 2Dx 100 +35 +30 +30
%D 2D 100 A0 A1 C0 C1
%D 2D
%D 2D +20 A2 A3 C2 C3
%D 2D
%D 2D +20 B0 B1 D0 D1
%D 2D
%D ren A0 A1 A2 A3 B0 B1 ==> ⊤_X \SiDX⊤_X \DXs\SiDX⊤_X \SiDX⊤_X X X×X
%D ren C0 C1 C2 C3 D0 D1 ==> ⊤ x{=}x' x{=}x x{=}x' X X×X
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l (R)
%D A1 A3 -> .plabel= r \id
%D A2 A3 <-|
%D A0 A3 harrownodes nil 20 nil <-|
%D B0 B1 -> .plabel= a Δ_X
%D ))
%D (( C0 C1 |->
%D C0 C2 -> .plabel= l (R)
%D C1 C3 -> .plabel= r \id
%D C2 C3 <-|
%D C0 C3 harrownodes nil 20 nil <-|
%D D0 D1 -> .plabel= a Δ_X
%D ))
%D enddiagram
%D
$$\pu
\diag{page-523-R}
$$
\newpage
% «page-523-eq-sub» (to ".page-523-eq-sub")
% (shyp 12 "page-523-eq-sub")
% (shy "page-523-eq-sub")
For (sub), note that we have a morphism:
%
$$\begin{array}{c}
π_2^*φ∧\SiDX⊤_X
\diagxyto/<->/<200>^{(\Frob)}
\SiDX(\DXs\pis2φ ∧ ⊤_X)
\diagxyto/<->/<200>
\SiDXφ
\diagxyto/<->/<200>
\SiDX\DXs\pis1φ
\diagxyto/->/<200>^{ε_{\pis1φ}}
\pis1φ
\\
P(x') ∧ x{=}x'
\diagxyto/<->/<200>^{(\Frob)}
x{=}x' ∧ (P(x)∧⊤)
\diagxyto/<->/<200>
x{=}x' ∧ P(x)
\diagxyto/<->/<200>
x{=}x' ∧ P(x)
\diagxyto/->/<200>^{ε_{\pis1φ}}
P(x)
\end{array}
$$
Let's see how to build its parts...
%D diagram frob-p.523
%D 2Dx 100 +60 +65
%D 2D 100 A0 A2
%D 2D
%D 2D +20 A3 A4 A5
%D 2D
%D 2D +20 A6 A8
%D 2D
%D 2D +15 B0 B1
%D 2D
%D ren A0 A2 ==> ⊤_X \SiDX⊤_X
%D ren A3 A4 A5 ==> \DXs\pis2φ∧⊤_X \SiDX(\DXs\pis2φ∧⊤_X) \pis2φ∧\SiDX⊤_X
%D ren A6 A8 ==> \DXs\pis2φ \pis2φ
%D ren B0 B1 ==> X X×X
%D
%D (( A0 A2 |->
%D A0 A3 <- A2 A4 <- A2 A5 <-
%D A3 A4 |-> A4 A5 <-> .plabel= a (\Frob)
%D A3 A6 -> A4 A8 -> A5 A8 ->
%D A6 A8 <-
%D B0 B1 -> .plabel= a Δ_X
%D
%D A0 A3 midpoint A2 A4 midpoint harrownodes nil 20 nil |->
%D A3 A6 midpoint A4 A8 midpoint harrownodes nil 20 nil |->
%D ))
%D enddiagram
%D
$$\pu
\diag{frob-p.523}
$$
%:
%: -----------
%: Δ_X;π_2=\id
%: ---------------
%: \DXs\pis2≅\id^* φ
%: ----------------------- -------------------
%: \DXs\pis2φ∧⊤↔\DXs\pis2φ \DXs\pis2φ↔φ
%: --------------------------------------
%: \DXs\pis2φ∧⊤↔φ
%: --------------------------
%: \SiDX(\DXs\pis2φ∧⊤)↔\SiDXφ
%:
%: ^p.523-tree-1
%:
%:
%: -----------
%: \id=Δ_X;π_1
%: ---------------
%: \id^*=\DXs\pis1 φ
%: -------------------
%: φ↔\DXs\pis1
%: ---------------------
%: \SiDXφ↔\SiDX\DXs\pis1
%:
%: ^p.523-tree-2
%:
%:
\pu
$$\ded{p.523-tree-1}
\quad
\ded{p.523-tree-2}
$$
%D diagram p.523-epsilon
%D 2Dx 100 +40 +30
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A3 A4 A5
%D 2D
%D 2D +15 B0 B1 B2
%D 2D
%D ren A0 A1 ==> \DXs\pis1φ \SiDX\DXs\pis1φ
%D ren A3 A4 A5 ==> \DXs\pis1φ \pis1φ φ
%D ren B0 B1 B2 ==> X X×X X
%D
%D (( A0 A1 |->
%D A0 A3 -> .plabel= l \id
%D A1 A4 -> .plabel= r ε_{\pis1φ}
%D A3 A4 <-| A4 A5 <-|
%D A0 A4 harrownodes nil 20 nil |->
%D B0 B1 -> .plabel= a Δ_X
%D B1 B2 -> .plabel= a π_1
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{p.523-epsilon}
$$
%
The actual form of (sub) can be easily derived from this.
% «thanks» (to ".thanks")
% Ana Luiza Tenorio
% Caio de Andrade Mendes
% Daniel Almeida
% Victor Nascimento
\newpage
\subsection*{Thanks}
...to (in alphabetical order): Ana Luiza Tenório, Caio Mendes, Daniel
Almeida and Victor Nascimento for lots of useful questions and
comments.
\printbibliography
\end{document}
% _____ _ _
% | ____| (_)___ _ __
% | _| | | / __| '_ \
% | |___| | \__ \ |_) |
% |_____|_|_|___/ .__/
% |_|
%
% «elisp» (to ".elisp")
% (find-angg ".emacs" "key-chord")
(key-chord-define-global ",." (eek-cmd "〈 〉 1*<left>"))
(key-chord-mode 1)
(key-chord-mode 0)
% __ __ _
% | \/ | __ _| | _____
% | |\/| |/ _` | |/ / _ \
% | | | | (_| | < __/
% |_| |_|\__,_|_|\_\___|
%
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2020seelyhyp veryclean
make -f 2019.mk STEM=2020seelyhyp pdf
% Local Variables:
% coding: utf-8-unix
% ee-tla: "shy"
% End: