|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2008hyp-utf8.tex")
% (find-LATEX "2008hyp.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2008hyp-utf8.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2008hyp-utf8.pdf"))
% (defun e () (interactive) (find-LATEX "2008hyp-utf8.tex"))
% (defun u () (interactive) (find-latex-upload-links "2008hyp-utf8"))
% (find-pdf-page "~/LATEX/2008hyp-utf8.pdf")
% (find-sh0 "cp -v ~/LATEX/2008hyp-utf8.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2008hyp-utf8.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2008hyp-utf8.pdf
% file:///tmp/2008hyp-utf8.pdf
% file:///tmp/pen/2008hyp-utf8.pdf
% http://angg.twu.net/LATEX/2008hyp-utf8.pdf
% (find-LATEX "2019.mk")
% «.haskell» (to "haskell")
% «.type-theory-origins» (to "type-theory-origins")
% «.eilenberg-maclane-1945» (to "eilenberg-maclane-1945")
% «.type-checking-and-related» (to "type-checking-and-related")
% «.weaker-systems» (to "weaker-systems")
% «.brownie-points» (to "brownie-points")
% «.subobjs-and-cob» (to "subobjs-and-cob")
% «.hyp-definition» (to "hyp-definition")
% «.quants-adjs-example» (to "quants-adjs-example")
% «.preservations-overview» (to "preservations-overview")
% «.pres-of-true-and-and» (to "pres-of-true-and-and")
% «.pres-of-false-and-or» (to "pres-of-false-and-or")
% «.pres-of-imp» (to "pres-of-imp")
% «.bcc-for-forall» (to "bcc-for-forall")
% «.bcc-for-exists» (to "bcc-for-exists")
% «.bcc-for-equality» (to "bcc-for-equality")
% «.frob-for-exists» (to "frob-for-exists")
% «.frob-for-equality» (to "frob-for-equality")
% «.frob-for-ex-eq» (to "frob-for-ex-eq")
% «.frob-and-pres-imp» (to "frob-and-pres-imp")
% «.bcc-ex-iff-bcc-fa» (to "bcc-ex-iff-bcc-fa")
% «.constrs-to-proofs-and-back» (to "constrs-to-proofs-and-back")
% «.adj-functors-as-seq-rules» (to "adj-functors-as-seq-rules")
% «.adj-functors-as-seq-rules-2» (to "adj-functors-as-seq-rules-2")
% «.adj-maps-as-seq-rules» (to "adj-maps-as-seq-rules")
% «.adj-maps-as-seq-rules-2» (to "adj-maps-as-seq-rules-2")
% «.adj-functors-as-ND-proofs» (to "adj-functors-as-ND-proofs")
% «.adj-functors-as-ND-proofs-2» (to "adj-functors-as-ND-proofs-2")
% «.adj-maps-as-ND-proofs» (to "adj-maps-as-ND-proofs")
% «.adj-maps-as-ND-proofs-2» (to "adj-maps-as-ND-proofs-2")
% «.adj-maps-as-ND-proofs-3» (to "adj-maps-as-ND-proofs-3")
% «.frob-maps-as-ND-proofs» (to "frob-maps-as-ND-proofs")
% «.frob-for-equality-2» (to "frob-for-equality-2")
% «.dep-eq-from-simple-eq» (to "dep-eq-from-simple-eq")
% «.eq-is-transitive» (to "eq-is-transitive")
% «.hyp-subst-quant-refl» (to "hyp-subst-quant-refl")
% «.hyp-sym-trans» (to "hyp-sym-trans")
% «.weak-strong-exelim» (to "weak-strong-exelim")
% «.rules-nd-sc» (to "rules-nd-sc")
% «.rules-categorically» (to "rules-categorically")
\documentclass[oneside]{book}
\usepackage[colorlinks,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{colorweb} % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (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{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")
%
% (find-es "tex" "geometry")
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
%\catcode`*=13 \def*{\ensuremath{\bullet}}
\catcode`\^^O=13 \def*{\ensuremath{\bullet}}
% (find-dn4 "experimental.lua" "relplace" "_|")
% (find-dednat6 "dednat6/diagforth.lua" "relplace")
% (find-dednat6 "dednat6/diagforth.lua" "diag-head")
% (find-dednat6 "dednat6/diagforth.lua" "diag-head" "dxyrun =")
% (find-dn4file "dednat4.lua" "dofs =")
% (find-dn4file "dednat4.lua" "macro =")
%L dxyrun = function (str, pos)
%L local oldsubj, oldpos = subj, pos
%L setsubj(str, pos or 1)
%L while getword() do
%L -- PP(word)
%L if forths[word] then forths[word]()
%L elseif nodes[word] then ds:push(nodes[word])
%L else Error("Unknown word: "..word)
%L end
%L end
%L subj, pos = oldsubj, oldpos
%L end
%L macro = function (str) return function () dxyrun(str) end end
%L forths["_|"] = macro "relplace 7 7 \\pbsymbol{7}"
% (find-dednat6 "dednat6/block.lua" "TexLines")
\directlua{tf:processuntil(texlines:nlines())}
% %L dofile "edrxtikz.lua" -- (find-LATEX "edrxtikz.lua")
% %L dofile "edrxpict.lua" -- (find-LATEX "edrxpict.lua")
% \pu
% «.haskell» (to "haskell")
% «.type-theory-origins» (to "type-theory-origins")
% «.eilenberg-maclane-1945» (to "eilenberg-maclane-1945")
% «.type-checking-and-related» (to "type-checking-and-related")
% «.weaker-systems» (to "weaker-systems")
% «.brownie-points» (to "brownie-points")
% «.subobjs-and-cob» (to "subobjs-and-cob")
% «.hyp-definition» (to "hyp-definition")
% «.quants-adjs-example» (to "quants-adjs-example")
% «.preservations-overview» (to "preservations-overview")
% «.pres-of-true-and-and» (to "pres-of-true-and-and")
% «.pres-of-false-and-or» (to "pres-of-false-and-or")
% «.pres-of-imp» (to "pres-of-imp")
% «.bcc-for-forall» (to "bcc-for-forall")
% «.bcc-for-exists» (to "bcc-for-exists")
% «.bcc-for-equality» (to "bcc-for-equality")
% «.frob-for-exists» (to "frob-for-exists")
% «.frob-for-equality» (to "frob-for-equality")
% «.frob-for-ex-eq» (to "frob-for-ex-eq")
% «.frob-and-pres-imp» (to "frob-and-pres-imp")
% «.bcc-ex-iff-bcc-fa» (to "bcc-ex-iff-bcc-fa")
% «.constrs-to-proofs-and-back» (to "constrs-to-proofs-and-back")
% «.adj-functors-as-seq-rules» (to "adj-functors-as-seq-rules")
% «.adj-functors-as-seq-rules-2» (to "adj-functors-as-seq-rules-2")
% «.adj-maps-as-seq-rules» (to "adj-maps-as-seq-rules")
% «.adj-maps-as-seq-rules-2» (to "adj-maps-as-seq-rules-2")
% «.adj-functors-as-ND-proofs» (to "adj-functors-as-ND-proofs")
% «.adj-functors-as-ND-proofs-2» (to "adj-functors-as-ND-proofs-2")
% «.adj-maps-as-ND-proofs» (to "adj-maps-as-ND-proofs")
% «.adj-maps-as-ND-proofs-2» (to "adj-maps-as-ND-proofs-2")
% «.adj-maps-as-ND-proofs-3» (to "adj-maps-as-ND-proofs-3")
% «.frob-maps-as-ND-proofs» (to "frob-maps-as-ND-proofs")
% «.frob-for-equality-2» (to "frob-for-equality-2")
% «.dep-eq-from-simple-eq» (to "dep-eq-from-simple-eq")
% «.eq-is-transitive» (to "eq-is-transitive")
% «.hyp-subst-quant-refl» (to "hyp-subst-quant-refl")
% «.hyp-sym-trans» (to "hyp-sym-trans")
% «.weak-strong-exelim» (to "weak-strong-exelim")
% «.rules-nd-sc» (to "rules-nd-sc")
% «.rules-categorically» (to "rules-categorically")
% (eedn4-51-bounded)
% (find-2005oct20seminar "" "PLC-diags-sqth1")
% (find-angg "LATEX/2005oct20-seminar.tex" "PLC-diags-sqth1")
Index of the slides:
\msk
% To update the list of slides uncomment this line:
\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")
\tocline {Haskell} {2}
\tocline {Type theory: origins} {3}
\tocline {Eilenbeg/MacLane 1945} {4}
\tocline {Type-checking and related problems} {5}
\tocline {Weaker systems} {6}
\tocline {Slides vs. brownie points} {7}
\tocline {Hyperdoctrines: subobjects and change-of-base} {8}
\tocline {Hyperdoctrine: definition} {9}
\tocline {Quantifiers as adjoints: an example} {10}
\tocline {Preservations by change-of-base: overview} {11}
\tocline {Preservation of `true' and `and'} {12}
\tocline {Preservation of `false' and `or'} {13}
\tocline {Preservation of `implies'} {14}
\tocline {BCC for `forall'} {15}
\tocline {BCC for `exists'} {16}
\tocline {BCC for equality} {17}
\tocline {Frobenius for `exists'} {18}
\tocline {Frobenius for equality} {19}
\tocline {Frobenius for exists-equal} {20}
\tocline {Frobenius is equivalent to preservation of `implies'} {21}
\tocline {BCC for `exists' holds iff BCC for `forall' holds} {22}
\tocline {From ``constructions'' to ``intuitionistic proofs'', and back} {23}
\tocline {The adjunction functors as sequent rules} {24}
\tocline {The adjunction functors as sequent rules (2)} {25}
\tocline {The adjunction maps as sequent rules} {26}
\tocline {The adjunction maps as sequent rules (2)} {27}
\tocline {The adjunction functors as ND proofs} {28}
\tocline {The adjunction functors as ND proofs (2)} {29}
\tocline {The adjunction maps as ND proofs} {30}
\tocline {The adjunction maps as ND proofs (2)} {31}
\tocline {The adjunction maps as ND proofs (3)} {32}
\tocline {The Frobenius maps as ND proofs} {33}
\tocline {Frobenius for equality (2)} {34}
\tocline {Dependent equality from simple equality} {35}
\tocline {Transitivity of equality} {36}
\tocline {Hyperdoctrines: substitution, quantifiers, reflexivity} {37}
\tocline {Hyperdoctrines: symmetry, transitivity} {38}
\tocline {Weak and strong exists-elim} {39}
\tocline {Rules in ND and sequent calculus} {40}
\tocline {Rules, categorically} {41}
%:*&*\&*
%:*\&*\&*
%:*'**^{\prime*}*
%:*b=b'*b{=}b'*
%:*b=b''*b{=}b''*
%:*b'=b''*b'{=}b''*
%:*a=fb*a{=}fb*
%:*b=fa*b{=}fa*
%:*×*{×}*
%:*\s[*\dncdisplay[*
%:*`*\ign *
\def\ign#1{}
\def\Eq{𝐬{Eq}}
\def\ExEq{∃{=}}
\def\co{\mathrm{co}}
\def\dncdisplay[#1|#2]{\begin{pmatrix} #2 \\ #1 \end{pmatrix}}
\def\lcurlybar#1{\left\{\mskip#1mu\middle|}
\def\rcurlybar#1{\middle|\mskip#1mu\right\}}
\def\scof#1#2{\lcurlybar{#1}#2\rcurlybar{#1}}
\def\scst#1#2#3{\lcurlybar{#1}#2\middle\|#3\rcurlybar{#1}}
\def\Sst#1#2{\scst{-4}{#1}{#2}}
\def\footwo#1#2{%
\begin{array}{ccc}
#1 && #2 \\
\end{array}
}
\def\footwov#1#2{%
\begin{array}{ccc}
#1 \\ \\ #2 \\
\end{array}
}
\def\foothreev#1#2#3{%
\begin{array}{ccc}
#1 \\ \\ #2 \\ \\ #3 \\
\end{array}
}
\def\foofour#1#2#3#4{%
\begin{array}{ccc}
#1 & #2 \\ \\
#3 & #4 \\
\end{array}
}
\def\fooFour#1#2#3#4{%
\begin{array}{ccc}
#1 && #2 \\ \\
#3 && #4 \\
\end{array}
}
\def\lcurlybar#1{\left\{\mskip#1mu\middle|}
\def\rcurlybar#1{\middle|\mskip#1mu\right\}}
\def\cbsof#1{\lcurlybar{-4}#1\rcurlybar{-4}}
\def\cbsst#1#2{\lcurlybar{-4}#1\,\middle|\,#2\rcurlybar{-4}}
\def\cbsubobj#1#2{\lcurlybar{-4}#1\,\middle\|\,#2\rcurlybar{-4}}
\newpage
% --------------------
% «haskell» (to ".haskell")
% (s "Haskell" "haskell")
\myslide {Haskell} {haskell}
{%\myttchars
% \footnotesize
\begin{verbatim}
-- (find-libhugsfile "libraries/Hugs/Prelude.hs")
foldl :: (a -> b -> a) -> a -> [b] -> a
foldl f z [] = z
foldl f z (x:xs) = foldl f (f z x) xs
foldl1 :: (a -> a -> a) -> [a] -> a
foldl1 f (x:xs) = foldl f x xs
-- foldl1 max [1, 3, 2, 4]
---> foldl max 1 [3, 2, 4]
---> foldl max (max 1 3) [2, 4]
---> foldl max (max (max 1 3) 2) [4]
---> foldl max (max (max (max 1 3) 2) 4) []
---> (max (max (max 1 3) 2) 4)
---> (max (max 3 2) 4)
---> (max 3 4)
---> 4
\end{verbatim}
}
\newpage
% --------------------
% «type-theory-origins» (to ".type-theory-origins")
% (s "Type theory: origins" "type-theory-origins")
\myslide {Type theory: origins} {type-theory-origins}
% (find-automathpage (+ 21 4) "In order to prevent the paradoxes")
(From the introduction to {\sl 25 Years of Automath}:)
\begin{quote}
In order to prevent the paradoxes, Whitehead and Russell analysed the
{\sl vicious circles} present in all the known paradoxes. They came to
the conviction that a hierarchy was necessary for a sound development
of arithmetic and they proposed a type system: the {\sl simple type
theory}. It turned out that a refinement was necessary, which they
called the {\sl ramified theory of types}. This worked as they
desired, albeit they needed an extra axiom, in order to ``soften'' the
strictness of the typing hierarchy. Only with this {\sl axiom of
reducibility} they were able to incorporate full arithmetic, in
particular the real numbers, based on Dedekind cuts.
This idea of using types emerged quite naturally, once the vicious
circles had been detected. In fact, one may say that types existed
since early mathematics was developed: categories like `natural
number' and `real number' in calculus, or `point' and `line' in
geometry, grouped elements together in clusters with a common meaning
or structure. In this sense, types were meant to emphasize the {\sl
similarities} between given entities. But at the same time, types can
be of use in establishing {\sl differences} between entities. The
latter aspects turned out to be of great importance in combatting
against the paradoxes.
\end{quote}
\newpage
% --------------------
% «eilenberg-maclane-1945» (to ".eilenberg-maclane-1945")
% (s "Eilenbeg/MacLane 1945" "eilenberg-maclane-1945")
\myslide {Eilenbeg/MacLane 1945} {eilenberg-maclane-1945}
From Ralf Krömer's {\sl Tool and Object - A History and
Philosophy of Category Theory} (p.65) on the reception of the
first paper on Category Theory (Eilenberg/MacLane: ``General
Theory of Natural Equivalences'', 1945):
% (find-em45page (+ -229 231) "Contents")
% (find-kromerpage (+ 34 65) "2.3.2. The reception of the 1945 paper")
% (find-kromertext "\n2.3.2 The reception of the 1945 paper")
\begin{quote}
The readyness to write down and submit for publication a work almost
completely concerned with conceptual clarification (and with the
solution of some internal problems raised by the new concepts
themselves) is a remarkable expression of courage. While (as Corry
learned from Eilenberg, see [Corry 1996, 366 n.27]) Steenrod once
stated concerning [1945] that ``no paper had ever influenced his
thinking more'', P.A.\ Smith said that ``he had never read a more
trivial paper in his life''. [Mac Lane 1988a, 334] writes, without
mentioning a name: ``One of our good friends (an admirer of
Eilenberg) read the paper and told us privately that he thought that
the paper was without any content''.
\end{quote}
% (find-kromertext "The diagrams incorporate a large amount of information")
Krömer, p.82, quoting Eilenberg/Steenrod 1952:
\begin{quote}
The reader will observe the presence of numerous diagrams in the
text. [...] Two paths connecting the same pair of vertices usually
give the same homomorphism. This is called a {\sl commutativity
relation}. The combinatorially minded individual can regard it as
a homology relation due to the presence of 2-dimensional cells
adjoined to the graph. [...]
The diagrams incorporate a large amount of information. [...] In the
case of many theorems, the setting up of the correct diagram is the
major part of the proof [1952, xi].
\end{quote}
\newpage
% --------------------
% «type-checking-and-related» (to ".type-checking-and-related")
% (s "Type-checking and related problems" "type-checking-and-related")
\myslide {Type-checking and related problems} {type-checking-and-related}
% (find-angg ".emacs.papers" "urzyczyn")
% (find-urzypage (+ 12 89) "6. Type-checking and related problems")
% (find-urzytext "The type checking problem is")
From Urzyczyn/Sorensen's ``Lectures on the Curry-Howard Isomorphism''
(online draft, p.89):
\begin{quote}
1. The type checking problem is to decide whether $\GG \vdash M:τ$
holds, for a given context $\GG$, a term $M$ and a type $τ$.
2. The type reconstruction problem, also called typability problem,
is to decide, for a given term $M$, whether there exist a context
$\GG$ and a type $τ$, such that $\GG \vdash M:τ$ holds, i.e.,
whether $M$ is typable.
3. The type inhabitation problem, also called type emptiness
problem, is to decide, for a given type $τ$, whether there exists a
closed term $M$, such that $\GG \vdash M:τ$ holds. (Then we say that
$τ$ is non-empty and has an inhabitant $M$).
\end{quote}
\newpage
% --------------------
% «weaker-systems» (to ".weaker-systems")
% (s "Weaker systems" "weaker-systems")
\myslide {Weaker systems} {weaker-systems}
Why do we want weaker systems?
Things that can be constructed in them may have nicer properties:
Every reduction sequence terminates.
All terms of type $A×B \to B×A$ are the flip function
Each proof in Natural Deduction corresponds to a lambda-term
Every term is typed
Type-checking can be used to detect errors
\msk
Weaker systems should have more models:
If a judgment $J$
is true in a stronger system $S$
but false in a weaker system $W$
then there should be a model of $W$
in which $J$ is not collapsed to ``true''.
\msk
How do we get intuition about weaker systems?
Stronger system: $S$, the universe of ZFC
Weaker system: $W$, where $¬¬P = P$ is not ``true''
All constructions in $W$ can be carried out in $S$.
% \end{document}
\newpage
% --------------------
% «brownie-points» (to ".brownie-points")
% (s "Slides vs. brownie points" "brownie-points")
\myslide {Slides vs. brownie points} {brownie-points}
% This technical report has an unusual format -- slides --
% an unsual aims. Let me explain. First of all, I am in a kind of
% a professional limbo: from 2005 to 2007 I worked as a programmer,
% but at the end of that I was on the verge of killing people and
% then blowing myself up -- because ``someone had to do that'' and
% because ``I had absolutely nothing to lose'' -- but then I
% applied to an academic position, went through all the admission
% process, and was selected for the job; I became an {\sl almost-
% professor} in a federal university in Brazil...
% ...then it turned out that one of the other candidates --
% who was applying to a position {\sl in another department} (!) --
% had found some slight legal inconsistencies in the official public
% anouncement of these job openings and of the rules of the selection
% process, and had denounced that, and demanded certain changes in
% the rules...
%
% To make a long story short: there are 12 almost-professors,
% including me, waiting since june for the legal mumbo-jumbo to be
% completed so that we can be hired -- I am writing this in november.
% The process is taking longer than anyone expected, and
% as {\sl I have not gotten rid of my anger yet} -- far from that --
% I decided that I would not follow the ``path of the articles'',
% that would give me more CV-karma and more brownie points.
I have not been hired by UFF yet.
This is going to happen ``at any moment'' -- since june.
http://angg.twu.net/concurso.html
I am (choose one):
• almost a university professor
• currently unemployed
• in unpayed holidays
• on strike
\msk
Articles would get me more brownie points from funding agencies,
but right now seminars and slides are more useful --
\msk
I need to discuss with local people, who are:
• algebraic geometers,
• (modal) logicians,
• computer scientists
• grad students who just had a CT course (that was ``too algebraic'')
\newpage
% --------------------
% «subobjs-and-cob» (to ".subobjs-and-cob")
% (s "Hyperdoctrines: subobjects and change-of-base" "subobjs-and-cob")
\myslide {Hyperdoctrines: subobjects and change-of-base} {subobjs-and-cob}
Our archetypal hyperdoctrine is this:
$\begin{array}{rrcl}
\Cod: & \Sub(\Set) & \to & \Set \\
& (A' \monicto A) & \mto & A \\
\end{array}
$
\msk
A linguistic trick:
everything will simplify A LOT if we pretend
that all subobject are subsets.
Another shorthand: `$P$' instead of `$P(a)$'.
$\begin{array}{rcl}
(\cbsst{a}{P} \monicto A) & \mto & A \\
(\cbsst{a}{P} \monicto \cbsof{a}) & \mto & \cbsof{a} \\
\cbsubobj{a}{P} & \mto & \cbsof{a} \\
(a\|P) & \funto & a \\
\end{array}
$
\msk
We will downcase the projection functor, $\Cod$, to $(a\|P) \funto a$.
We will often draw it vertically and omit the `$a\|$' and the `$\funto$':
%D diagram cod-omits
%D 2Dx 100 +30 +30 +29
%D 2D 100 A0 A1 A2 A3
%D 2D
%D 2D +20 B0 B1 B2 B3
%D 2D
%D (( A0 .tex= \cbsubobj{a}{P} B0 .tex= A |->
%D A1 .tex= a\|P B1 .tex= a =>
%D A2 .tex= P B2 .tex= a =>
%D A3 .tex= P place B3 .tex= a place
%D ))
%D enddiagram
%D
$$\diag{cod-omits}$$
\msk
The change-of-base functors in $\Cod: \Sub(\Set) \to \Set$
are induced by pullbacks:
%D diagram cob-as-PB-in-sub-set
%D 2Dx 100 +45 +30 +40
%D 2D 100 A0 -> A1 B0 -> B1
%D 2D v _| v v _| v
%D 2D +15 | | B02 B13
%D 2D v v v v
%D 2D +15 A2 -> A3 B2 -> B3
%D 2D
%D 2D +15 A4 -> A5 B4 -> B5
%D 2D
%D (( A0 .tex= \cbsst{a}{P(f(a))} A1 .tex= \cbsst{a}{P(b)}
%D A2 .tex= A A3 .tex= B
%D A4 .tex= A A5 .tex= B
%D A0 A1 -> .plabel= a f'
%D A0 A2 >-> .plabel= l f^*P
%D A1 A3 >-> .plabel= r P
%D A2 A3 -> .plabel= a f
%D A0 relplace 7 7 \pbsymbol{7}
%D A0 A3 harrownodes nil 20 nil <-| .plabel= a f^*
%D A4 A5 -> .plabel= a f
%D ))
%D (( B02 .tex= f^*P B13 .tex= P
%D B4 .tex= A B5 .tex= B
%D B02 B13 -> sl^ .plabel= a \ov{f}P\equiv(f',f)
%D B02 B13 <-| sl_ .plabel= b f^*
%D B02 B4 |-> .plabel= l \Cod
%D B13 B5 |-> .plabel= r \Cod
%D B4 B5 -> .plabel= a f
%D ))
%D enddiagram
%D
$$\diag{cob-as-PB-in-sub-set}$$
\msk
The map $\ov{f}P: \cbsubobj{a}{P(f(a))} \to \cbsubobj{b}{P(b)}$
corresponds to a pullback square in $\Sub(\Set)$.
It is a {\sl cartesian map} in the fibration $\Cod: \Sub(\Set) \to \Set$.
(We will see the abstract definition of cartesian maps later).
We will indicate cartesian maps with a `$◻$'.
We will downcase the change-of-base diagram as this:
%D diagram cob-in-set-dnc
%D 2Dx 100 +35 +25 +30
%D 2D 100 Pfa <=== Pb B0 <=== B1
%D 2D
%D 2D +25 a |----> b B2 |--> B3
%D 2D
%D (( Pfa Pb a b
%D @ 0 @ 1 |-> sl^ .plabel= a ◻ @ 0 @ 1 <= sl_
%D a b |-> .plabel= a f
%D ))
%D (( B0 .tex= P B1 .tex= P
%D B2 .tex= a B3 .tex= b
%D @ 0 @ 1 |-> sl^ .plabel= a ◻ @ 0 @ 1 <= sl_
%D @ 2 @ 3 |->
%D ))
%D enddiagram
%D
$$\diag{cob-in-set-dnc}$$
\newpage
% --------------------
% «hyp-definition» (to ".hyp-definition")
% (s "Hyperdoctrine: definition" "hyp-definition")
\myslide {Hyperdoctrine: definition} {hyp-definition}
Formally, a hyperdoctrine is a fibration for which:
(i) the base category is cartesian closed,
(ii) each fiber is bicartesian closed,
(iii) the change-of-base functors preserve the BiCCC structure modulo iso,
(iv) each change-of-base functor has a left adjoint
\quad obeying Beck-Chevalley and Frobenius,
(v) each change-of-base functor has a right adjoint
\quad obeying Beck-Chevalley and Frobenius.
\msk
The base category is (bi)cartesian closed:
%D diagram CCC
%D 2Dx 100 +25 +25 +15 +20 +25
%D 2D 100 --| p0 |- t0 a0 <==== a1
%D 2D / - \ - - -
%D 2D / | \ | | <--> |
%D 2D v v v v v v
%D 2D +25 p1 <--| p2 |--> p3 t1 a2 ====> a3
%D 2D
%D 2D +15 c0 |--> c1 <--| c2 i0
%D 2D / - \ -
%D 2D \ | / |
%D 2D \ v / v
%D 2D +25 --> c3 <- i1
%D 2D
%D (( p0 .tex= a
%D p1 .tex= b p2 .tex= b,c p3 .tex= c
%D @ 0 @ 1 |-> @ 0 @ 2 |-> @ 0 @ 3 |->
%D @ 1 @ 2 <-| @ 2 @ 3 |->
%D ))
%D (( c0 .tex= a c1 .tex= a⊔b c2 .tex= b
%D c3 .tex= c
%D @ 0 @ 1 |-> @ 1 @ 2 <-|
%D @ 0 @ 3 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D ))
%D (( t0 .tex= a t1 .tex= *
%D @ 0 @ 1 |->
%D ))
%D (( i0 .tex= ⊥ i1 .tex= a
%D @ 0 @ 1 |->
%D ))
%D (( a0 .tex= a,b a1 .tex= a
%D a2 .tex= c a3 .tex= b|->c
%D @ 0 @ 1 <= @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram
$$\diag{CCC}$$
\msk
Each fiber is bicartesian closed:
%D diagram HA
%D 2Dx 100 +25 +25 +15 +20 +25
%D 2D 100 --| p0 |- t0 a0 <==== a1
%D 2D / - \ - - -
%D 2D / | \ | | <--> |
%D 2D v v v v v v
%D 2D +25 p1 <--| p2 |--> p3 t1 a2 ====> a3
%D 2D
%D 2D +15 c0 |--> c1 <--| c2 i0
%D 2D / - \ -
%D 2D \ | / |
%D 2D \ v / v
%D 2D +25 --> c3 <- i1
%D 2D
%D (( p0 .tex= P
%D p1 .tex= Q p2 .tex= Q&R p3 .tex= R
%D @ 0 @ 1 |-> @ 0 @ 2 |-> @ 0 @ 3 |->
%D @ 1 @ 2 <-| @ 2 @ 3 |->
%D ))
%D (( c0 .tex= P c1 .tex= P∨Q c2 .tex= Q
%D c3 .tex= R
%D @ 0 @ 1 |-> @ 1 @ 2 <-|
%D @ 0 @ 3 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D ))
%D (( t0 .tex= P t1 .tex= {⊤}
%D @ 0 @ 1 |->
%D ))
%D (( i0 .tex= ⊥ i1 .tex= P
%D @ 0 @ 1 |->
%D ))
%D (( a0 .tex= P&Q a1 .tex= P
%D a2 .tex= R a3 .tex= Q→R
%D @ 0 @ 1 <= @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram
$$\diag{HA}$$
\msk
Left adjoints ($∃/\&{=}/∃{=}$) and right adjoints ($∀/→{=}/∀{=}$)
for change-of-base functors:
%D diagram adjs-to-change-of-base
%D 2Dx 100 +30 +30 +35 +30 +40
%D 2D 100 A0 ===> A1 B0 ===> B1 C0 ===> C1
%D 2D - - - - - -
%D 2D | <-> | | <-> | | <-> |
%D 2D v v v v v v
%D 2D +20 A2 <=== A3 B2 <=== B3 C2 <=== C3
%D 2D - - - - - -
%D 2D | <-> | | <-> | | <-> |
%D 2D v v v v v v
%D 2D +20 A4 ===> A5 B4 ===> B5 C4 ===> C5
%D 2D
%D 2D +20 a0 |--> a1 b0 |--> b1 c0 |--> c1
%D 2D
%D (( A0 .tex= Pab A1 .tex= ∃b.Pab
%D A2 .tex= Qa A3 .tex= Qa
%D A4 .tex= Rab A5 .tex= ∀b.Rab
%D a0 .tex= a,b a1 .tex= a
%D A0 A1 =>
%D A0 A2 |-> A1 A3 |-> A0 A3 harrownodes nil 20 nil <->
%D A2 A3 <=
%D A2 A4 |-> A3 A5 |-> A2 A5 harrownodes nil 20 nil <->
%D A4 A5 =>
%D a0 a1 |->
%D ))
%D (( B0 .tex= Pab B1 .tex= b=b'&Pabb
%D B2 .tex= Qabb B3 .tex= Qabb'
%D B4 .tex= Rab B5 .tex= b=b'→Rab
%D b0 .tex= a,b b1 .tex= a,b,b'
%D B0 B1 =>
%D B0 B2 |-> B1 B3 |-> B0 B3 harrownodes nil 20 nil <->
%D B2 B3 <=
%D B2 B4 |-> B3 B5 |-> B2 B5 harrownodes nil 20 nil <->
%D B4 B5 =>
%D b0 b1 |->
%D ))
%D (( C0 .tex= Pa C1 .tex= ∃a.b=fa&Pb
%D C2 .tex= Qfa C3 .tex= Qb
%D C4 .tex= Ra C5 .tex= ∀a.b=fa→Pb
%D c0 .tex= a c1 .tex= b
%D C0 C1 =>
%D C0 C2 |-> C1 C3 |-> C0 C3 harrownodes nil 20 nil <->
%D C2 C3 <=
%D C2 C4 |-> C3 C5 |-> C2 C5 harrownodes nil 20 nil <->
%D C4 C5 =>
%D c0 c1 |-> .plabel= a f
%D ))
%D enddiagram
%D
$$\diag{adjs-to-change-of-base}$$
% \end{document}
\newpage
% --------------------
% «quants-adjs-example» (to ".quants-adjs-example")
% (s "Quantifiers as adjoints: an example" "quants-adjs-example")
\myslide {Quantifiers as adjoints: an example} {quants-adjs-example}
%D diagram quants-set
%D 2Dx 100 +55 +40 +35
%D 2D 100 A0 ====> A1 B0 ====> B1
%D 2D - - - -
%D 2D | <-> | | <-> |
%D 2D v v v v
%D 2D +30 A2 <===== A3 B2 <===== B3
%D 2D - - - -
%D 2D | <-> | | <-> |
%D 2D v v v v
%D 2D +30 A4 =====> A5 B4 =====> B5
%D 2D
%D 2D +15 A6 |----> A7 B6 |----> B7
%D 2D
%D (( A0 .tex= \Sst{a,b}{P(a,b)} A1 .tex= \Sst{a}{∃b.P(a,b)}
%D A2 .tex= \Sst{a,b}{Q(a)} A3 .tex= \Sst{a}{Q(a)}
%D A4 .tex= \Sst{a,b}{R(a,b)} A5 .tex= \Sst{a}{∀b.R(a,b)}
%D A6 .tex= A×B A7 .tex= A
%D @ 0 @ 1 |->
%D @ 0 @ 2 -> @ 1 @ 3 ->
%D @ 2 @ 3 <-|
%D @ 2 @ 4 -> @ 3 @ 5 ->
%D @ 4 @ 5 |->
%D @ 0 @ 3 harrownodes nil 20 nil <->
%D @ 2 @ 5 harrownodes nil 20 nil <->
%D @ 6 @ 7 ->
%D ))
%D (( B0 .tex= \sm{100\,000\\110\,000} B1 .tex= \sm{110\,000}
%D B2 .tex= \sm{111\,000\\111\,000} B3 .tex= \sm{111\,000}
%D B4 .tex= \sm{111\,100\\111\,110} B5 .tex= \sm{111\,100}
%D B6 .tex= A×B B7 .tex= A
%D @ 0 @ 1 |->
%D @ 0 @ 2 -> @ 1 @ 3 ->
%D @ 2 @ 3 <-|
%D @ 2 @ 4 -> @ 3 @ 5 ->
%D @ 4 @ 5 |->
%D @ 0 @ 3 harrownodes nil 20 nil <->
%D @ 2 @ 5 harrownodes nil 20 nil <->
%D @ 6 @ 7 ->
%D ))
%D enddiagram
\def\sm#1{\begin{smallmatrix}#1\end{smallmatrix}}
`$∃$' and `$∀$' are left and right adjoint to
change-of-base along a projection $A×B \to A$...
That this is true is far from obvious,
so let's look at an example. If
$A \equiv \sm{***\,***}$ and
$B \equiv \sm{*\\*}$, then
$A×B \equiv \sm{***\,***\\***\,***}$;
using the obvious positional notation with 0s and 1s
to denote subsets of $A×B$ and $A$,
and for the right $P(a,b)$, $Q(a)$, $R(a,b)$, we have:
\msk
$\diag{quants-set}$
\bsk
\msk
Later we will see that `$∃ \dashv π^* \dashv ∀$' holds
even when the logic is just intuitionistic ---
and we will use this to ``define'' $∃$ and $∀$ in hyperdoctrines...
\msk
Also, we will see in which sense
``hyperdoctrines are models of typed intuitionistic logic'',
and we will construct some hyperdoctrines in which the logic
is not classical.
\newpage
% --------------------
% «preservations-overview» (to ".preservations-overview")
% (s "Preservations by change-of-base: overview" "preservations-overview")
\myslide {Preservations by change-of-base: overview} {preservations-overview}
Start with $f: A \to B$,
and $\cbsubobj{b}{P(b)}$ and $\cbsubobj{b}{Q(b)}$.
\msk
There are two different categorical ways to build
an object that ``deserves the name''
$\cbsubobj{a}{P(f(a))\&Q(f(a))}$.
\msk
We want these two ways to be isomorphic,
and there is a natural way to build
one of the directions of the iso ---
so the technical condition
``change-of-base functors preserve the BiCCC structure''
becomes, for each of the connectives $⊤, ⊥, \&, ∨, →$,
that this natural half-side of the iso
will have an inverse.
\msk
More precisely:
%D diagram preservations-overview
%D 2Dx 100 +30 +40
%D 2D 100 T0 I0 IMP0
%D 2D
%D 2D
%D 2D +30 T1 I1 IMP1
%D 2D
%D 2D +20 A0 <==========> A1
%D 2D
%D 2D +20 O0 <==========> O1
%D 2D
%D (( T0 .tex= f^*⊤_B T1 .tex= ⊤_A
%D T0 T1 -> sl_ .plabel= l ♮=!
%D T0 T1 <- sl^ .plabel= r 𝐬P⊤
%D ))
%D (( I0 .tex= ⊥_A I1 .tex= f^*⊥_B
%D I0 I1 -> sl_ .plabel= l ♮=!
%D I0 I1 <- sl^ .plabel= r 𝐬P⊥
%D ))
%D (( A0 .tex= f^*P&f^*Q A1 .tex= f^*(P&Q)
%D A0 A1 <- sl^ .plabel= a ♮=\ang{f^*π,f^*π'}
%D A0 A1 -> sl_ .plabel= b 𝐬P\&
%D ))
%D (( O0 .tex= f^*P∨f^*Q O1 .tex= f^*(P∨Q)
%D O0 O1 -> sl^ .plabel= a ♮=[f^*\iota,f^*\iota']
%D O0 O1 <- sl_ .plabel= b 𝐬P∨
%D ))
%D (( IMP0 .tex= f^*(P→Q) IMP1 .tex= f^*P→f^*Q
%D IMP0 IMP1 -> sl_ .plabel= l ♮=...
%D IMP0 IMP1 <- sl^ .plabel= r 𝐬P→
%D ))
%D enddiagram
\msk
$\diag{preservations-overview}$
\msk
We will see the diagrams for these constructions in the next slides.
The natural half for `$→$', in particular, is a big construction.
\msk
The Beck-Chevalley conditions are similar: they say that the two
natural constructions for two objects that ``deserve the same name''
are isomorphic --- the natural half-side of an iso has an inverse.
\msk
Frobenius conditions are more like distributivities.
The case where they are more natural will appear later,
in another hyperdoctrine, where the same structure will
interpret different operations. There it will be this:
\msk
%D diagram frobenius-overview
%D 2Dx 100 +50
%D 2D 100 b,(c,d) (b,c),d
%D 2D
%D (( b,(c,d) (b,c),d |-> sl^ .plabel= a ♮
%D b,(c,d) (b,c),d <-| sl_ .plabel= b 𝐬{Frob}
%D ))
%D enddiagram
$\diag{frobenius-overview}$
\newpage
% --------------------
% «pres-of-true-and-and» (to ".pres-of-true-and-and")
% (s "Preservation of `true' and `and'" "pres-of-true-and-and")
\myslide {Preservation of `true' and `and'} {pres-of-true-and-and}
% (find-LATEX "2008hyp.tex" "first-preservations")
% (find-dn4 "experimental.lua" "thereplusxy" "x+=")
%D diagram new-pres-T-and-AND-dnc
%D 2Dx 100 +30 +30 +45 +45
%D 2D 100 A0 <============ A1
%D 2D ^ ^ ^
%D 2D | \ <-| |
%D 2D - - -
%D 2D +20 T0 <==== T1 A2 <--| A3 <==== A4
%D 2D - - - -
%D 2D | | / <-| |
%D 2D v v v v
%D 2D +20 T2 A5 <============ A6
%D 2D
%D 2D +15 ta |---> tb aa |-----------> ab
%D 2D
%D (( T0 .tex= ⊤ T1 .tex= ⊤
%D T2 .tex= ⊤
%D ta .tex= a tb .tex= b
%D T0 T1 <= T0 T2 |-> sl_ .plabel= l ♮ T0 T2 <-| sl^ .plabel= r 𝐬P⊤
%D ta tb |->
%D ))
%D (( A0 .tex= P A1 .tex= P
%D A2 .tex= P&Q A3 .tex= P&Q A4 .tex= P&Q
%D A5 .tex= Q A6 .tex= Q
%D aa x+= 10 .tex= a ab .tex= b
%D A0 A1 <=
%D A0 A2 <-| A0 A3 <-|
%D A1 A4 <-|
%D A0 A3 midpoint A1 A4 midpoint harrownodes nil 20 nil <-|
%D A2 A3 <-| sl^ .plabel= a {♮} A2 A3 |-> sl_ .plabel= b 𝐬P& A3 A4 <=
%D A2 A5 |-> A3 A5 |->
%D A4 A6 |->
%D A3 A5 midpoint A4 A6 midpoint harrownodes nil 20 nil <-|
%D A5 A6 <=
%D aa ab |->
%D ))
%D enddiagram
%D diagram new-pres-T-and-AND-std
%D 2Dx 100 +30 +30 +45 +45
%D 2D 100 A0 <============ A1
%D 2D ^ ^ ^
%D 2D | \ <-| |
%D 2D - - -
%D 2D +20 T0 <==== T1 A2 <--| A3 <==== A4
%D 2D - - - -
%D 2D | | / <-| |
%D 2D v v v v
%D 2D +20 T2 A5 <============ A6
%D 2D
%D 2D +15 ta |---> tb aa |-----------> ab
%D 2D
%D (( T0 .tex= f^*⊤_B T1 .tex= ⊤_B
%D T2 .tex= ⊤_A
%D ta .tex= A tb .tex= B
%D T0 T1 <-| T0 T2 -> sl_ .plabel= l ♮ T0 T2 <- sl^ .plabel= r 𝐬P⊤
%D ta tb -> .plabel= a f
%D ))
%D (( A0 .tex= f^*P A1 .tex= P
%D A2 .tex= f^*P&f^*Q A3 .tex= f^*(P&Q) A4 .tex= P&Q
%D A5 .tex= f^*Q A6 .tex= Q
%D aa x+= 10 .tex= A ab .tex= B
%D A0 A1 <-|
%D A0 A2 <- A0 A3 <-
%D A1 A4 <-
%D A0 A3 midpoint A1 A4 midpoint harrownodes nil 20 nil <-|
%D A2 A3 <- sl^ .plabel= a {♮} A2 A3 -> sl_ .plabel= b 𝐬P& A3 A4 <-|
%D A2 A5 -> A3 A5 ->
%D A4 A6 ->
%D A3 A5 midpoint A4 A6 midpoint harrownodes nil 20 nil <-|
%D A5 A6 <-|
%D aa ab -> .plabel= a f
%D ))
%D enddiagram
$$\diag{new-pres-T-and-AND-dnc}$$
$$\diag{new-pres-T-and-AND-std}$$
\newpage
% --------------------
% «pres-of-false-and-or» (to ".pres-of-false-and-or")
% (s "Preservation of `false' and `or'" "pres-of-false-and-or")
\myslide {Preservation of `false' and `or'} {pres-of-false-and-or}
%D diagram pres-bot-and-or-dnc
%D 2Dx 100 +30 +30 +45 +45
%D 2D 100 I0 O0 <============ O1
%D 2D -^ - - -
%D 2D ♮|| | \ <-| |
%D 2D v- v v v
%D 2D +20 I1 <==== I2 O2 |--> O3 <==== O4
%D 2D ^ ^ ^
%D 2D | / <-| |
%D 2D - - -
%D 2D +20 O5 <============ O6
%D 2D
%D 2D +15 ia |---> ib oa |-----------> ob
%D 2D
%D (( I0 .tex= ⊥
%D I1 .tex= ⊥ I2 .tex= ⊥
%D ia .tex= a ib .tex= b
%D I1 I2 <=
%D I0 I1 |-> sl_ .plabel= l ♮ I0 I1 <-| sl^ .plabel= r 𝐬P⊥
%D ia ib |->
%D ))
%D (( O0 .tex= P O1 .tex= P
%D O2 .tex= P∨Q O3 .tex= P∨Q O4 .tex= P∨Q
%D O5 .tex= Q O6 .tex= Q
%D oa x+= 10 .tex= a ob .tex= b
%D O0 O1 <=
%D O0 O2 |-> O0 O3 |->
%D O1 O4 |->
%D O0 O3 midpoint O1 O4 midpoint harrownodes nil 20 nil <-|
%D O2 O3 |-> sl^ .plabel= a {♮} O2 O3 <-| sl_ .plabel= b 𝐬P∨ O3 O4 <=
%D O2 O5 <-| O3 O5 <-|
%D O4 O6 <-|
%D O3 O5 midpoint O4 O6 midpoint harrownodes nil 20 nil <-|
%D O5 O6 <=
%D oa ob |->
%D ))
%D enddiagram
%D diagram pres-bot-and-or-std
%D 2Dx 100 +30 +30 +45 +45
%D 2D 100 I0 O0 <============ O1
%D 2D -^ - - -
%D 2D ♮|| | \ <-| |
%D 2D v- v v v
%D 2D +20 I1 <==== I2 O2 |--> O3 <==== O4
%D 2D ^ ^ ^
%D 2D | / <-| |
%D 2D - - -
%D 2D +20 O5 <============ O6
%D 2D
%D 2D +15 ia |---> ib oa |-----------> ob
%D 2D
%D (( I0 .tex= ⊥_A
%D I1 .tex= f^*⊥_B I2 .tex= ⊥_B
%D ia .tex= a ib .tex= b
%D I1 I2 <-|
%D I0 I1 -> sl_ .plabel= l ♮ I0 I1 <- sl^ .plabel= r 𝐬P⊥
%D ia ib ->
%D ))
%D (( O0 .tex= f^*P O1 .tex= P
%D O2 .tex= f^*P∨f^*Q O3 .tex= f^*(P∨Q) O4 .tex= P∨Q
%D O5 .tex= f^*Q O6 .tex= Q
%D oa x+= 10 .tex= a ob .tex= b
%D O0 O1 <-|
%D O0 O2 -> O0 O3 ->
%D O1 O4 ->
%D O0 O3 midpoint O1 O4 midpoint harrownodes nil 20 nil <-|
%D O2 O3 -> sl^ .plabel= a {♮} O2 O3 <- sl_ .plabel= b 𝐬P∨ O3 O4 <-|
%D O2 O5 <- O3 O5 <-
%D O4 O6 <-
%D O3 O5 midpoint O4 O6 midpoint harrownodes nil 20 nil <-|
%D O5 O6 <-|
%D oa ob ->
%D ))
%D enddiagram
$$\diag{pres-bot-and-or-dnc}$$
$$\diag{pres-bot-and-or-std}$$
\newpage
% --------------------
% «pres-of-imp» (to ".pres-of-imp")
% (s "Preservation of `implies'" "pres-of-imp")
\myslide {Preservation of `implies'} {pres-of-imp}
%D diagram new-pres-prod-1
%D 2Dx 100 +45 +55 +45
%D 2Dx 100 +60 +55 +60
%D 2D 100 B0 <-> B0' <============== B1
%D 2D -/\ -/\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\==================== B3 \\
%D 2D \\ \\ \\ \\
%D 2D +15 \\ B4 <===================== B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \/v Vv
%D 2D +20 B6 B7
%D 2D
%D 2D +0 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +35 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= (P→Q)&P B0' .tex= (P→Q)&P B1 .tex= (P→Q)&P
%D B2 .tex= Q B3 .tex= Q
%D B4 .tex= P→Q B5 .tex= P→Q
%D B6 .tex= P→Q B7 .tex= P→Q
%D B0 B0' <-| sl^ .plabel= a {♮}
%D B0 B0' |-> sl_ .plabel= b 𝐬P&
%D B0' B1 <= B0 B2 |-> B0' B2 |-> B1 B3 |-> B2 B3 <=
%D B0 B4 <= B2 B6 =>
%D B1 B5 <= B3 B7 =>
%D B4 B5 <= B5 B7 |-> .plabel= r \id
%D B4 B6 |-> sl_ .plabel= l ♮ B4 B6 <-| sl^ .plabel= r 𝐬P→
%D B0' B2 midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( b0 b2 midpoint .TeX= a b1 b3 midpoint .TeX= b |->
%D ))
%D enddiagram
%
$$\diag{new-pres-prod-1}$$
%D diagram new-pres-prod-2
%D 2Dx 100 +60 +55 +60
%D 2D 100 B0 <-> B0' <============== B1
%D 2D -/\ -/\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\==================== B3 \\
%D 2D \\ \\ \\ \\
%D 2D +25 \\ B4 <===================== B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \/v Vv
%D 2D +20 B6 B7
%D 2D
%D 2D +0 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +35 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= f^*(P→Q)&f^*P B0' .tex= f^*((P→Q)&P) B1 .tex= (P→Q)&P
%D B2 .tex= f^*Q B3 .tex= Q
%D B4 .tex= f^*(P→Q) B5 .tex= P→Q
%D B6 .tex= f^*P→f^*Q B7 .tex= P→Q
%D B0 B0' <- sl^ .plabel= a {♮}
%D B0 B0' -> sl_ .plabel= b 𝐬P&
%D B0' B1 <-| B0 B2 -> B0' B2 -> B1 B3 -> B2 B3 <-|
%D B0 B4 <-| B2 B6 |->
%D B1 B5 <-| B3 B7 |->
%D B4 B5 <-| B5 B7 -> .plabel= r \id
%D B4 B6 -> sl_ .plabel= l ♮ B4 B6 <- sl^ .plabel= r 𝐬P→
%D B0' B2 midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( b0 b2 midpoint .TeX= A b1 b3 midpoint .TeX= B -> .plabel= a f
%D ))
%D enddiagram
%
$$\diag{new-pres-prod-2}$$
%%D (( b0 .tex= a,c b1 .tex= a
%%D b2 .tex= b,c b3 .tex= b
%%D b0 b1 |->
%%D b0 b2 |-> b1 b3 |->
%%D b2 b3 |->
%%D b0 relplace 18 9 \pbsymbol{9}
%%D ))
\newpage
% --------------------
% «bcc-for-forall» (to ".bcc-for-forall")
% (s "BCC for `forall'" "bcc-for-forall")
\myslide {BCC for `forall'} {bcc-for-forall}
%D diagram bcc-for-forall-1
%D 2Dx 100 +45 +55 +45
%D 2D 100 B0 <-> B0' <============== B1
%D 2D -/\ -/\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\==================== B3 \\
%D 2D \\ \\ \\ \\
%D 2D +15 \\ B4 <===================== B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \/v Vv
%D 2D +20 B6 B7
%D 2D
%D 2D +10 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +35 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= ∀c.P B0' .tex= ∀c.P B1 .tex= ∀c.P
%D B2 .tex= P B3 .tex= P
%D B4 .tex= ∀c.P B5 .tex= ∀c.P
%D B6 .tex= ∀c.P B7 .tex= ∀c.P
%D B0 B0' <-> B0' B1 <= B0 B2 |-> B0' B2 |-> B1 B3 |-> B2 B3 <=
%D B0 B4 <= B2 B6 =>
%D B1 B5 <= B3 B7 =>
%D B4 B5 <= B5 B7 |-> .plabel= r \id
%D B4 B6 |-> sl_ .plabel= l ♮ B4 B6 <-| sl^ .plabel= r 𝐬{BCC}∀
%D B0' B2 midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a,c b1 .tex= b,c b2 .tex= a b3 .tex= b
%D b0 b1 |-> b0 b2 |-> b1 b3 |-> b2 b3 |->
%D b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-for-forall-1}$$
% dnc->std: (fooi "`->" ">->" "|->" "->" "<-|" "<-" "=>" "|->" "<=" "<-|")
%D diagram bcc-for-forall-2
%D 2Dx 100 +45 +55 +45
%D 2D 100 B0 <-> B0' <============== B1
%D 2D -/\ -/\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\==================== B3 \\
%D 2D \\ \\ \\ \\
%D 2D +15 \\ B4 <===================== B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \/v Vv
%D 2D +20 B6 B7
%D 2D
%D 2D +10 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +35 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= c'*f^*∀_cP B0' .tex= f'*c^*∀_cP B1 .tex= c^*∀_cP
%D B2 .tex= f'*P B3 .tex= P
%D B4 .tex= f^*∀_cP B5 .tex= ∀_cP
%D B6 .tex= ∀_{c'}f'*P B7 .tex= ∀_cP
%D B0 B0' <-> B0' B1 <-| B0 B2 -> B0' B2 -> B1 B3 -> B2 B3 <-|
%D B0 B4 <-| B2 B6 |->
%D B1 B5 <-| B3 B7 |->
%D B4 B5 <-| B5 B7 -> .plabel= r \id
%D B4 B6 -> sl_ .plabel= l ♮ B4 B6 <- sl^ .plabel= r 𝐬{BCC}∀
%D B0' B2 midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= A×C b1 .tex= B×C b2 .tex= A b3 .tex= B
%D b0 b1 -> .plabel= b f'
%D b0 b2 -> .plabel= l c'
%D b1 b3 -> .plabel= r c
%D b2 b3 -> .plabel= a f
%D b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-for-forall-2}$$
\newpage
% --------------------
% «bcc-for-exists» (to ".bcc-for-exists")
% (s "BCC for `exists'" "bcc-for-exists")
\myslide {BCC for `exists'} {bcc-for-exists}
%D diagram bcc-for-exists-1
%D 2Dx 100 +45 +55 +45
%D 2D 100 B0 <====================== B1
%D 2D -\\ -\\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\> B2' ============== B3 \\
%D 2D /\ \/ /\ \/
%D 2D +15 \\ B4 \\ B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +20 B6 <===================== B7
%D 2D
%D 2D +10 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +35 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= P B1 .tex= P
%D B2 .tex= ∃c.P B2' .tex= ∃c.P B3 .tex= ∃c.P
%D B4 .tex= ∃c.P B5 .tex= ∃c.P
%D B6 .tex= ∃c.P B7 .tex= ∃c.P
%D B0 B1 <= B0 B2 |-> B0 B2' |-> B1 B3 |-> B2 B2' <-> B2' B3 <=
%D B0 B4 => B1 B5 =>
%D B2 B6 <= B3 B7 <=
%D B6 B7 <= B5 B7 |-> .plabel= r \id
%D B4 B6 |-> sl_ .plabel= l ♮ B4 B6 <-| sl^ .plabel= r 𝐬{BCC}∃
%D B0 B2' midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a,c b1 .tex= b,c b2 .tex= a b3 .tex= b
%D b0 b1 |-> b0 b2 |-> b1 b3 |-> b2 b3 |->
%D b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-for-exists-1}$$
% dnc->std: (fooi "`->" ">->" "|->" "->" "<-|" "<-" "=>" "|->" "<=" "<-|")
%D diagram bcc-for-exists-2
%D 2Dx 100 +45 +55 +45
%D 2D 100 B0 <====================== B1
%D 2D -\\ -\\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\> B2' ============== B3 \\
%D 2D /\ \/ /\ \/
%D 2D +15 \\ B4 \\ B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +20 B6 <===================== B7
%D 2D
%D 2D +10 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +35 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= f'*P B1 .tex= P
%D B2 .tex= c'*f^*∃_cP B2' .tex= f'*c^*∃_cP B3 .tex= c^*∃_cP
%D B4 .tex= ∃_{c'}f'*P B5 .tex= ∃_cP
%D B6 .tex= f^*∃_cP B7 .tex= ∃_cP
%D B0 B1 <-| B0 B2 -> B0 B2' -> B1 B3 -> B2 B2' <-> B2' B3 <-|
%D B0 B4 |-> B1 B5 |->
%D B2 B6 <-| B3 B7 <-|
%D B6 B7 <-| B5 B7 -> .plabel= r \id
%D B4 B6 -> sl_ .plabel= l ♮ B4 B6 <- sl^ .plabel= r 𝐬{BCC}∃
%D B0 B2' midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= A×C b1 .tex= B×C b2 .tex= A b3 .tex= B
%D b0 b1 -> .plabel= b f'
%D b0 b2 -> .plabel= l c'
%D b1 b3 -> .plabel= r c
%D b2 b3 -> .plabel= b f
%D b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-for-exists-2}$$
\newpage
% --------------------
% «bcc-for-equality» (to ".bcc-for-equality")
% (s "BCC for equality" "bcc-for-equality")
\myslide {BCC for equality} {bcc-for-equality}
%D diagram bcc-for-equality-1
%D 2Dx 100 +45 +55 +45
%D 2D 100 B0 <====================== B1
%D 2D -\\ -\\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\> B2' ============== B3 \\
%D 2D /\ \/ /\ \/
%D 2D +15 \\ B4 \\ B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +20 B6 <===================== B7
%D 2D
%D 2D +10 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +35 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= P B1 .tex= P
%D B2 .tex= c{=}c{&}P B2' .tex= c{=}c{&}P B3 .tex= c{=}c{&}P
%D B4 .tex= c{=}c'{&}P B5 .tex= c{=}c'{&}P
%D B6 .tex= c{=}c'{&}P B7 .tex= c{=}c'{&}P
%D B0 B1 <= B0 B2 |-> B0 B2' |-> B1 B3 |-> B2 B2' <-> B2' B3 <=
%D B0 B4 => B1 B5 =>
%D B2 B6 <= B3 B7 <=
%D B6 B7 <= B5 B7 |-> .plabel= r \id
%D B4 B6 |-> sl_ .plabel= l ♮ B4 B6 <-| sl^ .plabel= r 𝐬{BCC}∃
%D B0 B2' midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a,c b1 .tex= b,c b2 .tex= a,c,c' b3 .tex= b,c,c'
%D b0 b1 |-> b0 b2 |-> b1 b3 |-> b2 b3 |->
%D b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-for-equality-1}$$
%D diagram bcc-for-equality-2
%D 2Dx 100 +45 +55 +45
%D 2D 100 B0 <====================== B1
%D 2D -\\ -\\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\> B2' ============== B3 \\
%D 2D /\ \/ /\ \/
%D 2D +15 \\ B4 \\ B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +20 B6 <===================== B7
%D 2D
%D 2D +10 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +35 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= f'*P B1 .tex= P
%D B2 .tex= c'*f^*\Eq_{c}P B2' .tex= f'*c^*\Eq_{c}P B3 .tex= c^*\Eq_{c}P
%D B4 .tex= \Eq_{c'}f'*P B5 .tex= \Eq_{c}P
%D B6 .tex= f^*\Eq_{c}P B7 .tex= \Eq_{c}P
%D B0 B1 <-| B0 B2 -> B0 B2' -> B1 B3 -> B2 B2' <-> B2' B3 <-|
%D B0 B4 |-> B1 B5 |->
%D B2 B6 <-| B3 B7 <-|
%D B6 B7 <-| B5 B7 -> .plabel= r \id
%D B4 B6 -> sl_ .plabel= l ♮ B4 B6 <- sl^ .plabel= r 𝐬{BCC}=
%D B0 B2' midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= A×C b1 .tex= B×C b2 .tex= A×C×C b3 .tex= B×C×C
%D b0 b1 -> .plabel= b f'
%D b0 b2 -> .plabel= l c'
%D b1 b3 -> .plabel= r c
%D b2 b3 -> .plabel= b f
%D b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-for-equality-2}$$
\newpage
% --------------------
% «frob-for-exists» (to ".frob-for-exists")
% (s "Frobenius for `exists'" "frob-for-exists")
\myslide {Frobenius for `exists'} {frob-for-exists}
%D diagram frob-for-exists-1
%D 2Dx 100 +45 +35 +10
%D 2D 100 B0 ================> B1
%D 2D ^ ^ ^
%D 2D | / |
%D 2D - \ -
%D 2D +20 B2 ========> B3 <--> B3'
%D 2D - / -
%D 2D | \ |
%D 2D v v v
%D 2D +20 B4 <================ B5
%D 2D
%D 2D +15 b0 |-----------> b1
%D 2D
%D ((
%D B0 .tex= P B1 .tex= ∃c.P
%D B2 .tex= P&Q B3 .tex= ∃c.(P&Q) B3' .tex= (∃c.P)&Q
%D B4 .tex= Q B5 .tex= Q
%D B0 B1 => B2 B0 |-> B3 B1 |-> B3' B1 |->
%D B4 B5 <= B2 B4 |-> B3 B5 |-> B3' B5 |->
%D B2 B3 => B3 B3' |-> sl^ .plabel= a ♮ B3 B3' <-| sl_ .plabel= b 𝐬{Frob}∃
%D B0 B2 midpoint B1 B3 midpoint harrownodes nil 20 nil |->
%D B2 B4 midpoint B3 B5 midpoint harrownodes nil 20 nil |->
%D ))
%D (( b0 .tex= b,c b1 .tex= b b0 b1 |->
%D ))
%D enddiagram
%
$$\diag{frob-for-exists-1}$$
% dnc->std: (fooi "`->" ">->" "|->" "->" "<-|" "<-" "=>" "|->" "<=" "<-|")
%D diagram frob-for-exists-2
%D 2Dx 100 +45 +35 +10
%D 2D 100 B0 ================> B1
%D 2D ^ ^ ^
%D 2D | / |
%D 2D - \ -
%D 2D +20 B2 ========> B3 <--> B3'
%D 2D - / -
%D 2D | \ |
%D 2D v v v
%D 2D +20 B4 <================ B5
%D 2D
%D 2D +15 b0 |-----------> b1
%D 2D
%D ((
%D B0 .tex= P B1 .tex= ∃_cP
%D B2 .tex= P&c^*Q B3 .tex= ∃_c(P&c^*Q) B3' .tex= (∃_cP)&Q
%D B4 .tex= c^*Q B5 .tex= Q
%D B0 B1 |-> B2 B0 -> B3 B1 -> B3' B1 ->
%D B4 B5 <-| B2 B4 -> B3 B5 -> B3' B5 ->
%D B2 B3 |-> B3 B3' -> sl^ .plabel= a ♮ B3 B3' <- sl_ .plabel= b 𝐬{Frob}∃
%D B0 B2 midpoint B1 B3 midpoint harrownodes nil 20 nil |->
%D B2 B4 midpoint B3 B5 midpoint harrownodes nil 20 nil |->
%D ))
%D (( b0 .tex= B×C b1 .tex= B b0 b1 -> .plabel= a c
%D ))
%D enddiagram
%
$$\diag{frob-for-exists-2}$$
\newpage
% --------------------
% «frob-for-equality» (to ".frob-for-equality")
% (s "Frobenius for equality" "frob-for-equality")
\myslide {Frobenius for equality} {frob-for-equality}
%D diagram frob-for-equality-1
%D 2Dx 100 +50 +40 +15
%D 2D 100 B0 ================> B1
%D 2D ^ ^ ^
%D 2D | / |
%D 2D - \ -
%D 2D +20 B2 ========> B3 <--> B3'
%D 2D - / -
%D 2D | \ |
%D 2D v v v
%D 2D +20 B4 <================ B5
%D 2D
%D 2D +15 b0 |-----------> b1
%D 2D
%D ((
%D B0 .tex= P B1 .tex= c{=}c'{&}P
%D B2 .tex= P&Q B3 .tex= c{=}c'{&}(P&Q) B3' .tex= (c{=}c'{&}P)&Q
%D B4 .tex= Q B5 .tex= Q
%D B0 B1 => B2 B0 |-> B3 B1 |-> B3' B1 |->
%D B4 B5 <= B2 B4 |-> B3 B5 |-> B3' B5 |->
%D B2 B3 => B3 B3' |-> sl^ .plabel= a ♮ B3 B3' <-| sl_ .plabel= b 𝐬{Frob}=
%D B0 B2 midpoint B1 B3 midpoint harrownodes nil 20 nil |->
%D B2 B4 midpoint B3 B5 midpoint harrownodes nil 20 nil |->
%D ))
%D (( b0 .tex= b,c b1 .tex= b,c,c' b0 b1 |->
%D ))
%D enddiagram
%
$$\diag{frob-for-equality-1}$$
%D diagram frob-for-equality-2
%D 2Dx 100 +45 +35 +10
%D 2Dx 100 +50 +40 +15
%D 2D 100 B0 ================> B1
%D 2D ^ ^ ^
%D 2D | / |
%D 2D - \ -
%D 2D +20 B2 ========> B3 <--> B3'
%D 2D - / -
%D 2D | \ |
%D 2D v v v
%D 2D +20 B4 <================ B5
%D 2D
%D 2D +15 b0 |-----------> b1
%D 2D
%D ((
%D B0 .tex= P B1 .tex= \Eq_cP
%D B2 .tex= P&c^*Q B3 .tex= \Eq_c(P&c^*Q) B3' .tex= (\Eq_cP)&Q
%D B4 .tex= c^*Q B5 .tex= Q
%D B0 B1 |-> B2 B0 -> B3 B1 -> B3' B1 ->
%D B4 B5 <-| B2 B4 -> B3 B5 -> B3' B5 ->
%D B2 B3 |-> B3 B3' -> sl^ .plabel= a ♮ B3 B3' <- sl_ .plabel= b 𝐬{Frob}=
%D B0 B2 midpoint B1 B3 midpoint harrownodes nil 20 nil |->
%D B2 B4 midpoint B3 B5 midpoint harrownodes nil 20 nil |->
%D ))
%D (( b0 .tex= B×C b1 .tex= B×C×C b0 b1 -> .plabel= a c
%D ))
%D enddiagram
%
$$\diag{frob-for-equality-2}$$
\newpage
% --------------------
% «frob-for-ex-eq» (to ".frob-for-ex-eq")
% (s "Frobenius for exists-equal" "frob-for-ex-eq")
\myslide {Frobenius for exists-equal} {frob-for-ex-eq}
%D diagram frob-for-ex-eq-1
%D 2Dx 100 +60 +55 +25
%D 2D 100 B0 ================> B1
%D 2D ^ ^ ^
%D 2D | / |
%D 2D - \ -
%D 2D +20 B2 ========> B3 <--> B3'
%D 2D - / -
%D 2D | \ |
%D 2D v v v
%D 2D +20 B4 <================ B5
%D 2D
%D 2D +15 b0 |-----------> b1
%D 2D
%D ((
%D B0 .tex= Pa B1 .tex= ∃a.b=fa&Pa
%D B2 .tex= Pa&Qfa B3 .tex= ∃a.b=fa&(Pa&Qfa) B3' .tex= (∃a.b=fa&Pa)&Qb
%D B4 .tex= Qfa B5 .tex= Qb
%D B0 B1 => B2 B0 |-> B3 B1 |-> B3' B1 |->
%D B4 B5 <= B2 B4 |-> B3 B5 |-> B3' B5 |->
%D B2 B3 => B3 B3' |-> sl^ .plabel= a ♮ B3 B3' <-| sl_ .plabel= b 𝐬{Frob}∃=
%D B0 B2 midpoint B1 B3 midpoint harrownodes nil 20 nil |->
%D B2 B4 midpoint B3 B5 midpoint harrownodes nil 20 nil |->
%D ))
%D (( b0 .tex= a b1 .tex= b b0 b1 |->
%D ))
%D enddiagram
%
$$\diag{frob-for-ex-eq-1}$$
%D diagram frob-for-ex-eq-2
%D 2Dx 100 +60 +55 +25
%D 2D 100 B0 ================> B1
%D 2D ^ ^ ^
%D 2D | / |
%D 2D - \ -
%D 2D +20 B2 ========> B3 <--> B3'
%D 2D - / -
%D 2D | \ |
%D 2D v v v
%D 2D +20 B4 <================ B5
%D 2D
%D 2D +15 b0 |-----------> b1
%D 2D
%D ((
%D B0 .tex= P B1 .tex= \Eq_fP
%D B2 .tex= P&f^*Q B3 .tex= \Eq_f(P&f^*Q) B3' .tex= (\Eq_fP)&Q
%D B4 .tex= f^*Q B5 .tex= Q
%D B0 B1 |-> B2 B0 -> B3 B1 -> B3' B1 ->
%D B4 B5 <-| B2 B4 -> B3 B5 -> B3' B5 ->
%D B2 B3 |-> B3 B3' -> sl^ .plabel= a ♮ B3 B3' <- sl_ .plabel= b 𝐬{Frob}∃=
%D B0 B2 midpoint B1 B3 midpoint harrownodes nil 20 nil |->
%D B2 B4 midpoint B3 B5 midpoint harrownodes nil 20 nil |->
%D ))
%D (( b0 .tex= A b1 .tex= B b0 b1 -> .plabel= a f
%D ))
%D enddiagram
%
$$\diag{frob-for-ex-eq-2}$$
\newpage
% --------------------
% «frob-and-pres-imp» (to ".frob-and-pres-imp")
% (s "Frobenius is equivalent to preservation of `implies'" "frob-and-pres-imp")
\myslide {Frobenius is equivalent to preservation of `implies'} {frob-and-pres-imp}
%D diagram lawfrob1
%D 2Dx 100 +40 +35 +40 +40 +45
%D 2D \aa∧()
%D 2D 100 P(Y)`0 -----> P(Y)`1 \aa∧\phiΣf <----| \phiΣf (∃b.Pab)∧Qa <=== ∃b.Pab
%D 2D | | ♮ ^v Frob ^ ♮ ^v Frob /\
%D 2D +20 | | ((f·\aa)∧\phi)Σf | ∃b.(Pab∧Qa) ||
%D 2D ()Σf| ()Σf| ^ | /\ ||
%D 2D v v | - || ||
%D 2D +30 P(X)`0 -----> P(X)`1 (f·\aa)∧\phi <---| \phi Pab∧Qa <====== Pab
%D 2D (f·\aa)∧()
%D 2D
%D (( P(Y)`0 P(Y)`1
%D P(X)`0 P(X)`1
%D @ 0 @ 1 <- .plabel= a \aa∧(\;)
%D @ 0 @ 2 <- .plabel= l (\;)Σf
%D @ 1 @ 3 <- .plabel= l (\;)Σf
%D @ 2 @ 3 <- .plabel= b (f·\aa)∧(\;)
%D ))
%D (( \aa∧\phiΣf \phiΣf
%D ((f·\aa)∧\phi)Σf
%D (f·\aa)∧\phi \phi
%D @ 0 @ 1 <-|
%D @ 0 @ 2 <- sl_ .plabel= l ♮ @ 0 @ 2 -> sl^ .plabel= r 𝐬{Frob}
%D @ 2 @ 3 <-| @ 1 @ 4 <-|
%D @ 3 @ 4 <-|
%D ))
%D (( (∃b.Pab)∧Qa ∃b.Pab
%D ∃b.(Pab∧Qa)
%D Pab∧Qa Pab
%D @ 0 @ 1 <=
%D @ 0 @ 2 <-| sl_ .plabel= l ♮ @ 0 @ 2 |-> sl^ .plabel= r 𝐬{Frob}
%D @ 2 @ 3 <= @ 1 @ 4 <=
%D @ 3 @ 4 <=
%D ))
%D enddiagram
%D
$$\diag{lawfrob1}$$
%D diagram lawfrob2
%D 2Dx 100 +40 +35 +40 +40 +45
%D 2D \aa=>()
%D 2D 100 P(Y)`0 -----> P(Y)`1 \psi |----> \aa=>\psi Ra`0 ===> Qa→Ra`0
%D 2D | | - - || ||
%D 2D f·()| f·()| | v || \/
%D 2D +30 | | | f·(\aa=>\psi) || Qa→Ra`1
%D 2D v v v ♮ v^ P→ \/ ♮ v^ P→
%D 2D +20 P(X)`0 -----> P(X)`1 f·\psi |--> f·\aa=>f·\psi Ra`2 ===> Qa→Ra`2
%D 2D (f·\aa)=>()
%D 2D
%D (( P(Y)`0 P(Y)`1
%D P(X)`0 P(X)`1
%D @ 0 @ 1 -> .plabel= a \aa=>(\;)
%D @ 0 @ 2 -> .plabel= l f·(\;)
%D @ 1 @ 3 -> .plabel= l f·(\;)
%D @ 2 @ 3 -> .plabel= b (f·\aa)=>(\;)
%D ))
%D (( \psi \aa=>\psi
%D f·(\aa=>\psi)
%D f·\psi f·\aa=>f·\psi
%D @ 0 @ 1 |-> @ 0 @ 3 |-> @ 1 @ 2 |-> @ 3 @ 4 |->
%D @ 2 @ 4 -> sl_ .plabel= l ♮ @ 2 @ 4 <- sl^ .plabel= r 𝐬P→
%D ))
%D (( Ra`0 Qa→Ra`0
%D Qa→Ra`1
%D Ra`2 Qa→Ra`2
%D @ 0 @ 1 => @ 0 @ 3 => @ 1 @ 2 => @ 3 @ 4 =>
%D @ 2 @ 4 |-> sl_ .plabel= l ♮ @ 2 @ 4 <- sl^ .plabel= r 𝐬P→
%D ))
%D enddiagram
%D
$$\diag{lawfrob2}$$
%D diagram lawfrob-std
%D 2Dx 100 +80
%D 2D 100 \H{\aa∧\phiΣf}{\psi} <---> \H{\phiΣf}{\aa=>\psi}
%D 2D ♮ v^ Frob ^
%D 2D +20 \H{((f·\aa)∧\phi)Σf}{\psi} |
%D 2D ^ |
%D 2D | |
%D 2D | v
%D 2D +10 | \H{\phi}{f·(\aa=>\psi)}
%D 2D v ♮ v^ P→
%D 2D +20 \H{(f·\aa)∧\phi}{f·\psi} <---> \H{\phi}{f·\aa=>f·\psi)}
%D 2D
%D (( \H{\aa∧\phiΣf}{\psi} \H{\phiΣf}{\aa=>\psi}
%D \H{((f·\aa)∧\phi)Σf}{\psi}
%D \H{\phi}{f·(\aa=>\psi)}
%D \H{(f·\aa)∧\phi}{f·\psi} \H{\phi}{f·\aa=>f·\psi)}
%D @ 0 @ 1 <->
%D @ 0 @ 2 -> sl_ .plabel= l ♮ @ 0 @ 2 <- sl^ .plabel= r 𝐬{Frob}
%D @ 1 @ 3 <-> @ 2 @ 4 <->
%D @ 3 @ 5 -> sl_ .plabel= l ♮ @ 3 @ 5 <- sl^ .plabel= r 𝐬P→
%D @ 4 @ 5 <->
%D ))
%D enddiagram
%D
$$\def\H#1#2{(#1\to#2)}
\diag{lawfrob-std}
$$
%D diagram lawfrob-dnc
%D 2Dx 100 +70
%D 2D 100 (∃b.Pab)∧Qa|-Ra <-> ∃b.Pab|-Qa→Ra
%D 2D ♮ v^ Frob ^
%D 2D +20 ∃b.(Pab∧Qa)|-Ra |
%D 2D ^ |
%D 2D | |
%D 2D | v
%D 2D +10 | Pab|-Qa→Ra`1
%D 2D v ♮ v^ P→
%D 2D +20 Pab∧Qa|-Ra <---> Pab|-Qa→Ra`2
%D 2D
%D (( (∃b.Pab)∧Qa|-Ra ∃b.Pab|-Qa→Ra
%D ∃b.(Pab∧Qa)|-Ra
%D Pab|-Qa→Ra`1
%D Pab∧Qa|-Ra Pab|-Qa→Ra`2
%D @ 0 @ 1 <->
%D @ 0 @ 2 -> sl_ .plabel= l ♮ @ 0 @ 2 <- sl^ .plabel= r 𝐬{Frob}
%D @ 1 @ 3 <-> @ 2 @ 4 <->
%D @ 3 @ 5 -> sl_ .plabel= l ♮ @ 3 @ 5 <- sl^ .plabel= r 𝐬P→
%D @ 4 @ 5 <->
%D ))
%D enddiagram
%D
$$\diag{lawfrob-dnc}$$
\newpage
% --------------------
% «bcc-ex-iff-bcc-fa» (to ".bcc-ex-iff-bcc-fa")
% (s "BCC for `exists' holds iff BCC for `forall' holds" "bcc-ex-iff-bcc-fa")
\myslide {BCC for `exists' holds iff BCC for `forall' holds} {bcc-ex-iff-bcc-fa}
%D diagram lawbcc1
%D 2Dx 100 +40 +35 +40 +40 +45
%D 2D 100 X -------> X' f·\psi |--> (f·\psi)Σx x·\phi <-------| \phi
%D 2D | _| x | ^ ♮ v^ BCCΣ - -
%D 2D +20 | | | f'·(\psiΣy) | |
%D 2D | f f' | | ^ v |
%D 2D +10 | | | | (x·\phi)Πf |
%D 2D v y v - - ♮ ^v BCCΠ v
%D 2D +20 Y -------> Y' \psi |----> \psiΣy y·(\phiΠf') <--| \phiΠf'
%D 2D
%D 2D +20 a,b,c |---> a,b Pac`2 ====> ∃c.Pac`2 Rab`1 <========= Rab`0
%D 2D - _| - /\ ♮ v^ BCC∃ || ||
%D 2D +20 | | || ∃c.Pac`1 || ||
%D 2D | | || /\ \/ ||
%D 2D +10 | | || || ∀b.Rab`2 ||
%D 2D v v || || ♮ ^v BCC∀ \/
%D 2D +20 a,c |-----> a Pac`0 ====> ∃c.Pac`0 ∀b.Rab`1 <===== ∀b.Rab`0
%D 2D
%D (( X X' Y Y'
%D @ 0 @ 1 -> .plabel= a x @ 0 relplace 7 7 \pbsymbol{7} # _|
%D @ 0 @ 2 -> .plabel= l f
%D @ 1 @ 3 -> .plabel= l f'
%D @ 2 @ 3 -> .plabel= a y
%D ))
%D (( f·\psi (f·\psi)Σx
%D f'·(\psiΣy)
%D \psi \psiΣy
%D @ 0 @ 1 |-> .plabel= a (\;)Σx
%D @ 0 @ 3 <-| .plabel= l f·(\;)
%D @ 1 @ 2 -> sl_ .plabel= l ♮ @ 1 @ 2 <- sl^ .plabel= r 𝐬{BCC}
%D @ 2 @ 4 <-| .plabel= l f'·(\;)
%D @ 3 @ 4 |-> .plabel= a (\;)Σy
%D ))
%D (( x·\phi \phi
%D (x·\phi)Πf
%D y·(\phiΠf') \phiΠf'
%D @ 0 @ 1 <-| .plabel= a x·(\;)
%D @ 0 @ 2 |-> .plabel= l (\;)Πf
%D @ 1 @ 4 |-> .plabel= l (\;)Πf'
%D @ 2 @ 3 -> sl_ .plabel= l ♮ @ 2 @ 3 <- sl^ .plabel= r 𝐬{BCC}
%D @ 3 @ 4 <-| .plabel= a y·(\;)
%D ))
%D (( a,b,c a,b a,c a
%D @ 0 @ 1 |-> @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D @ 0 relplace 7 7 \pbsymbol{7} # _|
%D ))
%D (( Pac`2 ∃c.Pac`2
%D ∃c.Pac`1
%D Pac`0 ∃c.Pac`0
%D @ 0 @ 1 => @ 0 @ 3 <=
%D @ 1 @ 2 |-> sl_ .plabel= l ♮ @ 1 @ 2 <-| sl^ .plabel= r 𝐬{BCC}
%D @ 2 @ 4 <= @ 3 @ 4 =>
%D ))
%D (( Rab`1 Rab`0
%D ∀b.Rab`2
%D ∀b.Rab`1 ∀b.Rab`0
%D @ 0 @ 1 <= @ 0 @ 2 => @ 1 @ 4 =>
%D @ 2 @ 3 |-> sl_ .plabel= l ♮ @ 2 @ 3 <-| sl^ .plabel= r 𝐬{BCC}
%D @ 3 @ 4 <=
%D ))
%D enddiagram
%
$$\diag{lawbcc1}$$
%D diagram lawbcc-std
%D 2Dx 100 +60
%D 2D 100 \H{f·\psi}{x·\phi} <--> \H{(f·\psi)Σx}{\phi}
%D 2D ^ ^v
%D 2D +20 | \H{f'·(\psiΣy)}{\phi}
%D 2D v ^
%D 2D +10 \H{\psi}{(x·\phi)Πf} |
%D 2D ^v v
%D 2D +20 \H{\psi}{y·(\phiΠf')} <-> \H{\psiΣy}{\phiΠf'}
%D 2D
%D (( \H{f·\psi}{x·\phi} \H{(f·\psi)Σx}{\phi}
%D \H{f'·(\psiΣy)}{\phi}
%D \H{\psi}{(x·\phi)Πf}
%D \H{\psi}{y·(\phiΠf')} \H{\psiΣy}{\phiΠf'}
%D @ 0 @ 1 <-> @ 0 @ 3 <->
%D @ 1 @ 2 -> sl_ .plabel= l ♮ @ 1 @ 2 <- sl^ .plabel= r 𝐬{BCC}
%D @ 2 @ 5 <->
%D @ 3 @ 4 -> sl_ .plabel= l ♮ @ 3 @ 4 <- sl^ .plabel= r 𝐬{BCC}
%D @ 4 @ 5 <->
%D ))
%D enddiagram
%D
$$\def\H#1#2{(#1\to#2)}
\diag{lawbcc-std}
$$
%D diagram lawbcc-dnc
%D 2Dx 100 +60
%D 2D 100 Pac|-Rab <---> ∃c.Pac|-Rab
%D 2D ^ v^
%D 2D +20 | {}∃c.Pac|-Rab
%D 2D v ^
%D 2D +10 Pac|-∀b.Rab{} |
%D 2D v^ v
%D 2D +20 Pac|-∀b.Rab <-> ∃c.Pac|-∀b.Rab
%D 2D
%D (( Pac|-Rab ∃c.Pac|-Rab
%D {}∃c.Pac|-Rab
%D Pac|-∀b.Rab{}
%D Pac|-∀b.Rab ∃c.Pac|-∀b.Rab
%D @ 0 @ 1 <-> @ 0 @ 3 <->
%D @ 1 @ 2 |-> sl_ .plabel= l ♮ @ 1 @ 2 <-| sl^ .plabel= r 𝐬{BCC}
%D @ 2 @ 5 <->
%D @ 3 @ 4 |-> sl_ .plabel= l ♮ @ 3 @ 4 <-| sl^ .plabel= r 𝐬{BCC}
%D @ 4 @ 5 <->
%D ))
%D enddiagram
%D
$$\diag{lawbcc-dnc}$$
\newpage
% --------------------
% «constrs-to-proofs-and-back» (to ".constrs-to-proofs-and-back")
% (s "From ``constructions'' to ``intuitionistic proofs'', and back" "constrs-to-proofs-and-back")
\myslide {From ``constructions'' to ``intuitionistic proofs'', and back} {constrs-to-proofs-and-back}
We have a notion of ``categorical construction''
and a notion of ``intuitionistic proof'';
neither of them are very clear now ---
but I will start with some examples,
and show how every ``categorical construction''
in a hyperdoctrine can be translated to an
``intuitionistic proof'', and how an
``intuitionistic proof'' in a certain
typed intuitionistic logic can be translated
to a ``categorical construction'' in a hyperdoctrine...
\msk
Only after seeing these two translations in detail
we will start to think about adding new constants,
axioms, operations and rules to our
``typed intuitionistic logic'', and how to add new
constants, operations, equalities, etc, to our
notion of hyperdoctrine.
\msk
Note: in this beginning all our categorical constructions
will look as if they were happening in Sub(Set)->Set ---
because at this moment that is the only hyperdoctrine we know ---
but the abstract diagrams that we will produce in the process
will later be seen to be appliable to every hyperdoctrine.
\msk
Similarly, all our intuitionistic proofs will look
as if they were just happening in a fragment of the full
language for sets and first-order predicates, but later
we will see that they will also apply to other ``languages''
and ``logics'', with ``models'' different from Sub(Set)->Set...
\msk
{\it But we need concrete examples to start with.}
\newpage
% --------------------
% «adj-functors-as-seq-rules» (to ".adj-functors-as-seq-rules")
% (hyp8p 26 "adj-functors-as-seq-rules")
% (hyp8 "adj-functors-as-seq-rules")
% (s "The adjunction functors as sequent rules" "adj-functors-as-seq-rules")
\myslide {The adjunction functors as sequent rules} {adj-functors-as-seq-rules}
%:
%:
%: P&Q <=== P P|-P' R|-R'
%: - <b| - ---------&Q ---------Q→
%: | | P&Q|-P'&Q Q→R|-Q→R'
%: v |#> v
%: R ===> Q→R ^andQ--ftr ^Qimp--ftr
%:
%: (P,Q) ==> P∨Q
%: - |b> -
%: | | P|-P' Q|-Q' R|-R' S|-S' T|-T'
%: v <#| v ------------∨ ---------------K ------------&
%: (R,R) <=== R P∨Q|-P'∨Q' (R|-R'),(R|-R') S&T|-S'&T'
%: - <b| -
%: | | ^or--ftr ^dbl--ftr ^and--ftr
%: v |#> v
%: (S,T) ==> S&T
%:
%: Pab ===> ∃b.Pab
%: - |b> -
%: | | Pab|-P'ab Qa|-Q'a Rab|-R'ab
%: v <#| v ---------------∃ -------W ---------------∀
%: Qa <====== Qa ∃b.Pab|-∃b.P'ab Qa|-Q'a ∀b.Rab|-∀b.R'ab
%: - <b| -
%: | | ^ex--ftr ^wkn--ftr ^fa--ftr
%: v |#> v
%: Rab ===> ∀b.Rab
%:
%: a,b|-----> a
%:
%: Pab ==> b=b'&Pab Pab|-P'ab Qabb'|-Q'abb'
%: - |b> - ------------------=& ---------(b':=b)
%: | | b=b'&Pab|-b=b'&Pab Qabb|-Q'abb
%: v <#| v
%: Qabb <== Qabb' ^=and--ftr ^smash--ftr
%: - <b| -
%: | | Rab|-R'ab
%: v |#> v ------------------=→
%: Rab ===> b=b'→Rab b=b'→Rab|-b=b'→R'ab
%:
%: a,b |--> a,b,b' ^=imp--ftr
%:
%:
%: Pa ==> ∃a.b=fa&Pb Pa|-P'a Qb|-Q'b
%: - |b> - -----------------------∃= ---------(b:=fa)
%: | | ∃a.b=fa&Pb|-∃a.b=fa&.Pb Qfa|-Q'fa
%: v <#| v
%: Qfa <====== Qb ^ex=--ftr ^ba--ftr
%: - <b| -
%: | | Ra|-R'a
%: v |#> v -----------------------∀=
%: Ra ===> ∀a.b=fa→Rb ∀a.b=fa→Ra|-∀a.b=fa→R'a
%:
%: a |------> b ^fa=--ftr
%:
\def\foooandimpftr{ \footwov { \ded{andQ--ftr} }{ \ded{Qimp--ftr} }}
\def\foooandorftr{ \foothreev { \ded{or--ftr} }{ \ded{dbl--ftr} }{ \ded{and--ftr} }}
\def\foooexfaftr{ \footwov { \ded{ex--ftr} }{ \ded{fa--ftr} }}
\def\foooexfaftr{ \foothreev { \ded{ex--ftr} }{ \ded{wkn--ftr} }{ \ded{fa--ftr} }}
\def\foooeqftr{ \foothreev { \ded{=and--ftr} }{ \ded{smash--ftr} }{ \ded{=imp--ftr} }}
\def\foooqeqftr{ \foothreev { \ded{ex=--ftr} }{ \ded{ba--ftr} }{ \ded{fa=--ftr} }}
$$\begin{array}{cc}
\cdiag{adj-cur-flsh} & \foooandimpftr \\ \\
\cdiag{adj-orand-flsh} & \foooandorftr \\ \\
\cdiag{adj-exfa-flsh} & \foooexfaftr \\
\end{array}
$$
\newpage
% --------------------
% «adj-functors-as-seq-rules-2» (to ".adj-functors-as-seq-rules-2")
% (s "The adjunction functors as sequent rules (2)" "adj-functors-as-seq-rules-2")
\myslide {The adjunction functors as sequent rules (2)} {adj-functors-as-seq-rules-2}
$$\begin{array}{cc}
\cdiag{adj-eq-flsh} & \foooeqftr \\\\
\cdiag{adj-qeq-flsh} & \foooqeqftr \\
\end{array}
$$
\newpage
% --------------------
% «adj-maps-as-seq-rules» (to ".adj-maps-as-seq-rules")
% (s "The adjunction maps as sequent rules" "adj-maps-as-seq-rules")
\myslide {The adjunction maps as sequent rules} {adj-maps-as-seq-rules}
\def\Cur{𝐫{Cur}}
\def\sh{\sharp}
\def\fl{\flat}
%D diagram adj-cur-flsh
%D 2Dx 100 +30
%D 2D 100 P&Q <=== P
%D 2D - <b| -
%D 2D | |
%D 2D v |#> v
%D 2D +30 R ===> Q→R
%D 2D
%D (( P&Q P R Q→R
%D @ 0 @ 1 <= @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D @ 0 @ 3 harrownodes nil 20 nil <-| sl^ .plabel= a \flat
%D @ 0 @ 3 harrownodes nil 20 nil |-> sl_ .plabel= b \sharp
%D ))
%D enddiagram
%D diagram adj-orand-flsh
%D 2Dx 100 +30
%D 2D 100 (P,Q) ==> P∨Q
%D 2D - |b> -
%D 2D | |
%D 2D v <#| v
%D 2D +30 (R,R) <=== R
%D 2D - <b| -
%D 2D | |
%D 2D v |#> v
%D 2D +30 (S,T) ==> S&T
%D 2D
%D (( (P,Q) P∨Q (R,R) R (S,T) S&T
%D @ 0 @ 1 =>
%D @ 0 @ 2 |-> @ 1 @ 3 |->
%D @ 2 @ 3 <=
%D @ 2 @ 4 |-> @ 3 @ 5 |->
%D @ 4 @ 5 =>
%D @ 0 @ 3 harrownodes nil 20 nil |-> sl^ .plabel= a \flat
%D @ 0 @ 3 harrownodes nil 20 nil <-| sl_ .plabel= b \sharp
%D @ 2 @ 5 harrownodes nil 20 nil <-| sl^ .plabel= a \flat
%D @ 2 @ 5 harrownodes nil 20 nil |-> sl_ .plabel= b \sharp
%D ))
%D enddiagram
%D diagram adj-exfa-flsh
%D 2Dx 100 +30
%D 2D 100 Pab ===> ∃b.Pab
%D 2D - |b> -
%D 2D | |
%D 2D v <#| v
%D 2D +30 Qa <====== Qa{}
%D 2D - <b| -
%D 2D | |
%D 2D v |#> v
%D 2D +30 Rab ===> ∀b.Rab
%D 2D
%D 2D +15 a,b |----> a
%D 2D
%D (( Pab ∃b.Pab Qa Qa{} Rab ∀b.Rab a,b a
%D @ 0 @ 1 =>
%D @ 0 @ 2 |-> @ 1 @ 3 |->
%D @ 2 @ 3 <=
%D @ 2 @ 4 |-> @ 3 @ 5 |->
%D @ 4 @ 5 =>
%D @ 0 @ 3 harrownodes nil 20 nil |-> sl^ .plabel= a \flat
%D @ 0 @ 3 harrownodes nil 20 nil <-| sl_ .plabel= b \sharp
%D @ 2 @ 5 harrownodes nil 20 nil <-| sl^ .plabel= a \flat
%D @ 2 @ 5 harrownodes nil 20 nil |-> sl_ .plabel= b \sharp
%D @ 6 @ 7 |->
%D ))
%D enddiagram
%D diagram adj-eq-flsh
%D 2Dx 100 +40
%D 2D 100 Pab ==> b=b'&Pab
%D 2D - |b> -
%D 2D | |
%D 2D v <#| v
%D 2D +30 Qabb <== Qabb'
%D 2D - <b| -
%D 2D | |
%D 2D v |#> v
%D 2D +30 Rab ===> b=b'→Rab
%D 2D
%D 2D +15 a,b |--> a,b,b'
%D 2D
%D (( Pab b=b'&Pab Qabb Qabb' Rab b=b'→Rab a,b a,b,b'
%D @ 0 @ 1 =>
%D @ 0 @ 2 |-> @ 1 @ 3 |->
%D @ 2 @ 3 <=
%D @ 2 @ 4 |-> @ 3 @ 5 |->
%D @ 4 @ 5 =>
%D @ 0 @ 3 harrownodes nil 20 nil |-> sl^ .plabel= a \flat
%D @ 0 @ 3 harrownodes nil 20 nil <-| sl_ .plabel= b \sharp
%D @ 2 @ 5 harrownodes nil 20 nil <-| sl^ .plabel= a \flat
%D @ 2 @ 5 harrownodes nil 20 nil |-> sl_ .plabel= b \sharp
%D @ 6 @ 7 |->
%D ))
%D enddiagram
%D diagram adj-qeq-flsh
%D 2Dx 100 +40
%D 2D 100 Pa ==> ∃a.b=fa&Pab
%D 2D - |b> -
%D 2D | |
%D 2D v <#| v
%D 2D +30 Qfa <==== Qb
%D 2D - <b| -
%D 2D | |
%D 2D v |#> v
%D 2D +30 Ra ===> ∀a.b=fa→Ra
%D 2D
%D 2D +15 a |------> b
%D 2D
%D (( Pa ∃a.b=fa&Pab Qfa Qb Ra ∀a.b=fa→Ra a b
%D @ 0 @ 1 =>
%D @ 0 @ 2 |-> @ 1 @ 3 |->
%D @ 2 @ 3 <=
%D @ 2 @ 4 |-> @ 3 @ 5 |->
%D @ 4 @ 5 =>
%D @ 0 @ 3 harrownodes nil 20 nil |-> sl^ .plabel= a \flat
%D @ 0 @ 3 harrownodes nil 20 nil <-| sl_ .plabel= b \sharp
%D @ 2 @ 5 harrownodes nil 20 nil <-| sl^ .plabel= a \flat
%D @ 2 @ 5 harrownodes nil 20 nil |-> sl_ .plabel= b \sharp
%D @ 6 @ 7 |->
%D ))
%D enddiagram
%: P [Q]^1 P&Q
%: --------&I ---&E_1
%: P&Q <=== P P&Q P&Q P
%: - <b| - ::: ---&E_2 :
%: | | R Q Q→R P&Q|-R P|-Q→R
%: v |#> v ---(→I) -------------→E ------\Cur^\sh ------\Cur^\fl
%: R ===> Q→R Q→R R P|-Q→R P&Q|-R
%:
%: ^cur-sh ^cur-fl ^cur--sh ^cur--fl
%:
%:
%: (P,Q) ==> P∨Q [P]^1 [Q]^1 P Q
%: - |b> - : : ---∨I_1 ---∨I_2
%: | | P∨Q R R P∨Q P∨Q P|-R Q|-R P∨Q|-R P∨Q|-R
%: v <#| v ---------------∨E : : ----------∨^\fl ------∨^\sh_1 ------∨^\sh_2
%: (R,R) <=== R R R R P∨Q|-R P|-R Q|-R
%:
%: ^or-fl ^or-sh1 ^or-sh2 ^or--fl ^or--sh1 ^or--sh2
%:
%: (R,R) <=== R R R R R
%: - <b| - : : : :
%: | | S T S&T S&T R|-S R|-T R|-S&T R|-S&T
%: v |#> v -----&I ---&E_1 ---&E_2 ----------∨^\sh ------∨^\fl_1 -----∨^\fl_2
%: (S,T) ==> S&T S&T S T T|-S&T R|-S R|-T
%:
%: ^and-sh ^and-fl1 ^and-fl2 ^and--sh ^and--fl1 ^and--fl2
%:
%: Pab ===> ∃b.Pab [Pab]^1 Pab
%: - |b> - : ------∃I
%: | | ∃b.Pab Qa ∃b.Pab Pab|-Qa ∃b.Pab|-Qa
%: v <#| v -----------∃E : ----------∃^\fl ----------∃^\sh
%: Qa <====== Qa Qa Qa ∃b.Pab|-Qa Pab|-Qa
%:
%: a,b|-----> a ^ex-fl ^ex-sh ^ex--fl ^ex--sh
%:
%: Qa <====== Qa [Qa]^1 Qa
%: - <b| - : :
%: | | Qa Rab b ∀b.Rab Qa|-Rab Qa|-∀b.Rab
%: v |#> v ---------∀I ---------∀E ----------∀^\sh ----------∀^\fl
%: Rab ===> ∀b.Rab ∀b.Rab Rab Qa|-∀b.Rab Qa|-Rab
%:
%: a,b|-----> a ^fa-sh ^fa-fl ^fa--sh ^fa--fl
%:
%: Pab ==> b=b'&Pab b=b'&Pab [b=b']^1 Pab
%: - |b> - -------&E_2 ------------
%: | | b=b'&Pab Pab b=b'&Pab
%: v <#| v -------&E_1 : ---=I :
%: Qbb <=== Qbb' b=b' Qabb b=b Qabb' Pab|-Qabb b=b'&Pab|-Qabb'
%: - <b| - ---------------=E ---------------b':=b;1 ---------=&^\fl ---------=&^\sh
%: | | Qabb' Qabb b=b'&Pab|-Qabb' Pab|-Qabb
%: v |#> v
%: Rab ==> b=b'→Rab ^eq-fl ^eq-sh ^eq--fl ^eq--sh
%:
%: a,b |--> a,b,b' [b=b']^1 Qabb' [Qabb']^1
%: ---------------? :
%: Qabb [b=b']^1 b=b'→Rab
%: : ---=I ------------------→E
%: Rab b=b Qabb Rab Qabb|-Rab Qabb'|-b=b'→Rab
%: --------→I;1 ---------------------b':=b;1 ---------=→^\sh ---------=→^\fl
%: b=b'→Rab Rab Qabb'|-b=b'→Rab Qabb|-Rab
%:
%: ^eqi-sh ^eqi-fl ^eqi--sh ^eqi--fl
%:
%: Pa ==> ∃a.b=fa&Pab Pa|-Qfa ∃a.b=fa&Pab|-Qb
%: - |b> - ---------∃=^\fl ---------∃=^\sh
%: | | ∃a.b=fa&Pab|-Qb Pa|-Qfa
%: v <#| v
%: Qfa <====== Qb ^ex=--fl ^ex=--sh
%: - <b| -
%: | | Qfa|-Ra Qb|-∀a.b=fa→Ra
%: v |#> v ---------=→^\sh ---------=→^\fl
%: Ra ===> ∀a.b=fa→Ra Qb|-∀a.b=fa→Ra Qfa|-Ra
%:
%: a |------> b ^fa=--sh ^fa=--fl
\def\foootwocur{ \footwo { \ded{cur--sh} }{ \ded{cur--fl} }}
\def\fooofourorand{ \fooFour{ \ded{or--fl} }{ \ded{or--sh1} \quad \ded{or--sh2} }
{ \ded{and--sh} }{ \ded{and--fl1} \quad \ded{and--fl2} }}
\def\fooofourexfa{ \fooFour{ \ded{ex--fl} }{ \ded{ex--sh} }
{ \ded{fa--sh} }{ \ded{fa--fl} }}
\def\fooofoureq{ \foofour{ \ded{eq--fl} }{ \ded{eq--sh} }
{ \ded{eqi--sh} }{ \ded{eqi--fl} }}
\def\fooofourqeq{ \foofour{ \ded{ex=--fl} }{ \ded{ex=--sh} }
{ \ded{fa=--sh} }{ \ded{fa=--fl} }}
\def\footwocur{ \footwo { \ded{cur-sh} }{ \ded{cur-fl} }}
\def\foofourorand{ \fooFour{ \ded{or-fl} }{ \ded{or-sh1} \quad \ded{or-sh2} }
{ \ded{and-sh} }{ \ded{and-fl1} \quad \ded{and-fl2} }}
\def\foofourexfa{ \fooFour{ \ded{ex-fl} }{ \ded{ex-sh} }
{ \ded{fa-sh} }{ \ded{fa-fl} }}
\def\foofoureq{ \foofour{ \ded{eq-fl} }{ \ded{eq-sh} }
{ \ded{eqi-sh} }{ \ded{eqi-fl} }}
$$\begin{array}{cc}
\cdiag{adj-cur-flsh} & \foootwocur \\ \\
\cdiag{adj-orand-flsh} & \fooofourorand \\ \\
\cdiag{adj-exfa-flsh} & \fooofourexfa \\
\end{array}
$$
\newpage
% --------------------
% «adj-maps-as-seq-rules-2» (to ".adj-maps-as-seq-rules-2")
% (s "The adjunction maps as sequent rules (2)" "adj-maps-as-seq-rules-2")
\myslide {The adjunction maps as sequent rules (2)} {adj-maps-as-seq-rules-2}
$$\begin{array}{cc}
\cdiag{adj-eq-flsh} & \fooofoureq \\ \\
\cdiag{adj-qeq-flsh} & \fooofourqeq \\
\end{array}
$$
\newpage
% --------------------
% «adj-functors-as-ND-proofs» (to ".adj-functors-as-ND-proofs")
% (hyp8p 28 "adj-functors-as-ND-proofs")
% (hyp8 "adj-functors-as-ND-proofs")
% (s "The adjunction functors as ND proofs" "adj-functors-as-ND-proofs")
\myslide {The adjunction functors as ND proofs} {adj-functors-as-ND-proofs}
%: [Q]^1 Q→R P&Q
%: ----------→E ---&E_1
%: P&Q <=== P R P P&Q
%: - <b| - : : ---&E_2
%: | | R' P' Q
%: v |#> v ----→I;1 ----------&I
%: R ===> Q→R Q→R' P'&Q
%:
%: ^Qimp-ftr ^andQ-ftr
%:
%: (P,Q) ==> P∨Q [P]^1 [Q]^1 S&T S&T
%: - |b> - : : ---&E_1 ---&E_2
%: | | P' Q' S T
%: v <#| v -----∨I_1 ----∨I_2 : :
%: (R,R) <=== R P∨Q P'∨Q' P'∨Q' S' T'
%: - <b| - ---------------------∨E -----------&I
%: | | P'∨Q' S'&T'
%: v |#> v
%: (S,T) ==> S&T ^or-ftr ^and-ftr
%:
%: Pab ===> ∃b.Pab
%: - |b> - [Pab]^1 [b]^1 ∀b.Rab
%: | | : -------------∀E
%: v <#| v P'ab Rab
%: Qa <====== Qa -------∃I :
%: - <b| - ∃b.Pab ∃b.P'ab R'ab
%: | | ----------------∃E -------∀I;1
%: v |#> v ∃b.P'ab ∀b.R'ab
%: Rab ===> ∀b.Rab
%: ^ex-ftr ^fa-ftr
%: a,b|-----> a
%:
\def\footwocurftr{ \footwo { \ded{andQ-ftr} }{ \ded{Qimp-ftr} }}
\def\footwoorandftr{ \footwo { \ded{or-ftr} }{ \ded{and-ftr} }}
\def\footwoexfaftr{ \footwo { \ded{ex-ftr} }{ \ded{fa-ftr} }}
$$\begin{array}{cc}
\cdiag{adj-cur-flsh} & \footwocurftr \\ \\
\cdiag{adj-orand-flsh} & \footwoorandftr \\ \\
\cdiag{adj-exfa-flsh} & \footwoexfaftr \\
% \cdiag{adj-eq-flsh} & \footwoeqftr \\
\end{array}
$$
\newpage
% --------------------
% «adj-functors-as-ND-proofs-2» (to ".adj-functors-as-ND-proofs-2")
% (hyp8p 29 "adj-functors-as-ND-proofs-2")
% (hyp8 "adj-functors-as-ND-proofs-2")
% (s "The adjunction functors as ND proofs (2)" "adj-functors-as-ND-proofs-2")
\myslide {The adjunction functors as ND proofs (2)} {adj-functors-as-ND-proofs-2}
%: b=b'&Pab
%: -------&E_2
%: b=b'&Pab Pab [Qabb']^1
%: -------&E_1 : :
%: b=b' P'ab Qabb Q'abb'
%: ---------------? ----------b':=b
%: Pab ==> b=b'&Pab b=b'&P'ab Q'abb
%: - |b> -
%: | | ^=and-ftr ^smash-ftr
%: v <#| v
%: Qabb <== Qabb' [b=b']^1 b=b'→Rab
%: - <b| - ------------------→E
%: | | Rab
%: v |#> v :
%: Rab ===> b=b'→Rab R'ab
%: --------→I;1
%: a,b |--> a,b,b' b=b'→Rab
%:
%: ^=imp-ftr
%:
%: [fa=b&Pa]^1 ∀a.fa=b→Ra
%: -----------&E_2 ----------
%: Pa ==> ∃a.b=fa&Pab [fa=b&Pa]^1 Pa [fa=b]^1 fa=b→Ra
%: - |b> - -----------&E_1 : ------------------
%: | | fa=b P'a Ra
%: v <#| v -----------------&I :
%: Qfa <====== Qb fa=b&P'a R'a
%: - <b| - -----------∃I --------1
%: | | ∃a.fa=b&Pa ∃a.fa=b&P'a fa=b→R'a
%: v |#> v ------------------------∃E;1 -----------
%: Ra ===> ∀a.b=fa→Ra ∃a.fa=b&P'a ∀a.fa=b→R'a
%:
%: a |------> b ^ex=-ftr ^fa=-ftr
%:
\def\footwoeqftr{ \footwo { \ded{=and-ftr} }{ \ded{=imp-ftr} }}
\def\footwoveqftr{ \footwov { \ded{=and-ftr} }{ \ded{=imp-ftr} }}
\def\foofoureqftr{ \foofour { \ded{=and-ftr} }{ \ded{smash-ftr} }
{ \ded{=imp-ftr} }{ }}
\def\footwovqeqftr{ \footwov { \ded{ex=-ftr} }{ \ded{fa=-ftr} }}
$$\begin{array}{cc}
\cdiag{adj-eq-flsh} & \footwoveqftr \\ \\
\cdiag{adj-qeq-flsh} & \footwovqeqftr \\
\end{array}
$$
\newpage
% --------------------
% «adj-maps-as-ND-proofs» (to ".adj-maps-as-ND-proofs")
% (s "The adjunction maps as ND proofs" "adj-maps-as-ND-proofs")
\myslide {The adjunction maps as ND proofs} {adj-maps-as-ND-proofs}
$$\begin{array}{cc}
\cdiag{adj-cur-flsh} & \footwocur \\ \\
\cdiag{adj-orand-flsh} & \foofourorand \\ \\
\cdiag{adj-exfa-flsh} & \foofourexfa \\
\end{array}
$$
\newpage
% --------------------
% «adj-maps-as-ND-proofs-2» (to ".adj-maps-as-ND-proofs-2")
% (s "The adjunction maps as ND proofs (2)" "adj-maps-as-ND-proofs-2")
\myslide {The adjunction maps as ND proofs (2)} {adj-maps-as-ND-proofs-2}
\msk
$\diag{adj-eq-flsh}$
$$\foofoureq$$
\newpage
% --------------------
% «adj-maps-as-ND-proofs-3» (to ".adj-maps-as-ND-proofs-3")
% (s "The adjunction maps as ND proofs (3)" "adj-maps-as-ND-proofs-3")
\myslide {The adjunction maps as ND proofs (3)} {adj-maps-as-ND-proofs-3}
\msk
$\diag{adj-qeq-flsh}$
%:
%: [b=fa]^1 Pa
%: -------------
%: [b=fa&Pa]^1 b=fa&Pa
%: ----------- ----------
%: [b=fa&Pa]^1 Pa ∃a.b=fa&Pa
%: ----------- :: ::
%: b=fa Qfa [b=fa]^1 Qb
%: ---------------- ----- -------------
%: ∃a.b=fa&Pa Qb fa=fa Qfa
%: ------------------------1 ----------------
%: Qb Qfa
%:
%: ^gen-exand-sharp ^gen-exand-flat
%:
%: [Qb]^1
%: ::
%: [fa=b]^1 Qb [Qfa']^2 ∀a.fa=b→Ra
%: ------------- ---------------------1
%: Qfa ∀a.fa=fa'→Ra
%: :: ------------
%: Ra Qfa fa=fa→Ra
%: -------1 ----- ----------------2
%: fa=b→Ra fa=fa fa=fa→Ra
%: ---------- ------------------
%: ∀a.fa=b→Ra Ra
%:
%: ^gen-eximp-flat ^gen-eximp-sharp
%:
$$\ded{gen-exand-sharp} \quad \ded{gen-exand-flat}$$
$$\ded{gen-eximp-flat} \qquad \ded{gen-eximp-sharp}$$
\newpage
% --------------------
% «frob-maps-as-ND-proofs» (to ".frob-maps-as-ND-proofs")
% (s "The Frobenius maps as ND proofs" "frob-maps-as-ND-proofs")
\myslide {The Frobenius maps as ND proofs} {frob-maps-as-ND-proofs}
The preservations of $⊤, ⊥, \&, ∨, →$ are all
trivially true intuitionistically, as they are all
of the form $\aa \vdash \aa$...
\msk
Same for Beck-Chevalley.
\msk
The $♮$ arrows whose inverses are the Frobenius maps
can be constructed from operations whose translations
to Intuitionistic Logic we have already seen.
%D diagram frob-maps
%D 2Dx 100 +80 +30 +50
%D 2D 100 AL <=====> AR al <=====> ar
%D 2D
%D 2D +20 al <=====> ar al <=====> ar
%D 2D
%D 2D +30 BL <=====> BR bl <=====> br
%D 2D
%D 2D +20 bl <=====> br bl <=====> br
%D 2D
%D 2D +30 CL <=====> CR cl <=====> cr
%D 2D
%D 2D +20 cl <=====> cr cl <=====> cr
%D 2D
%D (( AL .tex= ∃_π(P&π^*Q) AR .tex= (∃_πP)&Q
%D al .tex= ∃b.(Pab&Qa) ar .tex= (∃b.Pab)&Qa
%D @ 0 @ 1 -> sl^ .plabel= a ♮ @ 0 @ 1 <- sl_ .plabel= b 𝐬{Frob}∃
%D @ 2 @ 3 |-> sl^ .plabel= a ♮ @ 2 @ 3 <-| sl_ .plabel= b 𝐬{Frob}∃
%D ))
%D (( BL .tex= \Eq_δ(P&δ^*Q) BR .tex= (\Eq_δP)&Q
%D bl .tex= b=b'&(Pabb&Qab) br .tex= (b=b'&Pabb)&Qab
%D @ 0 @ 1 -> sl^ .plabel= a ♮ @ 0 @ 1 <- sl_ .plabel= b 𝐬{Frob}=
%D @ 2 @ 3 |-> sl^ .plabel= a ♮ @ 2 @ 3 <-| sl_ .plabel= b 𝐬{Frob}=
%D ))
%D (( CL .tex= \ExEq_f(P&f^*Q) CR .tex= (\ExEq_fP)&Q
%D cl .tex= ∃a.b=fa&(Pa&Qfa) cr .tex= (∃a.b=fa&Pa)&Qb
%D @ 0 @ 1 -> sl^ .plabel= a ♮ @ 0 @ 1 <- sl_ .plabel= b 𝐬{Frob}∃=
%D @ 2 @ 3 |-> sl^ .plabel= a ♮ @ 2 @ 3 <-| sl_ .plabel= b 𝐬{Frob}∃=
%D ))
%D enddiagram
%D
$$\diag{frob-maps}$$
\msk
We need to show that the Frobenius maps
``hold intuitionistically''.
\msk
Here is a ND proof for the first case:
(the other cases are similar - and the trees are big)
%: (∃b.Pab)&Qa
%: -----------&E_2
%: [Pab]^1 Qa
%: ---------------&I
%: (∃b.Pab)&Qa Pab&Qa
%: -----------&E_1 -----------∃I
%: ∃b.Pab ∃b.(Pab&Qa)
%: ------------------------------∃E;1
%: ∃b.(Pab&Qa)
%:
%: ^frob-ex-ND
%:
$$\ded{frob-ex-ND}$$
\newpage
% --------------------
% «frob-for-equality-2» (to ".frob-for-equality-2")
% (s "Frobenius for equality (2)" "frob-for-equality-2")
\myslide {Frobenius for equality (2)} {frob-for-equality-2}
(Now we will start to see consequences of the structure)
\msk
If we have $\Eq⊤$ and Frobenius, then we have $\Eq P$:
%D diagram EqTP-std
%D 2Dx 100 +50 +30 +30 +50
%D 2D 100 a ============> b
%D 2D ^ --> ^
%D 2D | / |
%D 2D - - -
%D 2D +20 c ====> d <===> e
%D 2D ^ ^ - -
%D 2D | | \ |
%D 2D v | --> v
%D 2D +20 f <=====|====== g <=== h
%D 2D ^ \\ |
%D 2D | \\ |
%D 2D | \\ v
%D 2D +20 | \> i
%D 2D | ^
%D 2D | |
%D 2D v v
%D 2D +20 j ====> k
%D 2D
%D 2D +20 a,b |---> a,b,b' |--> a,b{}
%D 2D
%D (( a .tex= ⊤ b .tex= \Eq⊤
%D c .tex= ⊤&δ^*π^*P d .tex= \Eq(⊤&δ^*π^*P) e .tex= \Eq⊤&π^*P
%D f .tex= δ^*π^*P g .tex= π^*P h .tex= P
%D i .tex= \Eq(δ^*π^*P)
%D j .tex= P k .tex= \Eq"P
%D a,b .tex= A×B a,b,b' .tex= A×B×B a,b{} .tex= A×B
%D ))
%D (( a .tex= 1_X b .tex= 1_XΣ\ang{X,f}
%D c .tex= \phi'∧1_X d .tex= (\phi'∧1_X)Σ\phi'∧1_X e .tex= π_X·\phi∧1_XΣ\ang{X,f}
%D f .tex= \phi' g .tex= π_X·\phi h .tex= \phi
%D i .tex= \phi'Σ\ang{X,f}
%D j .tex= \phi k .tex= \phiΣ\ang{X,f}
%D a,b .tex= X a,b,b' .tex= X×Y a,b{} .tex= X
%D ))
%D (( a b |-> c a -> d b -> e b ->
%D c d |-> d e -> sl^ .plabel= a ♮ d e <- sl_ .plabel= b 𝐬{Frob}
%D c f <-> d i <-> d g -> e g ->
%D f g <-| g h <-|
%D f j <-> f i |-> i k <-> j k |->
%D ))
%D (( a,b a,b,b' -> .plabel= a δ a,b,b' a,b{} -> .plabel= a π
%D ))
%D enddiagram
%D diagram EqTP-lawvere67
%D 2Dx 100 +50 +35 +35 +50
%D 2D 100 a ============> b
%D 2D ^ --> ^
%D 2D | / |
%D 2D - - -
%D 2D +20 c ====> d <===> e
%D 2D ^ ^ - -
%D 2D | | \ |
%D 2D v | --> v
%D 2D +20 f <=====|====== g <=== h
%D 2D ^ \\ |
%D 2D | \\ |
%D 2D | \\ v
%D 2D +20 | \> i
%D 2D | ^
%D 2D | |
%D 2D v v
%D 2D +20 j ====> k
%D 2D
%D 2D +20 a,b |---> a,b,b' |--> a,b{}
%D 2D
%D (( a .tex= 1_X b .tex= 1_XΣ\ang{X,f}
%D c .tex= \phi'∧1_X d .tex= (\phi'∧1_X)Σ\phi'∧1_X e .tex= π_X·\phi∧1_XΣ\ang{X,f}
%D f .tex= \phi' g .tex= π_X·\phi h .tex= \phi
%D i .tex= \phi'Σ\ang{X,f}
%D j .tex= \phi k .tex= \phiΣ\ang{X,f}
%D a,b .tex= X a,b,b' .tex= X×Y a,b{} .tex= X
%D ))
%D (( a b |-> c a -> d b -> e b ->
%D c d |-> d e -> sl^ .plabel= a ♮ d e <- sl_ .plabel= b 𝐬{Frob}
%D c f <-> d i <-> d g -> e g ->
%D f g <-| g h <-|
%D f j <-> f i |-> i k <-> j k |->
%D ))
%D (( a,b a,b,b' -> .plabel= a \ang{X,f} a,b,b' a,b{} -> .plabel= a π_X
%D ))
%D enddiagram
%D diagram EqTP-dnc
%D 2Dx 100 +50 +30 +30 +50
%D 2D 100 a ============> b
%D 2D ^ --> ^
%D 2D | / |
%D 2D - - -
%D 2D +20 c ====> d <===> e
%D 2D ^ ^ - -
%D 2D | | \ |
%D 2D v | --> v
%D 2D +20 f <=====|====== g <=== h
%D 2D ^ \\ |
%D 2D | \\ |
%D 2D | \\ v
%D 2D +20 | \> i
%D 2D | ^
%D 2D | |
%D 2D v v
%D 2D +20 j ====> k
%D 2D
%D 2D +20 a,b |---> a,b,b' |--> a,b{}
%D (( a .tex= ⊤ b .tex= b=b'&⊤
%D c .tex= ⊤&P d .tex= b=b'&(⊤&P) e .tex= (b=b'&⊤)&P
%D f .tex= P g .tex= P h .tex= P
%D i .tex= b=b'&P
%D j .tex= P k .tex= b=b'&P
%D ))
%D (( a b => c a |-> d b |-> e b |->
%D c d => d e |-> sl^ .plabel= a ♮ d e <-| sl_ .plabel= b 𝐬{Frob}
%D c f <-> d i <-> d g |-> e g |->
%D f g <= g h <=
%D f j <-> f i => i k <-> j k =>
%D ))
%D (( a,b a,b,b' |-> a,b,b' a,b{} |->
%D ))
%D enddiagram
% $$\diag{EqTP-std}$$
$$\diag{EqTP-lawvere67}$$
$$\diag{EqTP-dnc}$$
\bsk
From now on we will usually write ``$b{=}b'\&⊤$'' as just ``$b{=}b'$''.
Frobenius for equality implies that the four obvious definitions
for $b{=}b'\&P$ are isomorphic.
\newpage
% --------------------
% «dep-eq-from-simple-eq» (to ".dep-eq-from-simple-eq")
% (s "Dependent equality from simple equality" "dep-eq-from-simple-eq")
\myslide {Dependent equality from simple equality} {dep-eq-from-simple-eq}
%D diagram bcc-dep-T-std
%D 2Dx 100 +45 +55 +45
%D 2D 100 B0 <==> B0' <============= B1
%D 2D -\\ - -\\
%D 2D | \\ | <--| | \\
%D 2D v \\ v v \\
%D 2D +20 B2 <\\> B2' <============= B3 \\
%D 2D /\ \/ /\ \/
%D 2D +15 \\ B4 \\ B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +20 B6 <===================== B7
%D 2D
%D 2D +10 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +35 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= ⊤ B0' .tex= π_2^*⊤ B1 .tex= ⊤
%D B2 .tex= δ^*π_{23}^*\Eq⊤ B2' .tex= π_2^*δ^*\Eq⊤ B3 .tex= δ^*\Eq⊤
%D B4 .tex= \Eq_{δ'}⊤_{A×B} B5 .tex= \Eq⊤
%D B6 .tex= π_{23}^*\Eq_{δ}⊤_B B7 .tex= \Eq⊤
%D B0 B0' <- sl^ .plabel= a ♮ B0 B0' -> sl_ .plabel= b 𝐬P⊤
%D B0 B2 -> B0' B2' -> B2 B2' <->
%D B1 B3 -> B0' B1 <-| B2' B3 <-|
%D B0 B4 |-> B1 B5 |->
%D B2 B6 <-| B3 B7 <-|
%D B6 B7 <-| B5 B7 -> .plabel= r \id
%D B4 B6 -> sl_ .plabel= l ♮ B4 B6 <- sl^ .plabel= r 𝐬{BCC}∃
%D B0' B2' midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 16 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= A×B b1 .tex= B b2 .tex= A×B×B b3 .tex= B×B
%D b0 b1 -> .plabel= b π_2
%D b0 b2 -> .plabel= l δ'
%D b1 b3 -> .plabel= r δ
%D b2 b3 -> .plabel= b π_{23}
%D b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-dep-T-std}$$
%D diagram bcc-dep-T-dnc
%D 2Dx 100 +45 +55 +45
%D 2D 100 B0 <==> B0' <============= B1
%D 2D -\\ - -\\
%D 2D | \\ | <--| | \\
%D 2D v \\ v v \\
%D 2D +20 B2 <\\> B2' <============= B3 \\
%D 2D /\ \/ /\ \/
%D 2D +15 \\ B4 \\ B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +20 B6 <===================== B7
%D 2D
%D 2D +10 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +35 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= ⊤ B0' .tex= ⊤ B1 .tex= ⊤
%D B2 .tex= b=b B2' .tex= b=b B3 .tex= b=b
%D B4 .tex= b=b' B5 .tex= b=b'
%D B6 .tex= b=b' B7 .tex= b=b'
%D B0 B0' <-| sl^ .plabel= a ♮ B0 B0' |-> sl_ .plabel= b 𝐬P⊤
%D B0 B2 |-> B0' B2' |-> B2 B2' <->
%D B1 B3 |-> B0' B1 <= B2' B3 <=
%D B0 B4 => B1 B5 =>
%D B2 B6 <= B3 B7 <=
%D B6 B7 <= B5 B7 |-> .plabel= r \id
%D B4 B6 |-> sl_ .plabel= l ♮ B4 B6 <-| sl^ .plabel= r 𝐬{BCC}∃
%D B0' B2' midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a,b b1 .tex= b b2 .tex= a,b,b' b3 .tex= b,b'
%D b0 b1 |-> b0 b2 |-> b1 b3 |-> b2 b3 |->
%D b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-dep-T-dnc}$$
\newpage
% --------------------
% «eq-is-transitive» (to ".eq-is-transitive")
% (s "Transitivity of equality" "eq-is-transitive")
\myslide {Transitivity of equality} {eq-is-transitive}
%D diagram eqtransitivity-1
%D 2Dx 100 +40 +25 +40 +20 +35 +20 +35
%D 2D 100 A0 a0
%D 2D - ==> - ==>
%D 2D +20 | A1 | a1
%D 2D | - | -
%D 2D v | v |
%D 2D +20 A4 | A6 a4 | a6
%D 2D <=== v ==> <=== v ==>
%D 2D +20 A5 <========= A7 a5 <========= a7
%D 2D
%D 2D +15 B4 B6 b4 b6
%D 2D |-> |-> |-> |->
%D 2D +20 B5 |--------> B7 b5 |--------> b7
%D 2D
%D 2D +20 a0
%D 2D - ==>
%D 2D +20 | a1
%D 2D | -
%D 2D v |
%D 2D +20 a4 | a6
%D 2D <=== v ==>
%D 2D +20 a5 <========= a7
%D 2D
%D 2D +15 b4 b6
%D 2D |-> |->
%D 2D +20 b5 |--------> b7
%D 2D
%D (( A0 .tex= δ'^*π_{24}^*\Eq_δ⊤ A1 .tex= \Eq_{δ'}δ'^*π_{24}^*\Eq_δ⊤
%D A4 .tex= δ'^*π_{24}^*\Eq_δ⊤ A5 .tex= π_{24}^*\Eq_δ⊤
%D A6 .tex= ⊤ A7 .tex= \Eq_δ⊤
%D A0 A1 |-> A0 A4 -> .plabel= l \id A1 A5 -> A4 A5 <-| A6 A7 |-> A5 A7 <-|
%D A0 A4 midpoint A1 A5 midpoint dharrownodes nil 20 nil |->
%D ))
%D (( B4 .tex= (A×B)×B B5 .tex= ((A×B)×B)×B
%D B6 .tex= A×B B7 .tex= (A×B)×B
%D B4 B5 -> .PLABEL= _(0.35) δ'
%D B6 B7 -> .PLABEL= ^(0.5) δ
%D B5 B7 -> .plabel= b π_{24}
%D ))
%D (( a0 .tex= b=b' a1 .tex= b'=b''&b=b'
%D a4 .tex= b=b' a5 .tex= b=b''
%D a6 .tex= ⊤ a7 .tex= b=b''
%D a0 a1 => a0 a4 |-> .plabel= l \id a1 a5 |-> a4 a5 <= a6 a7 => a5 a7 <=
%D a0 a4 midpoint a1 a5 midpoint dharrownodes nil 20 nil |->
%D ))
%D (( b4 .tex= (a,b),b' b5 .tex= ((a,b),b'),b''
%D b6 .tex= a,b b7 .tex= (a,b),b''
%D b4 b5 |-> .PLABEL= _(0.35) b'':=b'\phantom{,}
%D b6 b7 |-> .PLABEL= ^(0.5) b'':=b
%D b5 b7 |->
%D ))
%D enddiagram
%D
\msk
$\diag{eqtransitivity-1}$
\newpage
% --------------------
% «hyp-subst-quant-refl» (to ".hyp-subst-quant-refl")
% (hyp8p 37 "hyp-subst-quant-refl")
% (hyp8 "hyp-subst-quant-refl")
% (s "Hyperdoctrines: substitution, quantifiers, reflexivity" "hyp-subst-quant-refl")
\myslide {Hyperdoctrines: substitution, quantifiers, reflexivity} {hyp-subst-quant-refl}
%D diagram Hyp-subst
%D 2Dx 100 +12 +50 +12
%D 2D
%D 2D 100 P <============ P{}
%D 2D - -
%D 2D | <-| |
%D 2D v v
%D 2D +30 Q <============ Q{}
%D 2D
%D 2D +20 a,c |---------> b,c
%D 2D +5 /\ /\
%D 2D || ||
%D 2D +10 a |-----------> b
%D 2D
%D (( P .tex= \s[a,c|P] P{} .tex= \s[b,c|P]
%D Q .tex= \s[b,c|Q] Q{} .tex= \s[b,c|Q]
%D @ 0 @ 1 <= sl_ @ 0 @ 1 |-> sl^ .plabel= a {◻}
%D @ 0 @ 2 |-> .plabel= l a,c;P|-Q
%D @ 1 @ 3 |-> .plabel= r b,c;P|-Q
%D @ 0 @ 3 harrownodes nil 20 nil <-|
%D @ 2 @ 3 <= sl_ @ 2 @ 3 |-> sl^ .plabel= a {◻}
%D
%D ))
%D (( a,c b,c a b
%D @ 0 @ 1 |-> # .plabel= a b:=b[a]
%D @ 0 @ 2 <= @ 1 @ 3 <=
%D @ 2 @ 3 |-> .plabel= b a|-b
%D ))
%D enddiagram
%D diagram Hyp-FaI
%D 2Dx 100 +10 +40 +10
%D 2D
%D 2D 100 P <============ P{}
%D 2D - -
%D 2D | |-> |
%D 2D v v
%D 2D +30 Q ============> ∀b.Q
%D 2D
%D 2D +20 a,b |----------> a
%D 2D
%D (( P .tex= \s[a,c|P] P{} .tex= \s[b,c|P]
%D Q .tex= \s[b,c|Q] ∀b.Q .tex= \s[b,c|∀b.Q]
%D @ 0 @ 1 <= sl_ @ 0 @ 1 |-> sl^ .plabel= a {◻}
%D @ 0 @ 2 |-> .plabel= l a,b;P|-Q
%D @ 1 @ 3 |-> .plabel= r a;P|-∀b.Q
%D @ 0 @ 3 harrownodes nil 20 nil |->
%D @ 2 @ 3 =>
%D ))
%D (( a,b a
%D @ 0 @ 1 |->
%D ))
%D enddiagram
%D diagram Hyp-FaE
%D 2Dx 100 +40 +40
%D 2D 100 {}Q <========== Q <======== Q{}
%D 2D - - -
%D 2D | <-| | <-| |
%D 2D v v v
%D 2D +30 {}R <========== R ========> ∀b.R
%D 2D
%D 2D +20 {}a |--------> a,b |-------> a{}
%D 2D
%D (( {}Q .tex= \s[a|P] Q .tex= \s[a,b|P] Q{} .tex= \s[a|P]
%D {}R .tex= \s[a|Q] R .tex= \s[a,b|Q] ∀b.R .tex= \s[a|∀b.Q]
%D @ 0 @ 1 <= sl_ @ 0 @ 1 |-> sl^ .plabel= a {◻}
%D @ 1 @ 2 <= sl_ @ 1 @ 2 |-> sl^ .plabel= a {◻}
%D @ 0 @ 3 |-> .plabel= l a;Q|-R
%D @ 1 @ 4 |->
%D @ 2 @ 5 |-> .plabel= r a;Q|-∀b.R
%D @ 0 @ 4 harrownodes nil 20 nil <-|
%D @ 1 @ 5 harrownodes nil 20 nil <-|
%D @ 3 @ 4 <= sl_ @ 3 @ 4 |-> sl^ .plabel= a {◻}
%D @ 4 @ 5 =>
%D ))
%D (( {}a a,b |-> .plabel= a a|-b
%D a,b a{} |->
%D ))
%D enddiagram
%D diagram Hyp-ExE
%D 2Dx 100 +10 +40 +10
%D 2D
%D 2D 100 P ============> ∃b.P
%D 2D - -
%D 2D | |-> |
%D 2D v v
%D 2D +30 Q <============ Q{}
%D 2D
%D 2D +20 a,b |----------> a
%D 2D
%D (( P .tex= \s[a,b|P] ∃b.P .tex= \s[a|∃b.P]
%D Q .tex= \s[b,c|Q] Q{} .tex= \s[a,b|Q]
%D @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{◻}
%D @ 0 @ 2 |-> .plabel= l a,b;P|-Q
%D @ 1 @ 3 |-> .plabel= r a;∃b.P|-Q
%D @ 0 @ 3 harrownodes nil 20 nil |->
%D @ 2 @ 3 <= sl_ @ 2 @ 3 |-> sl^ .plabel= a {◻}
%D ))
%D (( a,b a
%D @ 0 @ 1 |->
%D ))
%D enddiagram
%D diagram Hyp-ExI
%D 2Dx 100 +40 +40
%D 2D 100 {}P <========== P =======> {∃b.P}
%D 2D - - -
%D 2D | <-| | <-| | id
%D 2D v v v
%D 2D +30 {}∃b.P <====== ∃b.P <====== ∃b.P{}
%D 2D
%D 2D +20 {}a |--------> a,b |-------> a{}
%D 2D
%D (( {}P .tex= \s[a|P] P .tex= \s[a,b|P] {∃b.P} .tex= \s[a|∃b.P]
%D {}∃b.P .tex= \s[a|∃b.P] ∃b.P .tex= \s[a,b|∃b.P] ∃b.P{} .tex= \s[a|∃b.P]
%D @ 0 @ 1 <= sl_ @ 0 @ 1 |-> sl^ .plabel= a {◻}
%D @ 1 @ 2 => sl_ @ 1 @ 2 |-> sl^ .plabel= a \co{◻}
%D @ 0 @ 3 |-> .plabel= l a;P|-∃b.P
%D @ 1 @ 4 |->
%D @ 2 @ 5 |-> .plabel= r \id
%D @ 0 @ 4 harrownodes nil 20 nil <-|
%D @ 1 @ 5 harrownodes nil 20 nil <-|
%D @ 3 @ 4 <= sl_ @ 3 @ 4 |-> sl^ .plabel= a {◻}
%D @ 4 @ 5 <= sl_ @ 4 @ 5 |-> sl^ .plabel= a {◻}
%D ))
%D (( {}a a,b |-> .plabel= a a|-b
%D a,b a{} |->
%D ))
%D enddiagram
The substitution rule:
\msk
$\diag{Hyp-subst}$
\bsk
The `($∀$I)' and `($∀$E)' rules:
\msk
$\diag{Hyp-FaI} \qquad \diag{Hyp-FaE}$
\bsk
The `($∃$E)' and `($∃$I)' rules:
\msk
$\diag{Hyp-ExE} \qquad \diag{Hyp-ExI}$
\bsk
%D diagram Hyp-eq-refl
%D 2Dx 100 +45
%D 2D 100 e0 ======> e1
%D 2D - -
%D 2D refl | <-| | id
%D 2D v v
%D 2D +35 e2 <====== e3
%D 2D
%D 2D +20 b0 |-----> b1
%D 2D
%D (( e0 .tex= \s[a,b|⊤] e1 .tex= \s[a,b,b'|b{=}b']
%D e2 .tex= \s[a,b|b{=}b] e3 .tex= \s[a,b,b'|b{=}b']
%D b0 .tex= a,b b1 .tex= a,b,b'
%D e0 e1 => sl_ e0 e1 <-| sl^ .plabel= a \co{◻}
%D e0 e2 |-> .plabel= l a,b;⊤|-(b{=}b) # \text{refl}
%D e1 e3 |-> .plabel= r \text{id}
%D e0 e3 harrownodes nil 20 nil <-|
%D e2 e3 <= sl_ e2 e3 |-> sl^ .plabel= a {◻}
%D b0 b1 |-> .plabel= a b':=b
%D ))
%D enddiagram
The ``reflexivity'' rule for equality (on variables):
\msk
$\diag{Hyp-eq-refl}$
\newpage
% --------------------
% «hyp-sym-trans» (to ".hyp-sym-trans")
% (s "Hyperdoctrines: symmetry, transitivity" "hyp-sym-trans")
\myslide {Hyperdoctrines: symmetry, transitivity} {hyp-sym-trans}
%D diagram Hyp-eq-sym
%D 2Dx 100 +30 +30 +30
%D 2D 100 e0 ======> e1
%D 2D - -
%D 2D refl | |-> | sym
%D 2D v v
%D 2D +35 e2 <====== e3
%D 2D /\
%D 2D \\
%D 2D \\
%D 2D +35 e4 ======> e5
%D 2D
%D 2D +21 b2 |-----> b3
%D 2D /
%D 2D \
%D 2D v
%D 2D +35 b4 |-----> b5
%D 2D
%D (( e0 .tex= \s[a,b|⊤] e1 .tex= \s[a,b,b'|b{=}b']
%D e2 .tex= \s[a,b|b{=}b] e3 .tex= \s[a,b,b'|b'{=}b]
%D e4 .tex= \s[a,b'|⊤] e5 .tex= \s[a,b',b|b'{=}b]
%D b2 .tex= a,b b3 .tex= a,b,b'
%D b4 .tex= a,b' b5 .tex= a,b',b
%D e0 e1 => sl_ e0 e1 |-> sl^ .plabel= a \co{◻}
%D e0 e2 |-> .plabel= l \text{refl}
%D e1 e3 |-> .plabel= r a,b,b';(b{=}b')|-(b'{=}b) # \text{sym}
%D e0 e3 harrownodes nil 20 nil |->
%D e2 e3 <= sl_ e2 e3 |-> sl^ .plabel= a {◻}
%D e3 e5 <= sl_ e3 e5 |-> sl^ .plabel= a {◻}
%D e4 e5 => sl_ e4 e5 |-> sl^ .plabel= a \co{◻}
%D b2 b3 |-> .plabel= a b':=b
%D b3 b5 |->
%D b4 b5 |-> .plabel= a b':=b
%D ))
%D enddiagram
%D diagram Hyp-eq-trans
%D 2Dx 100 +30 +30 +30
%D 2D 100 e0 ======> e1
%D 2D - -
%D 2D id | |-> | trans
%D 2D v v
%D 2D +35 e2 <====== e3
%D 2D /\
%D 2D \\
%D 2D \\
%D 2D +35 e4 ======> e5
%D 2D
%D 2D +21 b2 |-----> b3
%D 2D /
%D 2D \
%D 2D v
%D 2D +35 b4 |-----> b5
%D 2D
%D (( e0 .tex= \s[a,b,b'|b{=}b'] e1 .tex= \s[a,b,b',b''|b'{=}b''&b{=}b']
%D e2 .tex= \s[a,b,b'|b{=}b'] e3 .tex= \s[a,b,b',b''|b{=}b'']
%D e4 .tex= \s[a,b|⊤] e5 .tex= \s[a,b',b''|b{=}b'']
%D b2 .tex= a,b,b' b3 .tex= a,b,b',b''
%D b4 .tex= a,b b5 .tex= a,b',b''
%D e0 e1 => sl_ e0 e1 |-> sl^ .plabel= a \co{◻}
%D e0 e2 |-> .plabel= l \text{id}
%D e1 e3 |-> .plabel= r a,b,b',b'';(b'{=}b'')&(b{=}b')|-(b{=}b'') # \text{trans}
%D e0 e3 harrownodes nil 20 nil |->
%D e2 e3 <= sl_ e2 e3 |-> sl^ .plabel= a {◻}
%D e3 e5 <= sl_ e3 e5 |-> sl^ .plabel= a {◻}
%D e4 e5 => sl_ e4 e5 |-> sl^ .plabel= a \co{◻}
%D b2 b3 |-> .plabel= a b'':=b'
%D b3 b5 |->
%D b4 b5 |-> .plabel= a b'':=b
%D ))
%D enddiagram
The ``symmetry'' rule for equality (on variables):
\msk
$\diag{Hyp-eq-sym}$
\bsk
The ``transitivity'' rule for equality (on variables):
\msk
$\diag{Hyp-eq-trans}$
\newpage
% --------------------
% «weak-strong-exelim» (to ".weak-strong-exelim")
% (s "Weak and strong exists-elim" "weak-strong-exelim")
\myslide {Weak and strong exists-elim} {weak-strong-exelim}
There are two versions of $(∃E)$, $(∃E^-)$ and $(∃E^+)$.
They are ``equivalent enough'', and $(∃E^-)$ is much simpler
categorically.
The rules, in natural deduction and sequent calculus forms:
%:
%: [P(a,b)]^1 Q(a)
%: ::::::::::::::::
%: ∃b.P(a,b) R(a) a,b;P(a,b),Q(a)|-R(a)
%: ---------------------1;(∃E^+) ----------------------(∃E^+)
%: R(a) a;∃b.P(a,b),Q(a)|-R(a)
%:
%: ^ex-elim-+-nd ^ex-elim-+-sc
%:
%: [P(a,b)]^1
%: ::::::::::
%: ∃b.P(a,b) Q(a) a,b;P(a,b)|-Q(a)
%: ------------------1;(∃E^-) -----------------(∃E^-)
%: Q(a) a;∃b.P(a,b)|-Q(a)
%:
%: ^ex-elim---nd ^ex-elim---sc
%:
$$\ded{ex-elim-+-nd} \qquad \ded{ex-elim-+-sc}$$
$$\ded{ex-elim---nd} \qquad \ded{ex-elim---sc}$$
%
\indent $(∃E^-)$ is a particular case of $(∃E^+)$ --- take $Q(a):=⊤$
in $(∃E^+)$.
\medskip
In the presence of $(→)$ the rule $(∃E^-)$ implies $(∃E^+)$:
%:
%: [P(a,b)]^2 [Q(a)]^1
%: ::::::::::::::::::::
%: R(a)
%: ---------1;(→I)
%: ∃b.P(a,b) Q(a)→R(a)
%: ---------------------2;(∃E^+)
%: Q(a) Q(a)→R(a)
%: ---------------------(→E)
%: R(a)
%:
%: ^ex-elim---implies-+
%:
$$\ded{ex-elim---implies-+}$$
%D diagram exists-elim--
%D 2Dx 100 +35
%D 2D 100 P(a,b) ====> ∃b.P(a,b)
%D 2D - -
%D 2D | |--> |
%D 2D v v
%D 2D +25 {}Q(a) <======= Q(a)
%D 2D
%D 2D +15 a,b |---------> a
%D 2D
%D (( P(a,b) ∃b.P(a,b)
%D {}Q(a) Q(a)
%D a,b a
%D @ 0 @ 1 =>
%D @ 0 @ 2 |-> @ 1 @ 3 |->
%D @ 0 @ 3 harrownodes nil 20 nil |->
%D @ 2 @ 3 <=
%D @ 4 @ 5 |->
%D ))
%D enddiagram
%D diagram exists-elim-+
%D 2Dx 100 +45 +50 +55
%D 2D 100 P(a,b)&Q(a) <=== P(a,b) ====> ∃b.P(a,b) ===> (∃b.P(a,b))&Q(a)
%D 2D - - - -
%D 2D | |--> | |--> | |--> |
%D 2D v v v v
%D 2D +25 {}R(a) ===> {}Q(a)→R(a) <= Q(a)→R(a){} <======= R(a)
%D 2D
%D 2D +15 {}a,b ========= a,b |---------> a ============== a{}
%D 2D
%D (( P(a,b)&Q(a) P(a,b) ∃b.P(a,b) (∃b.P(a,b))&Q(a)
%D {}R(a) {}Q(a)→R(a) Q(a)→R(a){} R(a)
%D {}a,b a,b a a{}
%D @ 0 @ 1 <= @ 1 @ 2 => @ 2 @ 3 =>
%D @ 0 @ 4 |-> @ 1 @ 5 |-> @ 2 @ 6 |-> @ 3 @ 7 |->
%D @ 0 @ 5 harrownodes nil 20 nil |->
%D @ 1 @ 6 harrownodes nil 20 nil |->
%D @ 2 @ 7 harrownodes nil 20 nil |->
%D @ 4 @ 5 => @ 5 @ 6 <= @ 6 @ 7 <=
%D @ 8 @ 9 = @ 9 @ 10 |-> @ 10 @ 11 =
%D ))
%D enddiagram
$(∃E^-)$, categorically:
$\diag{exists-elim--}$
\medskip
$(∃E^+)$, categorically:
$\diag{exists-elim-+}$
Note that $\O[\dncdisplay[a,b|Q(a)→R(a)]]$ has two constructions,
with a hidden iso between them.
\newpage
% --------------------
% «rules-nd-sc» (to ".rules-nd-sc")
% (s "Rules in ND and sequent calculus" "rules-nd-sc")
\myslide {Rules in ND and sequent calculus} {rules-nd-sc}
\def\hli{\mathstrut \\ \hline \mathstrut \\}
%:
%: (&I): P P --| P |--
%: : : / - \
%: Q R P|-Q P|-R / | \
%: -----(&I) ------------(&I) v v v
%: Q&R P|-Q&R Q <--| Q&R |--> R
%:
%: ^andI-nd ^andI-sc
%:
%:
%: (&E): Q&R Q&R
%: ---(&E_1) ---(&E_2)
%: P Q P R P,Q|-S P,R|-S
%: ::::: ::::: --------(&E_1) --------(&E_2)
%: S S P,Q&R|-S P,Q&R|-S
%:
%: ^andE1-nd ^andE2-nd ^andE1-sc ^andE2-sc
%:
%:
%: (→I): P [Q]^1 P&Q <=== P
%: ::::::::: - -
%: R P,Q|-R | |-> |
%: ---1;(→I) ------(→I) v v
%: Q→R P|-Q→R R ===> Q→R
%:
%: ^impI-nd ^impI-sc
%: ---| P |----
%: / - \
%: (→E): P P / | \
%: : : v v v
%: Q Q→R P|-Q P|-Q→R Q <--| (Q→R)&Q |--> Q→R{}
%: --------(→E) -------------(→E) - <=== -
%: R P|-R | <--| |\id
%: v v
%: ^impE-nd ^impE-sc R ======> Q→R
%:
%:
%:
%: (∀I): P(a) Q(a) <====== Q(a)
%: :::::: - -
%: Q(a,b) a,b;P(a)|-Q(a,b) | |--> |
%: ---------(∀I) ----------------(∀I) v v
%: ∀b.Q(a,b) a;P(a)|-∀b.Q(a,b) R(a,b) ===> ∀b.R(a,b)
%:
%: ^FaI-nd ^FaI-sc a,b |-------> a
%:
%:
%: (∀E): a Q(a)
%: : :
%: f(a) ∀b.R(a,b) a|-f(a) a;Q(a)|-∀b.R(a,b)
%: ----------------(∀E) --------------------------(∀E)
%: R(a,f(a)) a;Q(a)|-R(a,f(a))
%:
%: ^FaE-nd ^FaE-sc
%:
%: Q(a) <====== Q(a) <===== Q(a)
%: - - -
%: | <--| | <--| |
%: v v v
%: R(a,f(a)) ==> R(a,b) ==> ∀b.R(a,b)
%: b:=f(a)
%: a |-------> a,b |------> a
%:
%: (∃I): Q(a)
%: :::::::::
%: P(a,f(a)) a;Q(a)|-P(a,f(a))
%: ---------(∃I) -----------------(∃I)
%: ∃b.P(a,b) a;Q(a)|-∃b.P(a,b)
%:
%: ^ExI-nd ^ExI-sc
%:
%: P(a,f(a)) <===== P(a,b) =====> ∃b.P(a,b)
%: - - -
%: | <--| | <--| |\id
%: v v v
%: ∃b.P(a,b) <=== ∃b.P(a,b) <=== ∃b.P(a,b)
%: b:=f(a)
%: a |---------> a,b |----------> a
%:
%:
%: (∃E): [P(a,b)]^1 Q(a)
%: ::::::::::::::::
%: ∃b.P(a,b) R(a) a,b;P(a,b),Q(a)|-R(a)
%: ---------------------(∃E) ----------------------(∃E)
%: R(a) a;∃b.P(a,b),Q(a)|-R(a)
%:
%: ^ExE-nd ^ExE-sc
%:
The rules, in natural deduction form ($(∀E)$ is wrong):
%
$$\begin{array}{c|c}
\ded{andI-nd} & \ded{andE1-nd} \qquad \ded{andE2-nd} \\ \hli
\ded{impI-nd} & \ded{impE-nd} \\ \hli
\ded{FaI-nd} & \ded{FaE-nd} \\ \hli
\ded{ExI-nd} & \ded{ExE-nd} \\
\end{array}
$$
The rules, in sequent calculus form ($(∀E)$ is wrong):
%
$$\begin{array}{c|c}
\ded{andI-sc} & \ded{andE1-sc} \qquad \ded{andE2-sc} \\ \hli
\ded{impI-sc} & \ded{impE-sc} \\ \hli
\ded{FaI-sc} & \ded{FaE-sc} \\ \hli
\ded{ExI-sc} & \ded{ExE-sc} \\
\end{array}
$$
\newpage
% --------------------
% «rules-categorically» (to ".rules-categorically")
% (s "Rules, categorically" "rules-categorically")
\myslide {Rules, categorically} {rules-categorically}
%D diagram andI-cat
%D 2Dx 100 +25 +25
%D 2D 100 --| P |--
%D 2D / - \
%D 2D / | \
%D 2D v v v
%D 2D +25 Q <--| Q&R |--> R
%D 2D
%D (( P Q Q&R R
%D @ 0 @ 1 |-> @ 0 @ 2 |-> @ 0 @ 3 |->
%D @ 1 @ 2 <-| .plabel= a \pi
%D @ 2 @ 3 |-> .plabel= a \pi'
%D ))
%D enddiagram
%D diagram andE-cat
%D 2Dx 100 +35 +35
%D 2D 100 Q <---| Q&R |---> R
%D 2D || - || - ||
%D 2D || | || | ||
%D 2D \/ v \/ v \/
%D 2D +25 P&Q <--| P&Q&R |--> P&R
%D 2D
%D (( Q Q&R R
%D P&Q P&Q&R P&R
%D @ 0 @ 1 <-| .plabel= a \pi
%D @ 1 @ 2 |-> .plabel= a \pi'
%D @ 0 @ 3 => @ 1 @ 4 => @ 2 @ 5 =>
%D @ 0 @ 4 varrownodes nil 18 nil |->
%D @ 1 @ 5 varrownodes nil 18 nil |->
%D @ 3 @ 4 <-| @ 4 @ 5 |->
%D ))
%D enddiagram
%D diagram impI-cat
%D 2Dx 100 +25
%D 2D 100 P&Q <=== P
%D 2D - -
%D 2D | |-> |
%D 2D v v
%D 2D +25 R ===> Q→R
%D 2D
%D (( P&Q P R Q→R
%D @ 0 @ 1 <=
%D @ 0 @ 2 |-> @ 1 @ 3 |->
%D @ 0 @ 3 harrownodes nil 20 nil |->
%D @ 2 @ 3 =>
%D ))
%D enddiagram
%D diagram impE-cat
%D 2Dx 100 +35 +35
%D 2D 100 ---| P |----
%D 2D / - \
%D 2D / | \
%D 2D v v v
%D 2D +25 Q <--| (Q→R)&Q |--> Q→R{}
%D 2D - <=== -
%D 2D | <--| |\id
%D 2D v v
%D 2D +25 R ======> Q→R
%D 2D
%D (( P
%D Q (Q→R)&Q Q→R{}
%D R Q→R
%D @ 0 @ 1 |-> @ 0 @ 2 |-> @ 0 @ 3 |->
%D @ 1 @ 2 <-| .plabel= a {\phantom{\;\;\;\;}\pi'}
%D @ 2 @ 3 |-> sl^ .plabel= a {\pi}
%D @ 2 @ 3 <= sl_
%D @ 2 @ 4 |-> @ 3 @ 5 |-> .plabel= r \id
%D @ 2 @ 5 harrownodes nil 20 nil <-|
%D @ 4 @ 5 =>
%D ))
%D enddiagram
%D diagram faI-cat
%D 2Dx 100 +35
%D 2D 100 Q(a) <====== Q(a){}
%D 2D - -
%D 2D | |--> |
%D 2D v v
%D 2D +25 R(a,b) ===> ∀b.R(a,b)
%D 2D
%D 2D +15 a,b |-------> a
%D 2D
%D (( Q(a) Q(a){}
%D R(a,b) ∀b.R(a,b)
%D a,b a
%D @ 0 @ 1 <=
%D @ 0 @ 2 |-> @ 1 @ 3 |->
%D @ 0 @ 3 harrownodes nil 20 nil |->
%D @ 2 @ 3 =>
%D @ 4 @ 5 |->
%D ))
%D enddiagram
%D diagram faE-cat
%D 2Dx 100 +35 +35
%D 2D 100 {}Q(a) <====== Q(a) <===== Q(a){}
%D 2D - - -
%D 2D | <--| | <--| |
%D 2D v v v
%D 2D +25 R(a,f(a)) ==> R(a,b) ==> ∀b.R(a,b)
%D 2D b:=f(a)
%D 2D +15 a |-------> a,b |------> a{}
%D 2D
%D (( {}Q(a) Q(a) Q(a){}
%D R(a,f(a)) R(a,b) ∀b.R(a,b)
%D a a,b a{}
%D @ 0 @ 1 <= @ 1 @ 2 <=
%D @ 0 @ 3 |-> @ 1 @ 4 |-> @ 2 @ 5 |->
%D @ 0 @ 4 harrownodes nil 20 nil <-|
%D @ 1 @ 5 harrownodes nil 20 nil <-|
%D @ 3 @ 4 => @ 4 @ 5 =>
%D @ 6 @ 7 |-> .plabel= a b:=f(a) @ 7 @ 8 |->
%D ))
%D enddiagram
%D diagram exI-cat
%D 2Dx 100 +40 +40
%D 2D 100 P(a,f(a)) <===== P(a,b) =====> ∃b.P(a,b){}{}
%D 2D - - -
%D 2D | <--| | <--| |\id
%D 2D v v v
%D 2D +25 {}∃b.P(a,b) <=== ∃b.P(a,b) <=== ∃b.P(a,b){}
%D 2D b:=f(a)
%D 2D +15 a |---------> a,b |----------> a{}
%D 2D
%D (( P(a,f(a)) P(a,b) ∃b.P(a,b){}{}
%D {}∃b.P(a,b) ∃b.P(a,b) ∃b.P(a,b){}
%D a a,b a{}
%D @ 0 @ 1 <= @ 1 @ 2 =>
%D @ 0 @ 3 |-> @ 1 @ 4 |-> @ 2 @ 5 |->
%D @ 0 @ 4 harrownodes nil 20 nil <-|
%D @ 1 @ 5 harrownodes nil 20 nil <-|
%D @ 3 @ 4 <= @ 4 @ 5 <=
%D @ 6 @ 7 |-> .plabel= a b:=f(a) @ 7 @ 8 |->
%D ))
%D enddiagram
The rules, categorically ($(\&E)$ needs explanations, $(∀E)$ is wrong):
%
$$\begin{array}{c|c}
\diag{andI-cat} & \diag{andE-cat} \\ \hli
\diag{impI-cat} & \diag{impE-cat} \\ \hli
\diag{faI-cat} & \diag{faE-cat} \\ \hli
\diag{exI-cat} & \text{(see next page)} \\
\end{array}
$$
\end{document}
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cp -v ~/LATEX/2008hyp.tex /tmp/o
~/LUA/texcatcodes.lua -trans /tmp/o /tmp/o2
# (find-fline "/tmp/o2")
% Local Variables:
% coding: utf-8-unix
% ee-tla: "hyp8"
% End: