% (find-LATEX "2020hyp.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020hyp.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2020hyp.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020hyp.pdf"))
% (defun e () (interactive) (find-LATEX "2020hyp.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020hyp"))
% (defun v0 () (interactive) (find-2a '(e) '(d)))
% (defun v  () (interactive) (find-2a '(e) '(d)) (g))
% (find-pdf-page   "~/LATEX/2020hyp.pdf")
% (find-sh0 "cp -v  ~/LATEX/2020hyp.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2020hyp.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2020hyp.pdf
%               file:///tmp/2020hyp.pdf
%           file:///tmp/pen/2020hyp.pdf
% http://angg.twu.net/LATEX/2020hyp.pdf
% http://angg.twu.net/LATEX/2020hyp.pdf#page=14
% (find-LATEX "2019.mk")

% «.defs»			(to "defs")
% «.limp-2020»			(to "limp-2020")
% «.myenumerate»		(to "myenumerate")

% «.title-page»			(to "title-page")
% «.sources»			(to "sources")
% «.bcc-seely-lccc»		(to "bcc-seely-lccc")
% «.equahyp-p5»			(to "equahyp-p5")
% «.preservation-of-imp»	(to "preservation-of-imp")
%
% «.introduction»		(to "introduction")
% «.hyp-ND-rules»		(to "hyp-ND-rules")
% «.why-hyperdoctrines»		(to "why-hyperdoctrines")
% «.why-hyperdoctrines-2»	(to "why-hyperdoctrines-2")
% «.quants-for-children»	(to "quants-for-children")
% «.or-elim»			(to "or-elim")
% «.quants-for-children-2»	(to "quants-for-children-2")
% «.dummett»			(to "dummett")
% «.we-can-use-to»		(to "we-can-use-to")
% «.judgments»			(to "judgments")
% «.judgments-cat»		(to "judgments-cat")
% «.arrows»			(to "arrows")
% «.pred»			(to "pred")
% «.predicates-over»		(to "predicates-over")
% «.predicates-over-2»		(to "predicates-over-2")
% «.plc»			(to "plc")

\documentclass[oneside]{book}
\usepackage[colorlinks,citecolor=DarkRed,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}
%\usepackage{kpfonts}                  % (find-es "tex" "mathfrak-kpfonts")
\usepackage{MnSymbol}                  % (find-es "tex" "lhookdownarrow")
%
% (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof}   % For derivation trees ("%:" lines)
\input diagxy        % For 2D diagrams ("%D" lines)
\xyoption{curve}     % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx15}               % (find-LATEX "edrx15.sty")
\input edrxaccents.tex            % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-LATEX "edrxheadfoot.tex")
%\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
%\input edrx17defs.tex             % (find-LATEX "edrx17defs.tex")
%\input 2017planar-has-defs.tex    % (find-LATEX "2017planar-has-defs.tex")
%
% (find-es "tex" "geometry")
% (find-latexgeomtext "total={6.5in,8.75in},")
\usepackage[paperwidth=11.5cm, paperheight=9.5cm,
            %total={6.5in,4in},
            %textwidth=4in,  paperwidth=4.5in,
            %textheight=5in, paperheight=4.5in,
            %a4paper,
            top=1.5cm, bottom=.5cm, left=1cm, right=1cm, includefoot
           ]{geometry}
%
\usepackage[backend=biber,
   style=alphabetic]{biblatex} % (find-es "tex" "biber")
\addbibresource{catsem-u.bib}  % (find-LATEX "catsem-u.bib")
%
% See: (find-es "tex" "limp-abx")
\DeclareFontFamily{U}{matha}{\hyphenchar\font45}
\DeclareFontShape{U}{matha}{m}{n}{
      <5> <6> <7> <8> <9> <10> gen * matha
      <10.95> matha10 <12> <14.4> <17.28> <20.74> <24.88> matha12
      }{}
\DeclareSymbolFont{matha}{U}{matha}{m}{n}
\DeclareMathSymbol{\thinsubset}{3}{matha}{"80}
\DeclareMathSymbol{\thinsupset}{3}{matha}{"81}
\def\limp{\thinsupset}
%
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

%L dofile "edrxtikz.lua"  -- (find-LATEX "edrxtikz.lua")
%L dofile "edrxpict.lua"  -- (find-LATEX "edrxpict.lua")
\pu


%  ____        __     
% |  _ \  ___ / _|___ 
% | | | |/ _ \ |_/ __|
% | |_| |  __/  _\__ \
% |____/ \___|_| |___/
%                     
% «defs»  (to ".defs")

\def\dnito{\lhookdownarrow}
\def\Ords{\mathsf{Ords}}

\def\psmi  #1#2{  \psm {#1 \\ \dnito \\ #2}}
\def\pmati #1#2{  \pmat{#1 \\ \dnito \\ #2}}
\def\pmatin#1#2#3{\pmat{#1 \\ \dnito & #3 \\ #2}}
\def \matin#1#2#3{ \mat{#1 \\ \dnito & #3 \\ #2}}

\long\def\ColorRed   #1{{\color{Red1}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorViolet#1{{\color{Violet!50!black}#1}}
\long\def\ColorGreen #1{{\color{SpringDarkHard}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#1}}
\long\def\ColorGreen #1{{\color{SpringGreen4}#1}}
\long\def\ColorGray  #1{{\color{GrayLight}#1}}
\long\def\ColorGray  #1{{\color{black!30!white}#1}}

% «limp-2020»  (to ".limp-2020")
% Logical implication, as a thin \supset - version 2020feb20
% (find-es "tex" "limp-abx")
% (find-es "tex" "thin_supset")
% (find-es "tex" "pict2e")
% (find-es "tex" "begin-picture" "(XSIZE,YSIZE)(XORG,YORG)")
%
%\def\limpbody{%
%  \begin{picture}%(4,2)
%                 (5.1,2.5)(-0.5,-0.25)
%    \Line(0,0)(3,0)
%    \Line(0,2)(3,2)
%    \put(3,1){\arc[-90,90]{1}}
%  \end{picture}%
%  }
%\def\limp{%
%  \mathrel{\vcenter{\hbox{%
%    \unitlength=2pt%
%    \linethickness{0.4pt}%
%    \limpbody%
%  }}}}

\catcode`✀=13 \def✀{\limp}
\catcode`⊸=13 \def⊸{\limp}

% Test:
% $R {\limp}
%  S \limp
%  T \supset
%  U \bhbox{$\supset$}
%  V \bhbox{$\limp$}
%  W
% $

\setlength{\parindent}{0pt}

% «myenumerate»  (to ".myenumerate")
% (find-LATEX "2020list-test.tex")
\newcounter{mycounter}
\long\def\myenumerate#1{%
  \begin{list}{\arabic{mycounter}.}%
    {\usecounter{mycounter}
     \setlength\topsep{0pt}
     \setlength\parsep{0pt}
     \setlength\itemsep{0pt}
    }
    #1 
  \end{list}
  }



%  _____ _ _   _                               
% |_   _(_) |_| | ___   _ __   __ _  __ _  ___ 
%   | | | | __| |/ _ \ | '_ \ / _` |/ _` |/ _ \
%   | | | | |_| |  __/ | |_) | (_| | (_| |  __/
%   |_| |_|\__|_|\___| | .__/ \__,_|\__, |\___|
%                      |_|          |___/      
%
% «title-page»  (to ".title-page")

Notes on Hyperdoctrines

\newpage

\noedrxfooter

{\bf Dummett's notation for Natural Deduction: $∃-$}

In \cite{Dummett}, p.89, he writes ND trees as $H_1,\ldots,H_n:C$...
%
%:  Γ:∃x\,A(x)   Δ,A(y):C
%:  ---------------------∃-
%:     Γ,Δ:C
%:
%:     ^Dummett-0
%:
%:  \vec{P}:∃x\,Q(x)   \vec{R},Q(y):S
%:  ---------------------------------
%:     \vec{P},\vec{R}:S
%:
%:     ^Dummett-1
%:
%:  P_1,P_2:∃x\,Q(x)   R_1,R_2,Q(y):S   α  β
%:  --------------------------------    ----
%:     P_1,P_2,R_1,R_2:S                 γ
%:
%:     ^Dummett-2                        ^Dummett-3
%:
%:  P_1  P_2    R_1  R_2  [Q(y)]^1
%:  ::::::::α   ::::::::::::::::::β
%:  ∃x\,Q(x)          S               P_1  P_2  R_1  R_2
%:  -------------------1              ::::::::::::::::::γ
%:          S                                S
%:
%:          ^Dummett-4                       ^Dummett-5
%:
\pu
$$\scalebox{0.8}{$
  \begin{array}{l}
    \begin{array}{lll}
      \ded{Dummett-0} \\ \\
      \ded{Dummett-1} \\ \\
      \ded{Dummett-2} & & \ded{Dummett-3} \\
    \end{array}
    \\
    \\
    \\
    \begin{array}{ccc}
      \ded{Dummett-4} &\Longrightarrow & \ded{Dummett-5} \\
    \end{array} \\
  \end{array}
  $}
$$

\newpage

{\bf A weaker rule: $∃-$}
%:
%:  Γ:∃x\,A(x)   Δ,A(y):C
%:  ---------------------∃-
%:     Γ,Δ:C
%:
%:     ^DumWeak-0
%:
%:  Γ:∃x\,A(x)   A(y):C
%:  -------------------∃--
%:     Γ:C
%:
%:     ^DumWeak-1
%:
%:               A(y):C
%:     ----------------∃---
%:     ∃x\,A(x):C
%:
%:     ^DumWeak--1
%:
%:  P_1,P_2:∃x\,Q(x)   R_1,R_2,Q(y):S
%:  ---------------------------------
%:     P_1,P_2,R_1,R_2:S             
%:
%:     ^DumWeak-2                    
%:
%:                      R_1,R_2,Q(y):S 
%:                      -------------- 
%:                      R_1,Q(y):R_2⊸S 
%:                     ----------------
%:  P_1,P_2:∃x\,Q(x)   Q(y):R_1⊸(R_2⊸S)
%:  -----------------------------------∃--
%:     P_1,P_2:R_1⊸(R_2⊸S)
%:     -------------------
%:     P_1,P_2,R_1:R_2⊸S             
%:     -----------------
%:     P_1,P_2,R_1,R_2:S             
%:                                   
%:     ^DumWeak-3 
%:
%:                       R_1,R_2,Q(y):S 
%:                       -------------- 
%:                       R_1,Q(y):R_2⊸S 
%:                      ----------------
%:                      Q(y):R_1⊸(R_2⊸S)
%:                    --------------------∃---
%:  P_1,P_2:∃x\,Q(x)  ∃x\,Q(x):R_1⊸(R_2⊸S)
%:  -------------------------------------𝐬{Cut}
%:     P_1,P_2:R_1⊸(R_2⊸S)
%:     -------------------
%:     P_1,P_2,R_1:R_2⊸S             
%:     -----------------
%:     P_1,P_2,R_1,R_2:S             
%:                                   
%:     ^DumWeak--3 
%:

\pu
\bsk
$\scalebox{0.8}{$
  \begin{array}{l}
    \ded{DumWeak-0} \\ \\
    \ded{DumWeak-1} \\ \\
    \ded{DumWeak-2} \\ \\
    \ded{DumWeak-3} \\
  \end{array}
  $}
$

\newpage

{\bf A rule that is even weaker: $∃---$}

\bsk
$\scalebox{0.8}{$
  \begin{array}{l}
    \ded{DumWeak-0} \\ \\
    \phantom{mmmmm}
    \ded{DumWeak--1} \\ \\
    \ded{DumWeak-2} \\ \\
    \ded{DumWeak--3} \\
  \end{array}
  $}
$

\newpage

{\bf A rule that is even weaker: $∃---$ (2)}

%:
%:                       [R_1]^2  [R_2]^1  [Q(y)]^3
%:                       ::::::::::::::::::::::::::β
%:                                  S               
%:                                -----1
%:            P_1  P_2            R_2⊸S
%:            ::::::::α        ----------2
%:            ∃x\,Q(x)         R_1⊸(R_2⊸S)
%:            ----------------------------3        
%:       R_1             R_1⊸(R_2⊸S)           
%:       ---------------------------
%:  R_2             R_2⊸S
%:  ---------------------
%:          S
%:
%:          ^DumWeak--3-ND
%:
\pu
\msk
$\scalebox{0.7}{$
  \begin{array}{ccc}
    \cded{DumWeak--3}   && \cded{Dummett-3}  \\ \\ \\
    \cded{DumWeak--3-ND} && \cded{Dummett-5}  \\
  \end{array}
  $}
$

\newpage

%  ____                                
% / ___|  ___  _   _ _ __ ___ ___  ___ 
% \___ \ / _ \| | | | '__/ __/ _ \/ __|
%  ___) | (_) | |_| | | | (_|  __/\__ \
% |____/ \___/ \__,_|_|  \___\___||___/
%                                      
% «sources»  (to ".sources")

{\bf Sources}

% https://ncatlab.org/nlab/show/Grothendieck+fibration#references

\cite{SeelyBeck},
\cite{SeelyLCCC},
\cite{SeelyPLC}
% (find-books "__cats/__cats.el" "seely-hyp")
% (find-books "__cats/__cats.el" "seely-lccc")
% (find-books "__cats/__cats.el" "seely-plc")

\cite{LawvereAdjFo},
\cite{LawvereEqHyp}
% (find-books "__cats/__cats.el" "lawvere-adjfo")
% (find-lawvereadjfopage 11 "A hyperdoctrine shall consist of")
% (find-lawvereadjfotext 11 "A hyperdoctrine shall consist of")
% (find-books "__cats/__cats.el" "lawvere-equahyp")

\cite{PareSchumacher}
% (find-books "__cats/__cats.el" "pare-schumacher")

\cite{Gray66}
% (find-books "__cats/__cats.el" "gray")

\cite{Jacobs}
% (find-books "__cats/__cats.el" "jacobs")

\cite{BarrWellsCTCS}
% (find-books "__cats/__cats.el" "barr-wells-ctcs")

% (find-books "__cats/__cats.el" "grothendieck-sga1")
% (find-books "__cats/__cats.el" "grothendieck-sga1" "VI. Categories fibrees")



\newpage

%  ____            _       _     ____ ____ ____ 
% / ___|  ___  ___| |_   _| |   / ___/ ___/ ___|
% \___ \ / _ \/ _ \ | | | | |  | |  | |  | |    
%  ___) |  __/  __/ | |_| | |__| |__| |__| |___ 
% |____/ \___|\___|_|\__, |_____\____\____\____|
%                    |___/                      
%
% «bcc-seely-lccc»  (to ".bcc-seely-lccc")
% (hypp 7 "bcc-seely-lccc")
% (hyp    "bcc-seely-lccc")
% (find-books "__cats/__cats.el" "seely-lccc")
% (find-seelylcccpage (+ -32 37)    "(iv)    P satisfies the Beck condition:")
% (find-seelylccctext (+ -32 37)    "(iv)    P satisfies the Beck condition:")
% (find-TH "dednat6" "a-big-example")
% (find-dednat6 "tug-slides.tex" "BCC")

{\bf BCC in the SeelyLCCC paper}

\def\BCCL{\mathsf{BCCL}}


%D diagram BCC-Seely-LCCC-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 A0 |---------------------> A1
%D 2D        |->                        |->
%D 2D +35        A2 |--------------------> A3
%D 2D
%D ((
%D    B0 .tex=       h^*φ            B1 .tex=       φ
%D    B2 .tex= k^*f^*Σ_gφ            B3 .tex= g^*Σ_gφ
%D   B2' .tex= h^*g^*Σ_gφ
%D    B4 .tex=    Σ_kh^*φ            B5 .tex= Σ_gφ
%D    B6 .tex=    f^*Σ_gφ            B7 .tex= Σ_gφ
%D    B0 B1 <-| B0 B2 -> B0 B2' -> B1 B3 -> B2 B2' <-> B2' B3 <-|
%D    B0 B4 |-> B1 B5 |->
%D    B2 B6 <-| B3 B7 <-|
%D    B6 B7 <-| B5 B7 -> .plabel= r \id
%D    B4 B6 -> sl_ .plabel= l ♮ B4 B6 <- sl^ .plabel= r \BCCL
%D    B0 B2' midpoint B1 B3 midpoint  harrownodes nil 20 nil <-|
%D    B0  B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D    B1  B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( A0 .tex= D   A1 .tex= C   A2 .tex= A   A3 .tex= B 
%D    A0 A1 -> .plabel= b h
%D    A0 A2 -> .plabel= l k
%D    A1 A3 -> .plabel= r g
%D    A2 A3 -> .plabel= a f
%D    A0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\pu
  \diag{BCC-Seely-LCCC-1}
$$

\newpage

{\bf BCC in the SeelyLCCC paper (2)}

%D diagram BCC-Seely-LCCC-my
%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 A0 |---------------------> A1
%D 2D        |->                        |->
%D 2D +35        A2 |--------------------> A3
%D 2D
%D ((
%D    B0 .tex=       h^*φ            B1 .tex=       φ
%D    B2 .tex= k^*f^*Σ_gφ            B3 .tex= g^*Σ_gφ
%D   B2' .tex= h^*g^*Σ_gφ
%D    B4 .tex=    Σ_kh^*φ            B5 .tex= Σ_gφ
%D    B6 .tex=    f^*Σ_gφ            B7 .tex= Σ_gφ
%D
%D    B0 .tex=   \bsm{x\\b,a,c}      B1 .tex= \bsm{x\\b,c}
%D    B2 .tex= \bsm{c,x\\b,a,c}      B3 .tex= \bsm{c,x\\b,c}
%D   B2' .tex= \bsm{c,x\\b,a,c}
%D    B4 .tex= \bsm{c,x\\b,a}        B5 .tex= \bsm{c,x\\b}
%D    B6 .tex= \bsm{c,x\\b,a}        B7 .tex= \bsm{c,x\\b}
%D
%D    B0 B1 <-| B0 B2 -> B0 B2' -> B1 B3 -> B2 B2' <-> B2' B3 <-|
%D    B0 B4 |-> B1 B5 |->
%D    B2 B6 <-| B3 B7 <-|
%D    B6 B7 <-| B5 B7 -> .plabel= r \id
%D    B4 B6 -> sl_ .plabel= l ♮ B4 B6 <- sl^ .plabel= r \BCCL
%D    B0 B2' midpoint B1 B3 midpoint  harrownodes nil 20 nil <-|
%D    B0  B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D    B1  B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( A0 .tex= D         A1 .tex= C       A2 .tex= A      A3 .tex= B
%D    A0 .tex= [b,a,c]   A1 .tex= [b,c]   A2 .tex= [b,a]  A3 .tex= [b] 
%D    A0 A1 -> .plabel= b h
%D    A0 A2 -> .plabel= l k
%D    A1 A3 -> .plabel= r g
%D    A2 A3 -> .plabel= a f
%D    A0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\pu
  \scalebox{0.9}{$
  \diag{BCC-Seely-LCCC-my}
  $}
$$

\newpage

{\bf BCC in the SeelyLCCC paper (2)}

% (nmop 2 "components")
% (nmo    "components")

%:
%:            φ
%:          ----
%:          Σ_gφ
%:     -------------
%:     \id:Σ_gφ→Σ_gφ                              φ
%:   -----------------         -------------    ----
%:   η=\id^♯:φ→g^*Σ_gφ         h^*g^*≅k^*f^*    Σ_gφ
%:   --------------------    -----------------------
%:   h^*η:h^*φ→h^*g^*Σ_gφ    α:h^*g^*Σ_gφ→k^*f^*Σ_gφ
%:   -----------------------------------------------
%:           α∘h^*η:h^*φ→k^*f^*Σ_gφ
%:         ----------------------------
%:         ♮=(α∘h^*η)^♭:Σ_kh^*φ→f^*Σ_gφ
%:   
%:         ^BCC-Seely-LCCC-1
%:
$$\pu
  \ded{BCC-Seely-LCCC-1}
$$



\newpage

%  _____                  _   _             
% | ____|__ _ _   _  __ _| | | |_   _ _ __  
% |  _| / _` | | | |/ _` | |_| | | | | '_ \ 
% | |__| (_| | |_| | (_| |  _  | |_| | |_) |
% |_____\__, |\__,_|\__,_|_| |_|\__, | .__/ 
%          |_|                  |___/|_|    
%
% «equahyp-p5»  (to ".equahyp-p5")
% (hypp 10 "equahyp-p5")
% (hyp     "equahyp-p5")
% (leqp 1 "reflexivity")
% (leq    "reflexivity")
% (find-books "__cats/__cats.el" "lawvere-equahyp")
% (find-lawvereequahyppage 5 "reflexivity")
% (find-lawvereequahyptext 5 "reflexivity")

{\bf Lawvere EquaHyp, p.5}


%D diagram ??
%D 2Dx     100 +35 +20 +10
%D 2D  100 A0  A1  A1= A1R
%D 2D
%D 2D  +25 A2  A3
%D 2D
%D 2D  +15 B0  B1
%D 2D
%D ren A0 A1 A1= A1R ==> 1_X 1_XΣ(Xδ) = Θ_X
%D ren A2 A3         ==> (Xδ)·Θ_X Θ_X
%D ren B0 B1         ==> X X×X
%D
%D (( A0 A1 |-> A1= place A1R place
%D    A0 A2 -> .plabel= l \text{refl}
%D    A1 A3 -> .plabel= r \id
%D    A0 A3 harrownodes nil 20 nil <-|
%D    A2 A3 <-|
%D    B0 B1 -> .plabel= a Xδ
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

\newpage

% «preservation-of-imp»  (to ".preservation-of-imp")
% (hypp 11 "preservation-of-imp")
% (hyp     "preservation-of-imp")

{\bf Preservation of `implies'}

% (find-LATEX "2008hyp-utf8.tex" "pres-of-imp")

\bsk

%D diagram pres-imp-1
%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' <->
%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
%
$\pu
  \scalebox{0.85}{$
  \diag{pres-imp-1}
  $}
$

% (find-lawvereequahyppage 6 "PROPOSITION (SUBSTITUTIVITY OF EQUALITY)")
% (find-lawvereequahyptext 6 "PROPOSITION (SUBSTITUTIVITY OF EQUALITY)")

%:                                       ---------------
%:                                       (P{→}Q)→(P{→}Q)
%:                                       ---------------
%:                                       (P{→}Q)∧P→Q
%:   ------------------------------   -------------------
%:   f^*(P{→}Q)∧f^*P↔f^*((P{→}Q)∧P)   f^*((P{→}Q)∧P)→f^*Q
%:   ----------------------------------------------------
%:             f^*(P{→}Q)∧f^*P→f^*Q
%:             ------------------------
%:             ♮:f^*(P{→}Q)→(f^*P→f^*Q)
%:
%:             ^pres-imp-1
%:
$$\pu
  \ded{pres-imp-1}
$$



%:
%:
%:   -----       -------      -------- 
%:   ⊤∧P→P       π∘Δ=\id      π'∘Δ=\id 
%:   -------   ----------   -----------
%:   ⊤→(P→P)   Δ^*π^*≅\id   Δ^*π'^*≅\id
%:   ----------------------------------
%:   ⊤→(Δ^*π^*P→Δ^*π'^*P)                 𝐬P→
%:   ----------------------------------------
%:     ⊤→Δ^*(π^*P→π'^*P)
%:     -----------------
%:     Σ_Δ⊤→(π^*P→π'^*P)
%:
%:      ^pres-imp-2
%:
$$\pu
  \ded{pres-imp-2}
$$


\newpage


%  ___       _                 _            _   _             
% |_ _|_ __ | |_ _ __ ___   __| |_   _  ___| |_(_) ___  _ __  
%  | || '_ \| __| '__/ _ \ / _` | | | |/ __| __| |/ _ \| '_ \ 
%  | || | | | |_| | | (_) | (_| | |_| | (__| |_| | (_) | | | |
% |___|_| |_|\__|_|  \___/ \__,_|\__,_|\___|\__|_|\___/|_| |_|
%                                                             
% «introduction»  (to ".introduction")
% (hypp 13 "introduction")
% (hyp     "introduction")

{\bf Introduction}

One of the main ideas that I tried to develop in my PhD thesis a
looong time ago was that {\sl constructions in Category Theory can be
  expressed in a language that looks like Natural Deduction}. That
language turned out to be {\sl very} difficult to formalize, but it
gave rise to several spin-offs, most of them related to translating
between languages... basically, between:

\ssk

\myenumerate{

\item the internal language of a topos

\item the language of the categorical constructions in a topos

\item the internal language of the ``archetypal'' topos, $\Set$

\item the language of the categorical constructions in a hyperdoctrine

\item the languages in Bart Jacobs's book

\ssk

\item the language of a general case (``for adults'')

\item the language of a particular case (``for children'')

}


\newpage

%  _   _               _   _ ____               _           
% | | | |_   _ _ __   | \ | |  _ \   _ __ _   _| | ___  ___ 
% | |_| | | | | '_ \  |  \| | | | | | '__| | | | |/ _ \/ __|
% |  _  | |_| | |_) | | |\  | |_| | | |  | |_| | |  __/\__ \
% |_| |_|\__, | .__/  |_| \_|____/  |_|   \__,_|_|\___||___/
%        |___/|_|                                           
%
% «hyp-ND-rules»  (to ".hyp-ND-rules")
% (hypp 7 "hyp-ND-rules")
% (hyp    "hyp-ND-rules")
% See: (hyp8p 37 "hyp-subst-quant-refl")
%      (hyp8     "hyp-subst-quant-refl")

{\bf hyp-ND-rules}
%
%D diagram hyp-ND-rules-fa-ex
%D 2Dx     100 +50 +50 +40 +40 +30
%D 2D  100     A0  A1  B0  B1
%D 2D
%D 2D  +25     A2  A3  B2  B3
%D 2D
%D 2D  +15     A4  A5  B4  B5
%D 2D
%D 2D  +20 C0  C1  C2  D0  D1
%D 2D
%D 2D  +25 C3  C4  C5  D2  D3
%D 2D
%D 2D  +15 C6  C7  C8  D4  D5
%D 2D
%D ren A4 A5 ==> A{×}B A
%D ren B4 B5 ==> A{×}B A
%D ren C6 C7 C8 ==> A A{×}B A
%D ren D4 D5 ==> A{×}B A
%D
%D ren A0 A1 ==>      P(a,b) ∃b⠆B.P(a,b)
%D ren A2 A3 ==> ∃b⠆B.P(a,b) ∃b⠆B.P(a,b)
%D
%D ren B0 B1 ==>      P(a,b) ∃b⠆B.P(a,b)
%D ren B2 B3 ==>        Q(a) Q(a)
%D
%D ren C0 C1 C2 ==> ∀b⠆B.R(a,b) ∀b⠆B.R(a,b) ∀b⠆B.R(a,b)
%D ren C3 C4 C5 ==>   R(a,f(a))      R(a,b) ∀b⠆B.R(a,b)
%D
%D ren D0 D1 ==> Q(a) Q(a)
%D ren D2 D3 ==> R(a,b) ∀b⠆B.R(a,b)
%D
%D (( A0 A1  A2 A3  A4 A5
%D    @ 0 @ 1 |->
%D    @ 0 @ 2  -> .plabel= l (∃Icat)
%D    @ 1 @ 3  -> .plabel= r \id
%D    @ 0 @ 3 harrownodes nil 20 nil <-|
%D    @ 2 @ 3 <-|
%D    @ 4 @ 5  -> .plabel= a π
%D ))
%D (( B0 B1  B2 B3  B4 B5
%D    @ 0 @ 1 |->
%D    @ 0 @ 2  ->
%D    @ 1 @ 3  ->
%D    @ 0 @ 3 harrownodes nil 20 nil |-> sl__ .plabel= a (∃Ecat)
%D    @ 2 @ 3 <-|
%D    @ 4 @ 5  -> .plabel= a π
%D ))
%D (( C0 C1 C2   C3 C4 C5   C6 C7 C8
%D    @ 0 @ 1 <-| @ 1 @ 2 <-|
%D    @ 0 @ 3 -> .plabel= l (∀Ecat)
%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 <-|
%D    @ 4 @ 5 |->
%D    @ 6 @ 7  -> .plabel= a \ang{\id,f}
%D    @ 7 @ 8  -> .plabel= a π
%D ))
%D (( D0 D1   D2 D3   D4 D5
%D    @ 0 @ 1 <-|
%D    @ 0 @ 2  ->
%D    @ 1 @ 3  ->
%D    @ 0 @ 3 harrownodes nil 20 nil |-> sl__ .plabel= a (∀Icat)
%D    @ 2 @ 3 |->
%D    @ 4 @ 5  -> .plabel= a π
%D ))
%D enddiagram
%D
$$\pu
  \scalebox{0.8}{$
  \diag{hyp-ND-rules-fa-ex}
  $}
$$

\newpage

{\bf hyp-ND-rules: equality}
%
%D diagram hyp-ND-rules-eq
%D 2Dx     100 +35 +35 +45
%D 2D  100 A0  A1  B0  B1
%D 2D
%D 2D  +25 A2  A3  B2  B3
%D 2D
%D 2D  +15 A4  A5  B4  B5
%D 2D
%D ren A4 A5 ==> A A{×}A
%D ren B4 B5 ==> A A{×}A
%D
%D ren A0 A1 ==> ⊤     a{=}a'
%D ren A2 A3 ==> a{=}a a{=}a'
%D
%D ren B0 B1 ==> P(a,a) a{=}a'∧P(a,a)
%D ren B2 B3 ==> P(a,a)        P(a,a')
%D
%D (( A0 A1  A2 A3  A4 A5
%D    @ 0 @ 1 |->
%D    @ 0 @ 2  -> .plabel= l (=Icat)
%D    @ 1 @ 3  -> .plabel= r \id
%D    @ 0 @ 3 harrownodes nil 20 nil <-|
%D    @ 2 @ 3 <-|
%D    @ 4 @ 5  -> .plabel= a Δ
%D ))
%D (( B0 B1  B2 B3  B4 B5
%D    @ 0 @ 1 |->
%D    @ 0 @ 2  -> .plabel= l \id
%D    @ 1 @ 3  -> .plabel= r (=Ecat)
%D    @ 0 @ 3 harrownodes nil 20 nil |->
%D    @ 2 @ 3 <-|
%D    @ 4 @ 5  -> .plabel= a Δ
%D ))
%D enddiagram
%D
$$\pu
  \diag{hyp-ND-rules-eq}
$$






\newpage

% __        ___             _                     
% \ \      / / |__  _   _  | |__  _   _ _ __  ___ 
%  \ \ /\ / /| '_ \| | | | | '_ \| | | | '_ \/ __|
%   \ V  V / | | | | |_| | | | | | |_| | |_) \__ \
%    \_/\_/  |_| |_|\__, | |_| |_|\__, | .__/|___/
%                   |___/         |___/|_|        
%
% «why-hyperdoctrines»  (to ".why-hyperdoctrines")
% (hypp 3 "why-hyperdoctrines")
% (hyp    "why-hyperdoctrines")

{\bf Why hyperdoctrines?}

A hyperdoctrine is a category in which we can

interpret first-order logic (``FOL'').

($↑$ Both Sequent Calculus and Natural Deduction!)

\msk

Hyperdoctrines are hard to define (many axioms!)

Toposes are easy to define (5 axioms!)

Every topos is a hyperdoctrine (hard to prove!)

We can interpret FOL in a topos (hard!)

We can interpret FOL in a hyperdoctrine (easy!)

\msk

Hyperdoctrines are more ``modular'' than toposes

(in the sense of \cite{Jacobs}, pages 8--11).

I have some technical and personal reasons for not

liking toposes very much --- see \cite{OchsIDARCT}, sections 12, 19,
20.

% (find-books "__cats/__cats.el" "jacobs")



\newpage

% __        ___             _                       ____  
% \ \      / / |__  _   _  | |__  _   _ _ __  ___  |___ \ 
%  \ \ /\ / /| '_ \| | | | | '_ \| | | | '_ \/ __|   __) |
%   \ V  V / | | | | |_| | | | | | |_| | |_) \__ \  / __/ 
%    \_/\_/  |_| |_|\__, | |_| |_|\__, | .__/|___/ |_____|
%                   |___/         |___/|_|                
%
% «why-hyperdoctrines-2»  (to ".why-hyperdoctrines-2")
% (hypp 4 "why-hyperdoctrines-2")
% (hyp    "why-hyperdoctrines-2")

{\bf Why hyperdoctrines? (2)}

The fibration $\Cod: \Set^\dnito → \Set$ is an

archetypal hyperdoctrine.

\msk

We can use hyperdoctrines to learn Natural Deduction!

Two of the quantifier rules in Natural Deduction

have restrictions that are very technical, and that

only made sense to me when I understood their

categorical versions!!! Or, more precisely, these adjunctions:
%
$$∃ ⊣ π^* ⊣ ∀$$

What made me understand them was the concrete example

in the next page...



\newpage

%   ___                    _          __                   _     _ 
%  / _ \ _   _  __ _ _ __ | |_ ___   / _| ___  _ __    ___| |__ (_)
% | | | | | | |/ _` | '_ \| __/ __| | |_ / _ \| '__|  / __| '_ \| |
% | |_| | |_| | (_| | | | | |_\__ \ |  _| (_) | |    | (__| | | | |
%  \__\_\\__,_|\__,_|_| |_|\__|___/ |_|  \___/|_|     \___|_| |_|_|
%                                                                  
% «quants-for-children»  (to ".quants-for-children")
% (hypp 18 "quants-for-children")
% (hyp     "quants-for-children")

{\bf Quantifiers as adjoints, for children}

\def\Lpred#1{#1}
\def\Rpred#1{#1}
\def\Lmat#1#2{\sm{#1\\#2}}
\def\Rmat#1{\sm{#1}}

A concrete example with

% $A=\{0,1,2,3,4\}$, $B=\{0,1\}$,

$X=\{0,1,2,3,4\}$, $Y=\{0,1\}$,

$P = \Lmat{00001}{00011}$, $Q = \Rmat{00111}$, $R = \Lmat{01111}{11111}$:

\msk

% (find-idarctpage 17 "13. Hyperdoctrines")
% (find-idarcttext 17 "13. Hyperdoctrines")

%D diagram quants-as-adjs-1
%D 2Dx     100 +45 +40 +45
%D 2D  100 A0  A1  B0  B1
%D 2D                    
%D 2D  +25 A2  A3  B2  B3
%D 2D                    
%D 2D  +25 A4  A5  B4  B5
%D 2D                    
%D 2D  +20 A6  A7  B6  B7
%D 2D
%D ren A0 A1 ==> \Lpred{P(a,b)} \Rpred{∃b⠆B.P(a,b)}
%D ren A2 A3 ==> \Lpred{Q(a)}   \Rpred{Q(a)}
%D ren A4 A5 ==> \Lpred{R(a,b)} \Rpred{∀b⠆B.R(a,b)}
%D ren A6 A7 ==> A{×}B A
%D
%D ren A0 A1 ==> \Lpred{P(x,y)} \Rpred{∃y⠆Y.P(x,y)}
%D ren A2 A3 ==> \Lpred{Q(x)}   \Rpred{Q(x)}
%D ren A4 A5 ==> \Lpred{R(x,y)} \Rpred{∀y⠆Y.R(x,y)}
%D ren A6 A7 ==> X{×}Y X
%D
%D ren B0 B1 ==> \Lmat{00001}{00011} \Rmat{00011}
%D ren B2 B3 ==> \Lmat{00111}{00111} \Rmat{00111}
%D ren B4 B5 ==> \Lmat{01111}{11111} \Rmat{01111}
%D ren B6 B7 ==> A{×}B A
%D ren B6 B7 ==> X{×}Y X
%D ren B6 B7 ==> \Lmat{•••••}{•••••} \Rmat{•••••}
%D
%D (( A0 A1  A2 A3  A4 A5
%D    @ 0 @ 1 |-> .plabel= a ∃
%D    @ 0 @ 2 -> @ 1 @ 3 -> @ 0 @ 3 harrownodes nil 20 nil <->
%D    @ 2 @ 3 <-| .plabel= a π^*
%D    @ 2 @ 4 -> @ 3 @ 5 -> @ 2 @ 5 harrownodes nil 20 nil <->
%D    @ 4 @ 5 |-> .plabel= a ∀
%D ))
%D (( # A6 A7 -> sl^^ .plabel= a ∃
%D    # A6 A7 <-      .plabel= m π
%D    # A6 A7 -> sl__ .plabel= b ∀
%D    A6 A7 ->  .plabel= a π
%D ))
%D
%D (( B0 B1  B2 B3  B4 B5
%D    @ 0 @ 1 |-> .plabel= a ∃
%D    @ 0 @ 2 -> @ 1 @ 3 -> @ 0 @ 3 harrownodes nil 20 nil <->
%D    @ 2 @ 3 <-| .plabel= a π^*
%D    @ 2 @ 4 -> @ 3 @ 5 -> @ 2 @ 5 harrownodes nil 20 nil <->
%D    @ 4 @ 5 |-> .plabel= a ∀
%D ))
%D (( # B6 B7 -> sl^^ .plabel= a ∃
%D    # B6 B7 <-      .plabel= m π
%D    # B6 B7 -> sl__ .plabel= b ∀
%D    B6 B7 ->  .plabel= a π
%D ))
%D enddiagram
%D
$$\pu
  \diag{quants-as-adjs-1}
$$





\newpage

%   ___            _____ _ _           
%  / _ \ _ __     | ____| (_)_ __ ___  
% | | | | '__|____|  _| | | | '_ ` _ \ 
% | |_| | | |_____| |___| | | | | | | |
%  \___/|_|       |_____|_|_|_| |_| |_|
%                                      
% «or-elim»  (to ".or-elim")

{\bf Cheap and expensive or-elimination}

One of the rules of ND that people find harder to understand

is `$∨E$', that can come in several forms...

The expensive form can have undischarged hypotheses.

The cheap form discharges the only hypothesis.





%:
%:
%:         [P]^1  R    [Q]^1   R
%:         ::::::::α   :::::::::β
%:  P{∨}Q      S           S
%:  ------------------------
%:             S
%:
%:             ^or-E-exp-1
%:
\pu
$$\ded{or-E-exp-1}$$



\newpage

%   ___                    _          __                   _     _   ____  
%  / _ \ _   _  __ _ _ __ | |_ ___   / _| ___  _ __    ___| |__ (_) |___ \ 
% | | | | | | |/ _` | '_ \| __/ __| | |_ / _ \| '__|  / __| '_ \| |   __) |
% | |_| | |_| | (_| | | | | |_\__ \ |  _| (_) | |    | (__| | | | |  / __/ 
%  \__\_\\__,_|\__,_|_| |_|\__|___/ |_|  \___/|_|     \___|_| |_|_| |_____|
%                                                                          
% «quants-for-children-2»  (to ".quants-for-children-2")

{\bf Quantifiers as adjoints, for children (2)}

$
  %\picturedotsadef{b3} (0,0)(4,5){ 2,0 3,1 4,2   1,1 2,2 3,3   0,2  1,3 2,4    1,5 }\quad
  % \picturedotsa(0,0)(4,5){ 2,0 3,1 4,2   1,1 2,2 3,3   0,2  1,3 2,4    1,5 }\quad
  b
$

$
% \picturedotsadef{b4} (0,0)(5,1){ 0,0 1,1 2,0 4,0 }\quad
a
$


\newpage

%     _                               
%    / \   _ __ _ __ _____      _____ 
%   / _ \ | '__| '__/ _ \ \ /\ / / __|
%  / ___ \| |  | | | (_) \ V  V /\__ \
% /_/   \_\_|  |_|  \___/ \_/\_/ |___/
%                                     
% «arrows»  (to ".arrows")

{\bf Arrows}

$$\scalebox{3.0}{$
  \begin{array}{cl}
  A \monicto B & \text{monic} \\
  A \ito     B & \text{inclusion} \\
  \end{array}
  $}
$$


\newpage

%  ____               _ 
% |  _ \ _ __ ___  __| |
% | |_) | '__/ _ \/ _` |
% |  __/| | |  __/ (_| |
% |_|   |_|  \___|\__,_|
%                       
% «pred»  (to ".pred")
% (hypp 6 "pred")
% (hyp    "pred")

{\bf A category of ``predicates''}

I will use `$\ito$' to denote inclusion maps in $\Set$.

The category $\Set^\dnito$ has:

inclusions as its objects, and

commutative squares as its morphisms.

A morphism $\psm{A \\ \dnito \\ B} \diagxyto/->/^{(f,g)} \psm{C \\ \dnito \\ D}$ in $\Set^\dnito$

is a commutative square
%
%D diagram pred-c-s
%D 2Dx     100 +25
%D 2D  100 A   C
%D 2D
%D 2D  +25 B   D
%D 2D
%D
%D (( A C -> .plabel= a f
%D    B D -> .plabel= a g
%D    A B `-> C D `->
%D
%D ))
%D enddiagram
%D
$\pu
  \diag{pred-c-s}
$
%
in $\Set$.

\msk

The codomain functor $\Cod: \Set^\dnito → \Set$ works like this:

\msk

$\Cod ( \psm{A \\ \dnito \\ B} ) = B$,
\;
$\Cod \left( \psm{A \\ \dnito \\ B} \diagxyto/->/^{(f,g)} \psm{C \\ \dnito \\ D} \right)
 \; = \; (B \diagxyto/->/^g D)$.



\newpage

%  ____               _ _           _                                  
% |  _ \ _ __ ___  __| (_) ___ __ _| |_ ___  ___    _____   _____ _ __ 
% | |_) | '__/ _ \/ _` | |/ __/ _` | __/ _ \/ __|  / _ \ \ / / _ \ '__|
% |  __/| | |  __/ (_| | | (_| (_| | ||  __/\__ \ | (_) \ V /  __/ |   
% |_|   |_|  \___|\__,_|_|\___\__,_|\__\___||___/  \___/ \_/ \___|_|   
%                                                                      
% «predicates-over»  (to ".predicates-over")
% (hypp 7 "predicates-over")
% (hyp    "predicates-over")

{\bf Predicates over a set}

I will draw the functor $\Cod: \Set^\dnito \to \Set$ as going downwards:

%D diagram pred-over-1
%D 2Dx     100   +25   +35
%D 2D  100 E     P --> Q
%D 2D      |     -     -
%D 2D      |     |     |
%D 2D      v     v     v
%D 2D  +30 B  CodP --> CodQ
%D 2D
%D ren E B ==> \Set^\dnito \Set
%D ren P Q CodP CodQ ==> \psmi{A}{B} \psmi{C}{D} B D
%D
%D (( E B -> .plabel= l \Cod
%D    P Q -> .plabel= a (f,g)
%D    P CodP |->
%D    Q CodQ |->
%D    CodP CodQ -> .plabel= a g
%D ))
%D enddiagram
%D
$$\pu
  \diag{pred-over-1}
$$

I will usually omit the downward `$↦$'s:

%D diagram pred-over-2
%D 2Dx     100   +25   +35
%D 2D  100 E     P --> Q
%D 2D      |     -     -
%D 2D      |     |     |
%D 2D      v     v     v
%D 2D  +30 B  CodP --> CodQ
%D 2D
%D ren E B ==> \Set^\dnito \Set
%D ren P Q CodP CodQ ==> \psmi{A}{B} \psmi{C}{D} B D
%D
%D (( E B -> .plabel= l \Cod
%D    P Q -> .plabel= a (f,g)
%D    # P CodP |->
%D    # Q CodQ |->
%D    CodP CodQ -> .plabel= a g
%D ))
%D enddiagram
%D
$$\pu
  \diag{pred-over-2}
$$


\newpage


{\bf Some standard terminology}

\ssk

(See \cite{Jacobs}, p.26, for the full definition!)

$p: \bbE → \bbB$ is a fibration (the general case),

$\Cod: \Set^\dnito→\Set$ is a fibration (our archetypal case),
%
%D diagram pred-over-3
%D 2Dx     100   +25   +35    +60
%D 2D  100 E     P --> Q      \labela
%D 2D      |     -     -
%D 2D  +12 |     |     |      \labelb
%D 2D      v     v     v
%D 2D  +12 B  CodP --> CodQ   \labelc
%D 2D
%D ren E B ==> \Set^\dnito \Set
%D ren P Q CodP CodQ ==> \psmi{A}{B} \psmi{C}{D} B D
%D
%D (( E B -> .plabel= l \Cod
%D    P Q -> .plabel= a (f,g)
%D    # P CodP |->
%D    # Q CodQ |->
%D    CodP CodQ -> .plabel= a g
%D
%D    \labela place
%D    \labelb place
%D    \labelc place
%D ))
%D enddiagram
%D
$$\pu
  \def\labela{\text{$←$ Entire category}}
  \def\labelb{\text{$←$ Projection functor}}
  \def\labelc{\text{$←$ Base category}}
  \diag{pred-over-3}
$$


$\psmi{A}{B}$ is an object ``over'' $B$,

$\psmi{A}{B} \diagxyto/->/<200>^{(f,g)} \psmi{C}{D}$ is a morphism
``over'' $B \ton{g} D$.

$\Cod^{-1}(B)$ is the \ColorRed{fiber} over $B$ (a category!)


\newpage

%  ____                                 _   _   
% |  _ \ _   _ _ __ ___  _ __ ___   ___| |_| |_ 
% | | | | | | | '_ ` _ \| '_ ` _ \ / _ \ __| __|
% | |_| | |_| | | | | | | | | | | |  __/ |_| |_ 
% |____/ \__,_|_| |_| |_|_| |_| |_|\___|\__|\__|
%                                               
% «dummett»  (to ".dummett")
% (hypp 3 "dummett")
% (hyp    "dummett")
% (find-books "__logic/__logic.el" "dummett")
% (find-dummetteipage (+ 14  88) "4.1. Natural Deduction")
% (find-dummetteipage (+ 14  89)   "logical rules")

{\bf Dummett}

The rules for the quantifiers in ND, from \cite{Dummett}, p.89:

%:
%:    Γ:A(y)         Γ:∀x\,A(x)
%:  ----------∀+     ----------∀-
%:  Γ:∀x\,A(x)         Γ:A(t)
%:
%:  ^Dum-Fa+           ^Dum-Fa-
%:
%:
%:    Γ:A(y)         Γ:∃x\,A(x)   Δ,A(y):C
%:  ----------∃+     ---------------------∃-
%:  Γ:∃x\,A(x)          Γ,Δ:C
%:
%:  ^Dum-Ex+            ^Dum-Ex-
%:
%:
\pu
$$\scalebox{0.8}{$
  \begin{array}{ccl}
  \ded{Dum-Fa+} && \ded{Dum-Fa-} \\ \\
  \ded{Dum-Ex+} && \ded{Dum-Ex-} \\
  \end{array}
  $}
$$

\msk

Let's specialize and change notation a bit...
%:
%:    P(x)⊢Q(x,y)         P(x)⊢∀y⠆Y.Q(x,y)
%:  ----------------∀+    ----------------∀-
%:  P(x)⊢∀y⠆Y.Q(x,y)       P(x)⊢Q(x,f(x))
%:
%:  ^Dum-Fa+.my            ^Dum-Fa-.my
%:
%:
%:  P(x)⊢Q(x,f(x))         P(x)⊢∃y⠆Y.Q(x,y)   R(x),Q(x,f(x))⊢S(x)
%:  -------------∃+        --------------------------------------∃-
%:  P(x)⊢∃y⠆Y.Q(x,y)       P(x),R(x)⊢S(x)
%:
%:  ^Dum-Ex+.my               ^Dum-Ex-.my                           
%:
%:
%:
\pu
$$\scalebox{0.7}{$
  \begin{array}{ccl}
  \ded{Dum-Fa+.my} && \ded{Dum-Fa-.my} \\ \\
  \ded{Dum-Ex+.my} && \ded{Dum-Ex-.my} \\
  \end{array}
  $}
$$



\newpage

% {\bf Dummett (as ND)}

{\bf The rule $∃-$ in Natural Deduction}

Let's convert the hardest rule, $∃-$, to ND...

$$\ded{Dum-Ex-.my}$$
%
% (find-es "tex" "proof")
% (find-es "tex" "proof" "\\DeduceSym")
% (find-tlfile "texmf-dist/tex/latex/lkproof/proof.sty" "\\DeduceSym")
%
%:
%:       P(x)                       \hspace{35pt}R(x)  [Q(x,f(x))]^1
%:   :::::::::::α                   :::::::::::::::::::::::::::::β
%:   ∃y⠆Y.Q(x,y)    \hspace{-40pt}      S(x)
%:   ----------------------------------∃-;1
%:              S(x)
%:
%:              ^Ex-ND-1
%:
%:
%:
%:   P(x)   R(x)
%:   :::::::::::γ
%:      S(x)
%:
%:      ^Ex-ND-2
%:
%:

It becomes:
\pu
$$\ded{Ex-ND-1}
  \Longrightarrow
  \quad
  \ded{Ex-ND-2}
$$

where:
%
$$\begin{array}{rcl}
  α &=& P(x)⊢∃y⠆Y.Q(x,y) \\
  β &=& R(x),Q(x,f(x))⊢S(x) \\
  γ &=& P(x),R(x)⊢S(x) \\
  \end{array}
$$


\newpage

{\bf A variant of the rule $∃-$}

Let's look at a simpler rule, called `$∃--$'.

%:
%:                  [Q(x,f(x))]^1
%:                  :::::::::::::δ
%:   ∃y⠆Y.Q(x,y)        S'(x)           ∃y⠆Y.Q(x,y)   
%:   -----------------------∃--;1      :::::::::::ε  
%:              S'(x)                     S'(x)       
%:                                                   
%:              ^Ex-ND-3                  ^Ex-ND-4
%:
%:   Q(x,f(x))⊢S'(x)           
%:   ----------------∃--      
%:   ∃y⠆Y.Q(x,y)⊢S'(x)         
%:
%:   ^Ex-ND-5                 
%:
\pu
$$\scalebox{0.9}{$
  \begin{array}{c}
    \ded{Ex-ND-1}
    \Longrightarrow
    \quad
    \ded{Ex-ND-2}
    \\
    \\
    \ded{Ex-ND-3}
    \quad
    \Longrightarrow
    \quad
    \ded{Ex-ND-4}
    \\
    \\
    \\
    \ded{Ex-ND-5}
  \end{array}
  $}
$$



\newpage

{\bf The rules $∃-$ and $∃--$ are ``equivalent'' (1)}

%:                       R(x),Q(x,f(x))⊢S(x)
%:                       ===================
%:                       Q(x,f(x))⊢R(x)⊸S(x)
%:                       -------------------∃--
%:  P(x)⊢∃y⠆Y.Q(x,y)     ∃y⠆Y.Q(x,y)⊢R(x)⊸S(x)
%:  --------------------------------------\text{Cut}
%:     P(x)⊢R(x)⊸S(x)
%:     ==============
%:     P(x),R(x)⊢S(x)
%:
%:     ^Dum-trans-1                        
%:
%:  P(x)⊢∃y⠆Y.Q(x,y)   Q(x,f(x))⊢S(x)
%:  ---------------------------------∃-
%:  P(x)⊢S(x)
%:
%:     ^Dum-trans-2                           
%:
%:  -----------------------
%:  ∃y⠆Y.Q(x,y)⊢∃y⠆Y.Q(x,y)   Q(x,f(x))⊢S'(x)
%:  ----------------------------------------∃-
%:  ∃y⠆Y.Q(x,y)⊢S'(x)
%:
%:     ^Dum-trans-3                   
%:
\pu
$$\begin{array}{c}
  \ded{Ex-ND-5} \\
  \\
  \ded{Dum-Ex-.my} \\
  \\
  \ded{Dum-trans-1} \\
  \end{array}
$$

\newpage

{\bf The rules $∃-$ and $∃--$ are ``equivalent'' (2)}

making $Δ:=\{\}$ instead of $Δ:=\{R(x)\}$,

and after that $P(x):=∃y⠆Y.Q(x,y)$ and $S(x):=S'(x)$,
%
$$\scalebox{0.9}{$
  \begin{array}{c}
  \ded{Ex-ND-5} \\
  \\
  \ded{Dum-Ex-.my} \\
  \\
  \ded{Dum-trans-2} \\
  \\
  \ded{Dum-trans-3} \\
  \end{array}
  $}
$$







% (find-books "__logic/__logic.el" "prawitz")
% (find-prawitzpage (+ -4  20)   "Restriction on the (Ex E)-rule")

% (find-books "__logic/__logic.el" "negri-vonplato")
% (find-negrivpspfpage (+ 19 64) "Quantifiers in natural deduction")
% (find-negrivpspftext (+ 19 64) "Quantifiers in natural deduction")

% (find-books "__logic/__logic.el" "gentzen")
% (find-gentzenpaperspage (+ 7  79)    "The three examples of" "5 1" "as NJ-derivations")
% (find-gentzenpaperstext (+ 7  79)    "The three examples of" "5 1" "as NJ-derivations")







\newpage

{\bf Predicates, visually}

% (lodp 11 "propositions-3")
% (lod     "propositions-3")


\newpage

% __        __                                        _        
% \ \      / /__    ___ __ _ _ __    _   _ ___  ___  | |_ ___  
%  \ \ /\ / / _ \  / __/ _` | '_ \  | | | / __|/ _ \ | __/ _ \ 
%   \ V  V /  __/ | (_| (_| | | | | | |_| \__ \  __/ | || (_) |
%    \_/\_/ \___|  \___\__,_|_| |_|  \__,_|___/\___|  \__\___/ 
%                                                              
% «we-can-use-to»  (to ".we-can-use-to")

{\bf We can use hyperdoctrines to understand:}

\msk

1. the rules for $∃$ in ND

2. some notations in \cite{Jacobs}

3. the internal language of a topos

4. polymorphism (as in Haskell; advanced)

\msk

We will do (1) and (2) in these notes.

\newpage

%      _           _                            _       
%     | |_   _  __| | __ _ _ __ ___   ___ _ __ | |_ ___ 
%  _  | | | | |/ _` |/ _` | '_ ` _ \ / _ \ '_ \| __/ __|
% | |_| | |_| | (_| | (_| | | | | | |  __/ | | | |_\__ \
%  \___/ \__,_|\__,_|\__, |_| |_| |_|\___|_| |_|\__|___/
%                    |___/                              
%
% «judgments»  (to ".judgments")

{\bf Judgments (for children)}

\ssk

We will interpret $a:A,b:B,P(a,b)⊢Q(a,b)$ as:

for every choice of $a∈A$,

for every choice of $b∈B$,

if $P(a,b)$ is true

then $Q(a,b)$ is true.

\msk

...or, equivalently, as:

$\setofst{(a,b)∈A×B}{P(a,b)} ⊆
 \setofst{(a,b)∈A×B}{Q(a,b)}.
$

\bsk

For variants of this and lots of fun (yeah!), see:

\url{http://angg.twu.net/LATEX/2019notes-types.pdf}

(slides 14-16).

% (ntyp 14 "set-comprehensions")
% (nty     "set-comprehensions")


\newpage

%      _           _                            _                   _   
%     | |_   _  __| | __ _ _ __ ___   ___ _ __ | |_ ___    ___ __ _| |_ 
%  _  | | | | |/ _` |/ _` | '_ ` _ \ / _ \ '_ \| __/ __|  / __/ _` | __|
% | |_| | |_| | (_| | (_| | | | | | |  __/ | | | |_\__ \ | (_| (_| | |_ 
%  \___/ \__,_|\__,_|\__, |_| |_| |_|\___|_| |_|\__|___/  \___\__,_|\__|
%                    |___/                                              
%
% «judgments-cat»  (to ".judgments-cat")
% (hypp 5 "judgments-cat")
% (hyp    "judgments-cat")

{\bf Judgments (for children, but categorically)}

\ssk

So $a:A,P(a)⊢Q(a)$ means

$\setofst{a∈A}{P(a)} ⊆
 \setofst{a∈A}{Q(a)},
$

and this is true if and only if

we have arrows `$\diagxyto/-->/<250>$' in:
%
%D diagram j-f-c-c-1
%D 2Dx     100 +30 +30
%D 2D  100 A       B
%D 2D
%D 2D  +40     C
%D 2D
%D ren A B C ==> \setofst{a{∈}A}{P(a)} \setofst{a{∈}A}{Q(a)} A
%D
%D (( A B --> A C `-> B C `->
%D
%D ))
%D enddiagram
%D
%D diagram j-f-c-c-2
%D 2Dx     100 +30 +30
%D 2D  100 A       B
%D 2D
%D 2D  +40 C       D
%D 2D
%D ren A B C D ==> \setofst{a{∈}A}{P(a)} \setofst{a{∈}A}{Q(a)} A A
%D
%D (( A B --> A C `-> B D `-> C D -> .plabel= a \id
%D
%D ))
%D enddiagram
%D
$$\pu
  \scalebox{0.8}{$
  \diag{j-f-c-c-1}
  \qquad
  \diag{j-f-c-c-2}
  $}
$$

When these arrows exist they are unique.


\newpage

%  ____               _                             ____  
% |  _ \ _ __ ___  __| |___    _____   _____ _ __  |___ \ 
% | |_) | '__/ _ \/ _` / __|  / _ \ \ / / _ \ '__|   __) |
% |  __/| | |  __/ (_| \__ \ | (_) \ V /  __/ |     / __/ 
% |_|   |_|  \___|\__,_|___/  \___/ \_/ \___|_|    |_____|
%                                                         
% «predicates-over-2»  (to ".predicates-over-2")
% (hypp 8 "predicates-over-2")
% (hyp    "predicates-over-2")

{\bf Predicates over a set (2)}

I will say that $\psmi{A}{B}$ is an object ``over'' $B$, and that

$\psmi{A}{B} \diagxyto/->/<200>^{(f,g)} \psmi{C}{D}$ is a morphism
``over'' $B \ton{g} D$.

\msk

Some standard terminology: in our particular case,

$\Cod: \Set^\dnito→\Set$ is a \ColorRed{fibration}.

$\Cod$ is the \ColorRed{projection functor}.

$\Set^\dnito$ is the \ColorRed{total category} (or the \ColorRed{entire category}).

$\Set$ is the \ColorRed{base category}.

\msk

General case (see \cite{Jacobs}, p.26, for the full definition):

$p: \bbE → \bbB$ is a \ColorRed{fibration}.

$p$ is the \ColorRed{projection functor}.

$\bbE$ is the \ColorRed{total category} (or the \ColorRed{entire category}).

$\bbB$ is the \ColorRed{base category}.






\newpage








For the general case and a formal definition see \cite{Jacobs},

page 26; he uses the notation $p: \bbE → \bbB$...

$$
  \mat{ {\Set^\dnito}            \\
        ↓ & {\hspace{-15pt}\Cod} \\
        {\Set}                   \\
      }
$$

\def\Codfibrationbody#1{
    {\Set^\dnito}           \\
    {↓} & {\hspace{#1}\Cod} \\
    {\Set}                  \\
  }
\def\pfibrationbody#1{
    {\bbE}               \\
    {↓} & {\hspace{#1}p} \\
    {\Set}               \\
  }

$$\pmat{
  hi \\
  \Set^\dnito \\
  \phantom{\Cod} \; ↓ \; \Cod \\
  \Set \\
  }
$$

$$\pmat{\pfibrationbody{-15pt}}$$


$$\def\b#1{\hspace{#1}}
 %
 \begin{array}{ccccccl}
 \Set^\dnito &      &&   \bbE &            & \text{(entire category)} \\
 ↓ & \b{-15pt}\Cod  &&   ↓ & \b{-12pt} p   & \text{(projection functor)} \\
 \Set        &      &&   \bbB &            & \text{(base category)} \\
 \end{array}
$$

\msk

% (find-jacobspage (+ 19  26)   "p: E -> B")




The functor $\pmat{\Set^\dnito \\ ↓ & \hspace{-15pt} \Cod \\ \Set}$ is a \ColorRed{fibration}.

General case: $\pmat{\bbE \\ ↓ & \hspace{-10pt} p \\ \bbB}$

% (find-books "__cats/__cats.el" "jacobs")




The \ColorRed{fiber over} an object $B$ of the \ColorRed{base
  category}




Some shorthands:

$$\pmati{\setofst{a∈A}{}}{}$$


and I will use this notation





I will draw 


\newpage


%  ____  _     ____ 
% |  _ \| |   / ___|
% | |_) | |  | |    
% |  __/| |__| |___ 
% |_|   |_____\____|
%                   
% «plc»  (to ".plc")
% (hypp 38 "plc")
% (hyp     "plc")
% (find-books "__cats/__cats.el" "seely")
% (find-seelyplcpage (+ -967 972) "1.1.2. Operators")
% (find-seelyplctext (+ -967 972) "1.1.2. Operators")

{\bf PL (1)}

$$\begin{array}[t]{rcccc}
      1 &:& \Ords \\
      Ω &:& \Ords \\
      A &:& \Ords \\
      B &:& \Ords \\
  A{×}B &:& \Ords \\
  A{→}Ω &:& \Ords \\
  \end{array}
  %
  \qquad
  %
  \begin{array}[t]{rcccc}
        ⊤ &:& Ω &:& \Ords \\
        ρ &:& Ω &:& \Ords \\
        σ &:& Ω &:& \Ords \\
        τ &:& Ω &:& \Ords \\
    σ{∧}τ &:& Ω &:& \Ords \\
    σ{⊸}τ &:& Ω &:& \Ords \\
        β &:& B &:& \Ords \\
   σ[τ/β] &:& Ω &:& \Ords \\
 Σβ{∈}B·ρ &:& Ω &:& \Ords \\
 Πβ{∈}B·τ &:& Ω &:& \Ords \\
  \end{array}
$$

\newpage

{\bf PL (1) in another notation}

$$\begin{array}[t]{rcccc}
      1 &:& Θ \\
      Ω &:& Θ \\
      A &:& Θ \\
      B &:& Θ \\
  A{×}B &:& Θ \\
  A{→}Ω &:& Θ \\
  \end{array}
  %
  \qquad
  %
  \begin{array}[t]{rcccc}
           ⊤ &:& Ω &:& Θ \\
           P &:& Ω &:& Θ \\
           Q &:& Ω &:& Θ \\
           R &:& Ω &:& Θ \\
       P{∧}Q &:& Ω &:& Θ \\
       P{⊸}Q &:& Ω &:& Θ \\
           b &:& B &:& Θ \\
  P[b:=f(a)] &:& Ω &:& Θ \\
    ∃b{∈}B.P &:& Ω &:& Θ \\
    ∀b{∈}B.R &:& Ω &:& Θ \\
  \end{array}
$$

\newpage

{\bf PL (2)}

% (find-seelyplcpage (+ -967 972) "1.1.2. Operators")
% (find-seelyplctext (+ -967 972) "1.1.2. Operators")

$$
  \begin{array}[t]{rcrccccccc}
         * &:&     ⊤ &:& Ω &:& \Ords   && ({⊤}I) \\[5pt]
     %
         a &:&     σ &:& Ω &:& \Ords \\
         b &:&     τ &:& Ω &:& \Ords \\
         c &:& σ{∧}τ &:& Ω &:& \Ords \\
      〈a,b〉 &:& σ{∧}τ &:& Ω &:& \Ords   && ({∧}I) \\
      π_1c &:&     σ &:& Ω &:& \Ords   && ({∧}E) \\
      π_2c &:&     τ &:& Ω &:& \Ords   && ({∧}E) \\[5pt]
     %
         a &:&     σ &:& Ω &:& \Ords \\
         b &:&     τ &:& Ω &:& \Ords \\
         f &:& σ{⊸}τ &:& Ω &:& \Ords \\
        fa &:&     τ &:& Ω &:& \Ords   && ({⊸}E) \\
  λx{∈}σ·b &:& σ{⊸}τ &:& Ω &:& \Ords   && ({⊸}I) \\
  \end{array}
$$

\newpage

{\bf PL (2) in another notation}

% (find-seelyplcpage (+ -967 972) "1.1.2. Operators")
% (find-seelyplctext (+ -967 972) "1.1.2. Operators")

$$
  \begin{array}[t]{rcrccccccc}
         * &:&     ⊤ &:& Ω &:& Θ   && ({⊤}I) \\[5pt]
     %
         p &:&     P &:& Ω &:& Θ \\
         q &:&     Q &:& Ω &:& Θ \\
         s &:& P{∧}Q &:& Ω &:& Θ \\
     (p,q) &:& P{∧}Q &:& Ω &:& Θ   && ({∧}I) \\
      π_1s &:&     P &:& Ω &:& Θ   && ({∧}E) \\
      π_2s &:&     Q &:& Ω &:& Θ   && ({∧}E) \\[5pt]
     %
         p &:&     P &:& Ω &:& Θ \\
         q &:&     Q &:& Ω &:& Θ \\
         f &:& P{⊸}Q &:& Ω &:& Θ \\
        fp &:&     Q &:& Ω &:& Θ   && ({⊸}E) \\
  λp{:}P.q &:& P{⊸}Q &:& Ω &:& Θ   && ({⊸}I) \\
  \end{array}
$$

\newpage

{\bf PL (3)}

% (find-seelyplcpage (+ -967 972) "1.1.2. Operators")
% (find-seelyplctext (+ -967 972) "1.1.2. Operators")

$$
  \begin{array}[t]{rcrcccccl}
                  & &        α &:& A &:& \Ords  && (\text{indet}) \\
                  & &        σ &:& Ω &:& \Ords \\
                  & &        τ &:& A &:& \Ords \\
                b &:&   σ[τ/α] &:& Ω &:& \Ords \\
             I(b) &:& Σα{∈}A·σ &:& Ω &:& \Ords  && (ΣI) \\
    I_{Σα·σ,τ}(b) &:& Σα{∈}A·σ &:& Ω &:& \Ords  && (ΣI) \\[5pt]
       %
             a &:&        σ{⊸}ρ &:& Ω &:& \Ords \\
               & &            α &:& A &:& \Ords  && (\text{indet n.f.}) \\
   𝐛Vα{∈}A·a &:& (Σα{∈}A·σ){⊸}ρ &:& Ω &:& \Ords && (ΣE) \\
  \end{array}
$$

\newpage

{\bf PL (3) in another notation}

% (find-seelyplcpage (+ -967 972) "1.1.2. Operators")
% (find-seelyplctext (+ -967 972) "1.1.2. Operators")

$$
  \begin{array}[t]{rcrcccccl}
                  & &           b &:& B &:& Θ  && (\text{indet}) \\
                  & &      P(a,b) &:& Ω &:& Θ \\
                  & &        f(a) &:& B &:& Θ \\
                p &:&   P(a,f(a)) &:& Ω &:& Θ \\
             I(p) &:& ∃b⠆B.P(a,b) &:& Ω &:& Θ  && (ΣI) \\
    I_{Σα·σ,τ}(b) &:& ∃b⠆B.P(a,b) &:& Ω &:& Θ  && (ΣI) \\[5pt]
       %
           a &:&        P(a,b){⊸}Q(a) &:& Ω &:& Θ \\
             & &                    b &:& B &:& Θ  && (\text{indet n.f.}) \\
   𝐛Vα{∈}A·a &:& (∃b⠆B.P(a,b)){⊸}Q(a) &:& Ω &:& Θ && (ΣE) \\
  \end{array}
$$

\newpage

{\bf PL (4)}

% (find-seelyplcpage (+ -967 972) "1.1.2. Operators")
% (find-seelyplctext (+ -967 972) "1.1.2. Operators")

$$
  \begin{array}[t]{rcrccccccc}
             a &:&            σ &:& Ω &:& \Ords \\
               & &            α &:& A &:& \Ords  && (\text{indet n.f.}) \\
      Λα{∈}A·a &:&     Πα{∈}A·σ &:& Ω &:& \Ords  && (ΠI) \\[5pt]
   %
             τ &:&            α &:& A &:& \Ords \\
             a &:&     Πα{∈}A·σ &:& Ω &:& \Ords \\
        a\{τ\} &:&       σ[τ/α] &:& A &:& \Ords  && (ΠE) \\
  \end{array}
$$

\newpage

{\bf PL (4) in another notation}

% (find-seelyplcpage (+ -967 972) "1.1.2. Operators")
% (find-seelyplctext (+ -967 972) "1.1.2. Operators")

% (fooi "\\Ords" "Θ")

$$
  \begin{array}[t]{rcrccccccc}
             r &:&          R(a,b) &:& Ω &:& Θ \\
               & &               b &:& B &:& Θ  && (\text{indet n.f.}) \\
            Λr &:&     ∀b⠆B.R(a,b) &:& Ω &:& Θ  && (ΠI) \\[5pt]
   %
               & &         f(a) &:& B &:& Θ \\
             g &:&  ∀b⠆B.R(a,b) &:& Ω &:& Θ \\
       g(f(a)) &:&    R(a,f(a)) &:& Ω &:& Θ  && (ΠE) \\
  \end{array}
$$




\newpage

\def\Vpred#1#2{\cmat{#2 \\ #1}}
\def\vpred#1#2{\csm {#2 \\ #1}}
\def\hpred#1#2{\setofst{#1}{#2}}

quants-my-1:

%D diagram quants-my-1
%D 2Dx     100 +50 +50
%D 2D  100 A0  A1
%D 2D
%D 2D  +30 A2  A3
%D 2D
%D 2D  +30 A4  A5
%D 2D
%D 2D  +20 B0  B1  B2
%D 2D
%D ren A0 A1 ==> \vpred{(a,b){∈}A{×}B}{P(a,b)} \vpred{a{∈}A}{∃b{∈}B.P(a,b)}
%D ren A2 A3 ==> \vpred{(a,b){∈}A{×}B}{Q(a)}   \vpred{a{∈}A}{Q(a)}
%D ren A4 A5 ==> \vpred{(a,b){∈}A{×}B}{R(a,b)} \vpred{a{∈}A}{∀b{∈}B.R(a,b)}
%D ren B0 B1 B2 ==> A{×}B A Ω
%D
%D (( A0 A1 |->
%D    A0 A2 ->
%D    A1 A3 ->
%D    A0 A3 harrownodes nil 20 nil <->
%D    A2 A3 <-|
%D    A2 A4 ->
%D    A3 A5 ->
%D    A2 A5 harrownodes nil 20 nil <->
%D    A4 A5 |->
%D
%D    B0 B1 -> .plabel= a π
%D    B1 B2 -> .plabel= a χiQ
%D    B0 B2 -> .slide= -10pt .plabel= m χiP
%D    B0 B2 -> .slide= -15pt .plabel= b χiR
%D ))
%D enddiagram
%D
$$\pu
  \diag{quants-my-1}
$$




\newpage

quants-my-2:

%D diagram quants-my-2
%D 2Dx     100 +30 +30
%D 2D  100 A0  A1
%D 2D
%D 2D  +25 A2  A3
%D 2D
%D 2D  +25 A4  A5
%D 2D
%D 2D  +20 B0  B1  B2
%D 2D
%D ren A0 A1 ==> P ∃_πP
%D ren A2 A3 ==> π^*Q Q
%D ren A4 A5 ==> Q ∀_πQ
%D ren B0 B1 B2 ==> A{×}B A Ω
%D
%D (( A0 A1 |->
%D    A0 A2 ->
%D    A1 A3 ->
%D    A0 A3 harrownodes nil 20 nil <->
%D    A2 A3 <-|
%D    A2 A4 ->
%D    A3 A5 ->
%D    A2 A5 harrownodes nil 20 nil <->
%D    A4 A5 |->
%D
%D    B0 B1 -> .plabel= a π
%D    B1 B2 -> .plabel= a χiQ
%D    B0 B2 -> .slide= -10pt .plabel= m χiP
%D    B0 B2 -> .slide= -15pt .plabel= b χiR
%D ))
%D enddiagram
%D
$$\pu
  \diag{quants-my-2}
$$




\newpage

quants-seely-1:

%D diagram quants-seely-1
%D 2Dx     100 +30 +30
%D 2D  100 A0  A1
%D 2D
%D 2D  +25 A2  A3
%D 2D
%D 2D  +25 A4  A5
%D 2D
%D 2D  +20 B0  B1  B2
%D 2D
%D ren A0 A1 ==> ρ Σβ{∈}B·ρ
%D ren A2 A3 ==> π^*σ σ
%D ren A4 A5 ==> τ Πβ{∈}B·τ
%D ren B0 B1 B2 ==> A{×}B A Ω
%D
%D (( A0 A1 |->
%D    A0 A2 ->
%D    A1 A3 ->
%D    A0 A3 harrownodes nil 20 nil <->
%D    A2 A3 <-|
%D    A2 A4 ->
%D    A3 A5 ->
%D    A2 A5 harrownodes nil 20 nil <->
%D    A4 A5 |->
%D
%D    B0 B1 -> .plabel= a π
%D    B1 B2 -> .plabel= a σ
%D    B0 B2 -> .slide= -10pt .plabel= m ρ
%D    B0 B2 -> .slide= -15pt .plabel= b τ
%D ))
%D enddiagram
%D
$$\pu
  \diag{quants-seely-1}
$$




\newpage

{\bf The rules for `$∃$' in Natural Deduction}

The rules are easier to understand and visualize

if we use bounded quantifiers and finite sets...

Bounded: $∃y⠆Y.P(x,y)$

Unbounded: $∃y.P(x,y)$

Finite sets: $X=\{1,2,3,4,5,6\}$, $Y=\{0,1,2\}$





% (find-books "__logic/__logic.el" "prawitz")
% (find-prawitzpage (+ -4  19) "The corresponding natural deduction is given below")



$\pmat{A \\ \dnito \\ B \\}
 \psm {A \\ \dnito \\ B \\}
 \Set^\dnito
$

$\mathsf{Cod}: \Set^\dnito \to \Set$

$\cmat{P(a) \\ a∈A} := \pmat {\setofst{a∈A}{P(a)} \\ \dnito \\ A \\}$

% (find-books "__cats/__cats.el" "jacobs")
% (find-jacobspage (+ 19  11)   "Pred")
% (find-jacobspage (+ 19  27)   "cartesian lifting")
% (find-jacobspage (+ 19  19) "1. Introduction to fibred category theory")
% (find-jacobspage (+ 19  19)   "simple slice categories")
% (find-jacobspage (+ 19  20) "1.1. Fibrations")
% (find-jacobspage (+ 19  22)   "Sets^\\to")
% (find-jacobspage (+ 19  23)   "cod: Sets^\\to -> Sets")




I learned hyperdoctrines




\end{document}

%  __  __       _        
% |  \/  | __ _| | _____ 
% | |\/| |/ _` | |/ / _ \
% | |  | | (_| |   <  __/
% |_|  |_|\__,_|_|\_\___|
%                        
% «make»  (to ".make")
% (find-LATEX "2019ilha-grande-poster-a4.tex")
% (find-LATEX "2019ilha-grande-poster-a4.tex" "write-poster-body")

 (eepitch-shell)
 (eepitch-kill)
 (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2020hyp veryclean
make -f 2019.mk STEM=2020hyp pdf
# (hypp)
# (hypp 25)



% Local Variables:
% coding: utf-8-unix
% ee-tla: "hyp"
% End:
