Index of the slides:

Hyperdoctrines: subobjects and change-of-base . . . . . . . . . . . . . . . . . . . . . . . . . .2 Hyperdoctrine: definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Quantifiers as adjoints: an example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Preservations by change-of-base: overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 Preservation of ‘true’ and ‘and’ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Preservation of ‘false’ and ‘or’ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 Preservation of ‘implies’ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 BCC for ‘forall’ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 BCC for ‘exists’ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .10 BCC for equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Frobenius for ‘exists’ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Frobenius for equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13 Frobenius for exists-equal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 From “constructions” to “intuitionistic proofs”, and back . . . . . . . . . . . . . . 15 The adjunction functors as sequent rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 The adjunction functors as sequent rules (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 The adjunction maps as sequent rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 The adjunction maps as sequent rules (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 The adjunction functors as ND proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .20 The adjunction functors as ND proofs (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 The adjunction maps as ND proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 The adjunction maps as ND proofs (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 The adjunction maps as ND proofs (3) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 The Frobenius maps as ND proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Frobenius for equality (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 Dependent equality from simple equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Hyperdoctrines: substitution, quantifiers, reflexivity . . . . . . . . . . . . . . . . . . . . 28 Transitivity of equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .29 Hyperdoctrines: symmetry, transitivity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .30 Weak and strong exists-elim . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Rules in ND and sequent calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Rules, categorically . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 First preservations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 First preservations (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Hyperdoctrines: subobjects and change-of-base Our archetypal hyperdoctrine is this:

Cod : Sub(Set) → Set
(A′ ↣ A) ↦ A

A linguistic trick: everything will simplify A LOT if we pretend that all subobject are subsets. Another shorthand: ‘P ’ instead of ‘P (a)’.

\begin{matrix}(\{|a | P |\} ↣ A) & ↦ & A \\ (\{|a | P |\} ↣ \{|a|\}) & ↦ & \{|a|\} \\ \{|a ∥ P |\} & ↦ & \{|a|\} \\ (a∥P) & ⇒ & a \end{matrix}

We will downcase the projection functor, Cod, to (a∥P) ⇒ a. We will often draw it vertically and omit the ‘a∥’ and the ‘⇒’:

[figure: {|a ∥ P |}; A; a∥P; a; P; a; P; a]

The change-of-base functors in Cod : Sub(Set) → Set are induced by pullbacks:

[figure: \{|a | P (f(a))|\}; \{|a | P (b)|\}; f′; \{|a | P (f(a))|\}; A; f^{∗}P; \{|a | P (b)|\}; B; P; A; B; f; f^{∗}; A; B; f; f^{∗}P; P; \overline{f}P ≡(f′,f); f^{∗}P; P; f^{∗}; f^{∗}P; A; Cod; P; B; Cod; A; B; f]

The map \overline{f}P : \{|a ∥ P (f(a))|\} → \{|b ∥ P (b)|\} corresponds to a pullback square in Sub(Set). It is a cartesian map in the fibration Cod : Sub(Set) → 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:

[figure: P fa; P b; □; P fa; P b; a; b; f; P; P; □; P; P; a; b]

Hyperdoctrine: 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

obeying Beck-Chevalley and Frobenius,

(v) each change-of-base functor has a right adjoint obeying Beck-Chevalley and Frobenius.

The base category is (bi)cartesian closed:

[figure: a; b; a; b, c; a; c; b; b, c; b, c; c; a; a ⊔ b; a ⊔ b; b; a; c; a ⊔ b; c; b; c; a; ∗; ⊥; a; a, b; a; a, b; c; a; b↦c; c; b↦c]

Each fiber is bicartesian closed:

P Q [figure] [figure]P Q&R [figure] P  R [figure] [figure] Q  Q&R [figure] Q&R  R [figure] P  P ∨ Q [figure] P ∨ Q  Q [figure] P  R [figure] [figure] P ∨ Q R[figure]  Q R [figure] [figure]  P ⊤[figure] ⊥ P[figure] P &Q  P [figure] P &Q R[figure]  P Q [figure]R [figure] R  Q [figure]R [figure] [figure] [figure]

Left adjoints (∃/&=/∃=) and right adjoints (∀/ [figure]=/∀=) for change-of-base functors:

P ab  ∃b.P ab [figure] P ab Qa [figure] ∃b.P ab Qa [figure] [figure] [figure] Qa  Qa [figure] Qa Rab [figure]  Qa ∀b.Rab [figure] [figure] [figure] Rab  ∀b.Rab [figure] a, b  a [figure]  P ab b=b′&P abb [figure] P ab Qabb [figure] b=b′&P abb Qabb′ [figure] [figure] [figure] Qabb  Qabb′ [figure] Qabb Rab [figure]  Qabb′ b=b′ [figure]Rab [figure] [figure] [figure] Rab b=b′ [figure]Rab [figure] a, b  a, b, b′ [figure]  P a  ∃a.b=fa&P b [figure] P a Qfa [figure]  ∃a.b=fa&P b Qb [figure] [figure] [figure] Qfa  Qb [figure] Qfa Ra [figure]  Qb ∀a.b=fa [figure]P b [figure] [figure] [figure] Ra  ∀a.b=fa [figure]P b [figure] a  b_{f}  [figure]

Quantifiers as adjoints: an example ‘∃’ and ‘∀’ are left and right adjoint to change-of-base along a projection A × B → A... That this is true is far from obvious, so let’s look at an example. If A ≡ ^{••• •••} and

B ≡ \begin{matrix}• \\ • \end{matrix}, then

A × B ≡ \begin{matrix}••• ••• \\ ••• ••• \end{matrix};

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:

[figure: \{|a, b∥P (a, b)|\}; \{|a∥∃b.P (a, b)|\}; \{|a, b∥P (a, b)|\}; \{|a, b∥Q(a)|\}; \{|a∥∃b.P (a, b)|\}; \{|a∥Q(a)|\}; \{|a, b∥Q(a)|\}; \{|a∥Q(a)|\}; \{|a, b∥Q(a)|\}; \{|a, b∥R(a, b)|\}; \{|a∥Q(a)|\}; \{|a∥∀b.R(a, b)|\}; \{|a, b∥R(a, b)|\}; \{|a∥∀b.R(a, b)|\}; A×B; A; {100 000 \atop 110 000}; 110 000; {100 000 \atop 110 000}; {111 000 \atop 111 000}; 110 000; 111 000; {111 000 \atop 111 000}; 111 000; {111 000 \atop 111 000}; {111 100 \atop 111 110}; 111 000; 111 100; {111 100 \atop 111 110}; 111 100; A×B; A]

Later we will see that ‘∃ ⊣ π^{∗} ⊣ ∀’ holds even when the logic is just intuitionistic — and we will use this to “define” ∃ and ∀ in hyperdoctrines...

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.

Preservations by change-of-base: overview Start with f : A → B, and {|b ∥ P (b)|} and {|b ∥ Q(b)|}.

There are two different categorical ways to build an object that “deserves the name” {|a ∥ P (f(a))&Q(f(a))|}.

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 ⊤, ⊥, &, ∨, [figure], that this natural half-side of the iso will have an inverse.

More precisely:

f^{∗}⊤_{B} ⊤_{A}_{♮=!} [figure] f^{∗}⊤_{B} ⊤_{A} [figure]_{P⊤}  ⊥_{A} f^{∗}⊥_{B}_{♮=!} [figure] ⊥_{A} f^{∗}⊥_{B} [figure]_{P⊥} f^{∗}P &f^{∗}Q  f^{∗}(P &Q) [figure]_{♮=⟨f^{∗}π,f^{∗}π′⟩} f^{∗}P &f^{∗}Q  f^{∗}(P &Q)_{P&}  [figure] f^{∗}P ∨ f^{∗}Q  f^{∗}(P ∨ Q)_{♮=[f^{∗}ι,f^{∗}ι′]} [figure] f^{∗}P ∨ f^{∗}Q  f^{∗}(P ∨ Q) [figure] _{P∨}  f^{∗}(P [figure]Q) f^{∗}P [figure]f^{∗}Q_{♮=...} [figure] f^{∗}(P [figure]Q) f^{∗}P [figure]f^{∗}Q [figure]_{P [figure]}

We will see the diagrams for these constructions in the next slides. The natural half for ‘ [figure]’, in particular, is a big construction.

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.

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:

[figure: b, (c, d); (b, c), d; ♮; b, (c, d); (b, c), d; Frob]

Preservation of ‘true’ and ‘and’

[figure: ⊤; ⊤; ⊤; ⊤; ♮; ⊤; ⊤; P⊤; a; b; P; P; P; P &Q; P; P &Q; P; P &Q; P &Q; P &Q; ♮; P &Q; P &Q; P&; P &Q; P &Q; P &Q; Q; P &Q; Q; P &Q; Q; Q; Q; a; b]

[figure: f^{∗}⊤_{B}; ⊤_{B}; f^{∗}⊤_{B}; ⊤_{A}; ♮; f^{∗}⊤_{B}; ⊤_{A}; P⊤; A; B; f; f^{∗}P; P; f^{∗}P; f^{∗}P &f^{∗}Q; f^{∗}P; f^{∗}(P &Q); P; P &Q; f^{∗}P &f^{∗}Q; f^{∗}(P &Q); ♮; f^{∗}P &f^{∗}Q; f^{∗}(P &Q); P&; f^{∗}(P &Q); P &Q; f^{∗}P &f^{∗}Q; f^{∗}Q; f^{∗}(P &Q); f^{∗}Q; P &Q; Q; f^{∗}Q; Q; A; B; f]

Preservation of ‘false’ and ‘or’

[figure: ⊥; ⊥; ⊥; ⊥; ♮; ⊥; ⊥; P⊥; a; b; P; P; P; P ∨ Q; P; P ∨ Q; P; P ∨ Q; P ∨ Q; P ∨ Q; ♮; P ∨ Q; P ∨ Q; P∨; P ∨ Q; P ∨ Q; P ∨ Q; Q; P ∨ Q; Q; P ∨ Q; Q; Q; Q; a; b]

[figure: f^{∗}⊥_{B}; ⊥_{B}; ⊥_{A}; f^{∗}⊥_{B}; ♮; ⊥_{A}; f^{∗}⊥_{B}; P⊥; a; b; f^{∗}P; P; f^{∗}P; f^{∗}P ∨ f^{∗}Q; f^{∗}P; f^{∗}(P ∨ Q); P; P ∨ Q; f^{∗}P ∨ f^{∗}Q; f^{∗}(P ∨ Q); ♮; f^{∗}P ∨ f^{∗}Q; f^{∗}(P ∨ Q); P∨; f^{∗}(P ∨ Q); P ∨ Q; f^{∗}P ∨ f^{∗}Q; f^{∗}Q; f^{∗}(P ∨ Q); f^{∗}Q; P ∨ Q; Q; f^{∗}Q; Q; a; b]

Preservation of ‘implies’

(P [figure]Q)&P  (P [figure]Q)&P [figure] ^{♮} (P [figure]Q)&P  (P [figure]Q)&P_{P&} [figure] (P [figure]Q)&P  (P [figure]Q)&P [figure] (P [figure]Q)&P Q[figure]  (P [figure]Q)&P Q [figure] [figure]  (P [figure]Q)&P Q[figure] Q  Q [figure] (P [figure]Q)&P  P [figure]Q [figure] [figure] Q  P [figure]Q [figure] [figure]  (P [figure]Q)&P  P [figure]Q [figure] [figure] Q  P [figure]Q [figure] [figure] P [figure]Q  P [figure]Q [figure]  P [figure]Q P [figure]Q_{id} [figure] P [figure]Q P [figure]Q_{♮} [figure] P [figure]Q P [figure]Q [figure]_{P [figure]} [figure] [figure] [figure]  [figure] [figure] a  b [figure]

f^{∗}(P [figure]Q)&f^{∗}P  f^{∗}((P [figure]Q)&P) [figure]^{♮} f^{∗}(P [figure]Q)&f^{∗}P  f^{∗}((P [figure]Q)&P)_{P&} [figure] f^{∗}((P [figure]Q)&P)  (P [figure]Q)&P [figure] f^{∗}(P [figure]Q)&f^{∗}P f^{∗}Q [figure]  f^{∗}((P [figure]Q)&P) f^{∗}Q [figure] [figure]  (P [figure]Q)&P Q[figure] f^{∗}Q  Q [figure] f^{∗}(P [figure]Q)&f^{∗}P  f^{∗}(P [figure]Q) [figure] [figure] f^{∗}Q  f^{∗}P [figure]f^{∗}Q [figure] [figure]  (P [figure]Q)&P  P [figure]Q [figure] [figure] Q  P [figure]Q [figure] [figure] f^{∗}(P [figure]Q)  P [figure]Q [figure]  P [figure]Q P [figure]Q_{id} [figure] f^{∗}(P [figure]Q) f^{∗}P [figure]f^{∗}Q_{♮} [figure] f^{∗}(P [figure]Q) f^{∗}P [figure]f^{∗}Q [figure]_{P [figure]} [figure] [figure] [figure]  [figure] [figure] A  B_{f}  [figure]

BCC for ‘forall’

[figure: ∀c.P; ∀c.P; ∀c.P; ∀c.P; ∀c.P; P; ∀c.P; P; ∀c.P; P; P; P; ∀c.P; ∀c.P; P; ∀c.P; ∀c.P; ∀c.P; P; ∀c.P; ∀c.P; ∀c.P; ∀c.P; ∀c.P; id; ∀c.P; ∀c.P; ♮; ∀c.P; ∀c.P; BCC∀; a, c; b, c; a, c; a; b, c; b; a; b]

[figure: c^{′∗}f^{∗}∀_{c}P; f^{′∗}c^{∗}∀_{c}P; f^{′∗}c^{∗}∀_{c}P; c^{∗}∀_{c}P; c^{′∗}f^{∗}∀_{c}P; f^{′∗}P; f^{′∗}c^{∗}∀_{c}P; f^{′∗}P; c^{∗}∀_{c}P; P; f^{′∗}P; P; c^{′∗}f^{∗}∀_{c}P; f^{∗}∀_{c}P; f^{′∗}P; ∀_{c′}f^{′∗}P; c^{∗}∀_{c}P; ∀_{c}P; P; ∀_{c}P; f^{∗}∀_{c}P; ∀_{c}P; ∀_{c}P; ∀_{c}P; id; f^{∗}∀_{c}P; ∀_{c′}f^{′∗}P; ♮; f^{∗}∀_{c}P; ∀_{c′}f^{′∗}P; BCC∀; A×C; B×C; f′; A×C; A; c′; B×C; B; c; A; B; f]

BCC for ‘exists’

[figure: P; P; P; ∃c.P; P; ∃c.P; P; ∃c.P; ∃c.P; ∃c.P; ∃c.P; ∃c.P; P; ∃c.P; P; ∃c.P; ∃c.P; ∃c.P; ∃c.P; ∃c.P; ∃c.P; ∃c.P; ∃c.P; ∃c.P; id; ∃c.P; ∃c.P; ♮; ∃c.P; ∃c.P; BCC∃; a, c; b, c; a, c; a; b, c; b; a; b]

[figure: f^{′∗}P; P; f^{′∗}P; c^{′∗}f^{∗}∃_{c}P; f^{′∗}P; f^{′∗}c^{∗}∃_{c}P; P; c^{∗}∃_{c}P; c^{′∗}f^{∗}∃_{c}P; f^{′∗}c^{∗}∃_{c}P; f^{′∗}c^{∗}∃_{c}P; c^{∗}∃_{c}P; f^{′∗}P; ∃_{c′}f^{′∗}P; P; ∃_{c}P; c^{′∗}f^{∗}∃_{c}P; f^{∗}∃_{c}P; c^{∗}∃_{c}P; ∃_{c}P; f^{∗}∃_{c}P; ∃_{c}P; ∃_{c}P; ∃_{c}P; id; ∃_{c′}f^{′∗}P; f^{∗}∃_{c}P; ♮; ∃_{c′}f^{′∗}P; f^{∗}∃_{c}P; BCC∃; A×C; B×C; f′; A×C; A; c′; B×C; B; c; A; B; f]

BCC for equality

[figure: P; P; P; c=c&P; P; c=c&P; P; c=c&P; c=c&P; c=c&P; c=c&P; c=c&P; P; c=c′&P; P; c=c′&P; c=c&P; c=c′&P; c=c&P; c=c′&P; c=c′&P; c=c′&P; c=c′&P; c=c′&P; id; c=c′&P; c=c′&P; ♮; c=c′&P; c=c′&P; BCC∃; a, c; b, c; a, c; a, c, c′; b, c; b, c, c′; a, c, c′; b, c, c′]

[figure: f^{′∗}P; P; f^{′∗}P; c^{′∗}f^{∗}Eq_{c}P; f^{′∗}P; f^{′∗}c^{∗}Eq_{c}P; P; c^{∗}Eq_{c}P; c^{′∗}f^{∗}Eq_{c}P; f^{′∗}c^{∗}Eq_{c}P; f^{′∗}c^{∗}Eq_{c}P; c^{∗}Eq_{c}P; f^{′∗}P; Eq_{c′}f^{′∗}P; P; Eq_{c}P; c^{′∗}f^{∗}Eq_{c}P; f^{∗}Eq_{c}P; c^{∗}Eq_{c}P; Eq_{c}P; f^{∗}Eq_{c}P; Eq_{c}P; Eq_{c}P; Eq_{c}P; id; Eq_{c′}f^{′∗}P; f^{∗}Eq_{c}P; ♮; Eq_{c′}f^{′∗}P; f^{∗}Eq_{c}P; BCC=; A×C; B×C; f′; A×C; A×C×C; c′; B×C; B×C×C; c; A×C×C; B×C×C; f]

Frobenius for ‘exists’

[figure: P; ∃c.P; P &Q; P; ∃c.(P &Q); ∃c.P; (∃c.P)&Q; ∃c.P; Q; Q; P &Q; Q; ∃c.(P &Q); Q; (∃c.P)&Q; Q; P &Q; ∃c.(P &Q); ∃c.(P &Q); (∃c.P)&Q; ♮; ∃c.(P &Q); (∃c.P)&Q; Frob∃; b, c; b]

[figure: P; ∃_{c}P; P &c^{∗}Q; P; ∃_{c}(P &c^{∗}Q); ∃_{c}P; (∃_{c}P)&Q; ∃_{c}P; c^{∗}Q; Q; P &c^{∗}Q; c^{∗}Q; ∃_{c}(P &c^{∗}Q); Q; (∃_{c}P)&Q; Q; P &c^{∗}Q; ∃_{c}(P &c^{∗}Q); ∃_{c}(P &c^{∗}Q); (∃_{c}P)&Q; ♮; ∃_{c}(P &c^{∗}Q); (∃_{c}P)&Q; Frob∃; B×C; B; c]

Frobenius for equality

[figure: P; c=c′&P; P &Q; P; c=c′&(P &Q); c=c′&P; (c=c′&P)&Q; c=c′&P; Q; Q; P &Q; Q; c=c′&(P &Q); Q; (c=c′&P)&Q; Q; P &Q; c=c′&(P &Q); c=c′&(P &Q); (c=c′&P)&Q; ♮; c=c′&(P &Q); (c=c′&P)&Q; Frob=; b, c; b, c, c′]

[figure: P; Eq_{c}P; P &c^{∗}Q; P; Eq_{c}(P &c^{∗}Q); Eq_{c}P; (Eq_{c}P)&Q; Eq_{c}P; c^{∗}Q; Q; P &c^{∗}Q; c^{∗}Q; Eq_{c}(P &c^{∗}Q); Q; (Eq_{c}P)&Q; Q; P &c^{∗}Q; Eq_{c}(P &c^{∗}Q); Eq_{c}(P &c^{∗}Q); (Eq_{c}P)&Q; ♮; Eq_{c}(P &c^{∗}Q); (Eq_{c}P)&Q; Frob=; B×C; B×C×C; c]

Frobenius for exists-equal

[figure: P a; ∃a.b=fa&P a; P a&Qfa; P a; ∃a.b=fa&(P a&Qfa); ∃a.b=fa&P a; (∃a.b=fa&P a)&Qb; ∃a.b=fa&P a; Qfa; Qb; P a&Qfa; Qfa; ∃a.b=fa&(P a&Qfa); Qb; (∃a.b=fa&P a)&Qb; Qb; P a&Qfa; ∃a.b=fa&(P a&Qfa); ∃a.b=fa&(P a&Qfa); (∃a.b=fa&P a)&Qb; ♮; ∃a.b=fa&(P a&Qfa); (∃a.b=fa&P a)&Qb; Frob∃=; a; b]

[figure: P; Eq_{f}P; P &f^{∗}Q; P; Eq_{f}(P &f^{∗}Q); Eq_{f}P; (Eq_{f}P)&Q; Eq_{f}P; f^{∗}Q; Q; P &f^{∗}Q; f^{∗}Q; Eq_{f}(P &f^{∗}Q); Q; (Eq_{f}P)&Q; Q; P &f^{∗}Q; Eq_{f}(P &f^{∗}Q); Eq_{f}(P &f^{∗}Q); (Eq_{f}P)&Q; ♮; Eq_{f}(P &f^{∗}Q); (Eq_{f}P)&Q; Frob∃=; A; B; f]

From “constructions” to “intuitionistic 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...

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.

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.

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...

But we need concrete examples to start with.

The adjunction functors as sequent rules

\begin{matrix}P &Q  P [figure] P &Q R[figure]  P Q [figure]R [figure] R  Q [figure]R [figure] [figure]_{♭}_{♯} [figure] & \begin{matrix}{P ⊢ P′ \atop P &Q ⊢ P′&Q} & &Q \\ {R ⊢ R′ \atop Q [figure]R ⊢ Q [figure]R′} & Q [figure] \end{matrix} \\ [figure: (P, Q); P ∨ Q; (P, Q); (R, R); P ∨ Q; R; (R, R); R; (R, R); (S, T); R; S&T; (S, T); S&T; ♭; ♯; ♭; ♯] & \begin{matrix}\begin{matrix}P ⊢ P′ & Q ⊢ Q′ \\ P ∨ Q ⊢ P′ ∨ Q′ \end{matrix} & ∨ \\ {R ⊢ R′ \atop (R ⊢ R′), (R ⊢ R′)} & K \\ \begin{matrix}S ⊢ S′ & T ⊢ T′ \\ S&T ⊢ S′&T′ \end{matrix} & & \end{matrix} \\ [figure: P ab; ∃b.P ab; P ab; Qa; ∃b.P ab; Qa; Qa; Qa; Qa; Rab; Qa; ∀b.Rab; Rab; ∀b.Rab; ♭; ♯; ♭; ♯; a, b; a] & \begin{matrix}{P ab ⊢ P′ab \atop ∃b.P ab ⊢ ∃b.P′ab} & ∃ \\ {Qa ⊢ Q′a \atop Qa ⊢ Q′a} & W \\ {Rab ⊢ R′ab \atop ∀b.Rab ⊢ ∀b.R′ab} & ∀ \end{matrix} \end{matrix}

The adjunction functors as sequent rules (2)

\begin{matrix}P ab  b=b′&P ab [figure] P ab Qabb [figure]  b=b′&P ab Qabb′ [figure] Qabb  Qabb′ [figure] Qabb Rab [figure]  Qabb′ b=b′ [figure]Rab [figure] Rab  b=b′ [figure]Rab [figure]_{♭} [figure] [figure]_{♯} [figure]_{♭}_{♯} [figure] a, b  a, b, b′ [figure] & \begin{aligned}{P ab ⊢ P′ab \atop b=b′&P ab ⊢ b=b′&P ab} & = & \\ {Qabb′ ⊢ Q′abb′ \atop Qabb ⊢ Q′abb} & (b′ := b) \\ {Rab ⊢ R′ab \atop b=b′ [figure]Rab ⊢ b=b′ [figure]R′ab} & = [figure] \end{aligned} \\ P a  ∃a.b=fa&P ab [figure] P a Qfa [figure] ∃a.b=fa&P ab Qb [figure] Qfa  Qb [figure] Qfa Ra [figure]  Qb ∀a.b=fa [figure]Ra [figure] Ra  ∀a.b=fa [figure]Ra [figure]_{♭} [figure] [figure]_{♯} [figure]_{♭}_{♯} [figure] a  b [figure] & \begin{matrix}{P a ⊢ P′a \atop ∃a.b=fa&P b ⊢ ∃a.b=fa&.P b} & ∃ = \\ {Qb ⊢ Q′b \atop Qfa ⊢ Q′fa} & (b := fa) \\ {Ra ⊢ R′a \atop ∀a.b=fa [figure]Ra ⊢ ∀a.b=fa [figure]R′a} & ∀ = \end{matrix} \end{matrix}

The adjunction maps as sequent rules

\begin{matrix}P &Q  P [figure] P &Q R[figure]  P Q [figure]R [figure] R  Q [figure]R [figure] [figure]_{♭}_{♯} [figure] & {P &Q ⊢ R \atop P ⊢ Q [figure]R} ^{Cur^{♯}}  {P ⊢ Q [figure]R \atop P &Q ⊢ R} ^{Cur^{♭}} \\ [figure: (P, Q); P ∨ Q; (P, Q); (R, R); P ∨ Q; R; (R, R); R; (R, R); (S, T); R; S&T; (S, T); S&T; ♭; ♯; ♭; ♯] & \begin{matrix}\begin{matrix}P ⊢ R & Q ⊢ R \\ P ∨ Q ⊢ R \end{matrix} ∨^{♭} & {P ∨ Q ⊢ R \atop P ⊢ R} ∨_{1}^{♯} {P ∨ Q ⊢ R \atop Q ⊢ R} ∨_{2}^{♯} \\ \begin{matrix}R ⊢ S & R ⊢ T \\ T ⊢ S&T \end{matrix} ∨^{♯} & {R ⊢ S&T \atop R ⊢ S} ∨_{1}^{♭} {R ⊢ S&T \atop R ⊢ T} ∨_{2}^{♭} \end{matrix} \\ [figure: P ab; ∃b.P ab; P ab; Qa; ∃b.P ab; Qa; Qa; Qa; Qa; Rab; Qa; ∀b.Rab; Rab; ∀b.Rab; ♭; ♯; ♭; ♯; a, b; a] & \begin{matrix}{P ab ⊢ Qa \atop ∃b.P ab ⊢ Qa} ∃^{♭} & {∃b.P ab ⊢ Qa \atop P ab ⊢ Qa} ∃^{♯} \\ {Qa ⊢ Rab \atop Qa ⊢ ∀b.Rab} ∀^{♯} & {Qa ⊢ ∀b.Rab \atop Qa ⊢ Rab} ∀^{♭} \end{matrix} \end{matrix}

The adjunction maps as sequent rules (2)

\begin{matrix}P ab  b=b′&P ab [figure] P ab Qabb [figure]  b=b′&P ab Qabb′ [figure] Qabb  Qabb′ [figure] Qabb Rab [figure]  Qabb′ b=b′ [figure]Rab [figure] Rab  b=b′ [figure]Rab [figure]_{♭} [figure] [figure]_{♯} [figure]_{♭}_{♯} [figure] a, b  a, b, b′ [figure] & \begin{matrix}{P ab ⊢ Qabb \atop b=b′&P ab ⊢ Qabb′} = &^{♭} & {b=b′&P ab ⊢ Qabb′ \atop P ab ⊢ Qabb} = &^{♯} \\ {Qabb ⊢ Rab \atop Qabb′ ⊢ b=b′ [figure]Rab} = [figure]^{♯} & {Qabb′ ⊢ b=b′ [figure]Rab \atop Qabb ⊢ Rab} = [figure]^{♭} \end{matrix} \\ P a  ∃a.b=fa&P ab [figure] P a Qfa [figure] ∃a.b=fa&P ab Qb [figure] Qfa  Qb [figure] Qfa Ra [figure]  Qb ∀a.b=fa [figure]Ra [figure] Ra  ∀a.b=fa [figure]Ra [figure]_{♭} [figure] [figure]_{♯} [figure]_{♭}_{♯} [figure] a  b [figure] & \begin{matrix}{P a ⊢ Qfa \atop ∃a.b=fa&P ab ⊢ Qb} ∃ =^{♭} & {∃a.b=fa&P ab ⊢ Qb \atop P a ⊢ Qfa} ∃ =^{♯} \\ {Qfa ⊢ Ra \atop Qb ⊢ ∀a.b=fa [figure]Ra} = [figure]^{♯} & {Qb ⊢ ∀a.b=fa [figure]Ra \atop Qfa ⊢ Ra} = [figure]^{♭} \end{matrix} \end{matrix}

The adjunction functors as ND proofs

\begin{matrix}P &Q  P [figure] P &Q R[figure]  P Q [figure]R [figure] R  Q [figure]R [figure] [figure]_{♭}_{♯} [figure] & \begin{matrix}{P &Q \atop P} &E_{1} ; ⋮ . ; P′ & {P &Q \atop Q} &E_{2} \\ P′&Q \end{matrix} ; &I  \begin{aligned}[Q]^{1} & Q [figure]R \\ & R \end{aligned} [figure]E ; ⋮ . ; R′ ; Q [figure]R′ ; [figure]I; 1 \\ [figure: (P, Q); P ∨ Q; (P, Q); (R, R); P ∨ Q; R; (R, R); R; (R, R); (S, T); R; S&T; (S, T); S&T; ♭; ♯; ♭; ♯] & \begin{aligned}P ∨ Q & [P]^{1} ; ⋮ . ; P′ ; P′ ∨ Q′ ∨I_{1} & [Q]^{1} ; ⋮ . ; Q′ ; P′ ∨ Q′ ∨I_{2} \\ & P′ ∨ Q′ \end{aligned} ; ∨E  \begin{matrix}{S&T \atop S} &E_{1} ; ⋮ . ; S′ & {S&T \atop T} &E_{2} ; ⋮ . ; T′ \\ S′&T′ \end{matrix} ; &I \\ [figure: P ab; ∃b.P ab; P ab; Qa; ∃b.P ab; Qa; Qa; Qa; Qa; Rab; Qa; ∀b.Rab; Rab; ∀b.Rab; ♭; ♯; ♭; ♯; a, b; a] & \begin{matrix}∃b.P ab & [P ab]^{1} ; ⋮ . ; P′ab ; ∃b.P′ab ∃I \\ ∃b.P′ab \end{matrix} ; ∃E  \begin{aligned}[b]^{1} & ∀b.Rab \\ & Rab \end{aligned} ∀E ; ⋮ . ; R′ab ; ∀b.R′ab ; ∀I; 1 \end{matrix}

The adjunction functors as ND proofs (2)

\begin{matrix}P ab  b=b′&P ab [figure] P ab Qabb [figure]  b=b′&P ab Qabb′ [figure] Qabb  Qabb′ [figure] Qabb Rab [figure]  Qabb′ b=b′ [figure]Rab [figure] Rab  b=b′ [figure]Rab [figure]_{♭} [figure] [figure]_{♯} [figure]_{♭}_{♯} [figure] a, b  a, b, b′ [figure] & \begin{matrix}{b=b′&P ab \atop b=b′} &E_{1} & {b=b′&P ab \atop P ab} &E_{2} ; ⋮ . ; P′ab \\ b=b′&P′ab \end{matrix} ; ? ; \begin{aligned}[b=b′]^{1} & b=b′ [figure]Rab \\ & Rab \end{aligned} [figure]E ; ⋮ . ; R′ab ; b=b′ [figure]Rab ; [figure]I; 1 \\ P a  ∃a.b=fa&P ab [figure] P a Qfa [figure] ∃a.b=fa&P ab Qb [figure] Qfa  Qb [figure] Qfa Ra [figure]  Qb ∀a.b=fa [figure]Ra [figure] Ra  ∀a.b=fa [figure]Ra [figure]_{♭} [figure] [figure]_{♯} [figure]_{♭}_{♯} [figure] a  b [figure] & \begin{matrix}∃a.fa = b&P a & \begin{matrix}{[fa = b&P a]^{1} \atop fa = b} &E_{1} & {[fa = b&P a]^{1} \atop P a} &E_{2} ; ⋮ . ; P′a \\ fa = b&P′a \end{matrix} ; &I ; ∃a.fa = b&P′a ; ∃I \\ ∃a.fa = b&P′a \end{matrix} ; ∃E; 1 ; \begin{aligned}[fa = b]^{1} & {∀a.fa = b [figure]Ra \atop fa = b [figure]Ra} \\ & Ra \end{aligned} ; ⋮ . ; R′a ; fa = b [figure]R′a ; 1 ; ∀a.fa = b [figure]R′a \end{matrix}

The adjunction maps as ND proofs

\begin{matrix}P &Q  P [figure] P &Q R[figure]  P Q [figure]R [figure] R  Q [figure]R [figure] [figure]_{♭}_{♯} [figure] & \begin{matrix}P & [Q]^{1} \\ P &Q \end{matrix} &I ; ⋮ . ; R ; Q [figure]R ; ( [figure]I)  \begin{matrix}{P &Q \atop Q} &E_{2} & {P &Q \atop P} &E_{1} ; ⋮ . ; Q [figure]R \\ R \end{matrix} ; [figure]E \\ [figure: (P, Q); P ∨ Q; (P, Q); (R, R); P ∨ Q; R; (R, R); R; (R, R); (S, T); R; S&T; (S, T); S&T; ♭; ♯; ♭; ♯] & \begin{matrix}\begin{aligned}P ∨ Q & [P]^{1} ; ⋮ . ; R & [Q]^{1} ; ⋮ . ; R \\ & R \end{aligned}∨E & {P \atop P ∨ Q} ∨I_{1} ; ⋮ . ; R {Q \atop P ∨ Q} ∨I_{2} ; ⋮ . ; R \\ \begin{matrix}R ; ⋮ . ; S & R ; ⋮ . ; T \\ S&T \end{matrix} &I & R ; ⋮ . ; S&T ; S &E_{1} R ; ⋮ . ; S&T ; T &E_{2} \end{matrix} \\ [figure: P ab; ∃b.P ab; P ab; Qa; ∃b.P ab; Qa; Qa; Qa; Qa; Rab; Qa; ∀b.Rab; Rab; ∀b.Rab; ♭; ♯; ♭; ♯; a, b; a] & \begin{matrix}\begin{matrix}∃b.P ab & [P ab]^{1} ; ⋮ . ; Qa \\ Qa \end{matrix} ; ∃E & {P ab \atop ∃b.P ab} ∃I ; ⋮ . ; Qa \\ \begin{matrix}Qa & [Qa]^{1} ; ⋮ . ; Rab \\ ∀b.Rab \end{matrix} ∀I & \begin{aligned}b & Qa ; ⋮ . ; ∀b.Rab \\ & Rab \end{aligned} ∀E \end{matrix} \end{matrix}

The adjunction maps as ND proofs (2)

P ab  b=b′&P ab [figure] P ab Qabb [figure]  b=b′&P ab Qabb′ [figure] Qabb  Qabb′ [figure] Qabb Rab [figure]  Qabb′ b=b′ [figure]Rab [figure] Rab  b=b′ [figure]Rab [figure]_{♭} [figure] [figure]_{♯} [figure]_{♭}_{♯} [figure] a, b  a, b, b′ [figure]

\begin{matrix}\begin{matrix}{b=b′&P ab \atop b=b′} &E_{1} & {b=b′&P ab \atop P ab} &E_{2} ; ⋮ . ; Qabb \\ Qabb′ \end{matrix} ; = E & \begin{matrix}b = b = I & \begin{matrix}[b=b′]^{1} & P ab \\ b=b′&P ab \end{matrix} ; ⋮ . ; Qabb′ \\ Qabb \end{matrix} ; b′ := b; 1 \\ \begin{matrix}[b=b′]^{1} & Qabb′ \\ Qabb \end{matrix} ? ; ⋮ . ; Rab ; b=b′ [figure]Rab ; [figure]I; 1 & \begin{aligned}b = b = I & Qabb & \begin{aligned}[b=b′]^{1} & [Qabb′]^{1} ; ⋮ . ; b=b′ [figure]Rab \\ & Rab \end{aligned} [figure]E \\ & Rab \end{aligned} ; b′ := b; 1 \end{matrix}

The adjunction maps as ND proofs (3)

P a  ∃a.b=fa&P ab [figure] P a Qfa [figure] ∃a.b=fa&P ab Qb [figure] Qfa  Qb [figure] Qfa Ra [figure]  Qb ∀a.b=fa [figure]Ra [figure] Ra  ∀a.b=fa [figure]Ra [figure]_{♭} [figure] [figure]_{♯} [figure]_{♭}_{♯} [figure] a  b [figure]

\begin{aligned}∃a.b=fa&P a & \begin{matrix}{[b=fa&P a]^{1} \atop b=fa} & {[b=fa&P a]^{1} \atop P a} ; ⋮ . ; Qfa \\ Qb \end{matrix} \\ & Qb \end{aligned} ; 1 \begin{aligned}fa = fa & \begin{matrix}[b=fa]^{1} & \begin{matrix}[b=fa]^{1} & P a \\ b=fa&P a \end{matrix} ; ∃a.b=fa&P a ; ⋮ . ; Qb \\ Qfa \end{matrix} \\ & Qfa \end{aligned}

\begin{matrix}\begin{matrix}[fa = b]^{1} & Qb \\ Qfa \end{matrix} ; ⋮ . ; Ra ; fa = b [figure]Ra & 1 \\ ∀a.fa = b [figure]Ra \end{matrix}  \begin{aligned}fa = fa & \begin{aligned}Qfa & \begin{matrix}\begin{matrix}[Qfa′]^{2} & [Qb]^{1} ; ⋮ . ; ∀a.fa = b [figure]Ra \\ ∀a.fa = fa′ [figure]Ra \end{matrix} & 1 \\ fa = fa [figure]Ra \end{matrix} \\ & fa = fa [figure]Ra \end{aligned} ; 2 \\ & Ra \end{aligned}

The Frobenius maps as ND proofs The preservations of ⊤, ⊥, &, ∨, [figure]are all trivially true intuitionistically, as they are all of the form α ⊢ α...

Same for Beck-Chevalley.

The ♮ arrows whose inverses are the Frobenius maps can be constructed from operations whose translations to Intuitionistic Logic we have already seen.

[figure: ∃_{π}(P &π^{∗}Q); (∃_{π}P)&Q; ♮; ∃_{π}(P &π^{∗}Q); (∃_{π}P)&Q; Frob∃; ∃b.(P ab&Qa); (∃b.P ab)&Qa; ♮; ∃b.(P ab&Qa); (∃b.P ab)&Qa; Frob∃; Eq_{δ}(P &δ^{∗}Q); (Eq_{δ}P)&Q; ♮; Eq_{δ}(P &δ^{∗}Q); (Eq_{δ}P)&Q; Frob=; b=b′&(P abb&Qab); (b=b′&P abb)&Qab; ♮; b=b′&(P abb&Qab); (b=b′&P abb)&Qab; Frob=; ∃=_{f}(P &f^{∗}Q); (∃=_{f}P)&Q; ♮; ∃=_{f}(P &f^{∗}Q); (∃=_{f}P)&Q; Frob∃=; ∃a.b=fa&(P a&Qfa); (∃a.b=fa&P a)&Qb; ♮; ∃a.b=fa&(P a&Qfa); (∃a.b=fa&P a)&Qb; Frob∃=]

We need to show that the Frobenius maps “hold intuitionistically”.

Here is a ND proof for the first case: (the other cases are similar - and the trees are big)

\begin{matrix}{(∃b.P ab)&Qa \atop ∃b.P ab} &E_{1} & \begin{matrix}[P ab]^{1} & {(∃b.P ab)&Qa \atop Qa} &E_{2} \\ P ab&Qa \end{matrix} ; &I ; ∃b.(P ab&Qa) ; ∃I \\ ∃b.(P ab&Qa) \end{matrix} ; ∃E; 1

Frobenius for equality (2) (Now we will start to see consequences of the structure)

If we have Eq⊤ and Frobenius, then we have EqP:

[figure: ⊤; Eq⊤; ⊤&δ^{∗}π^{∗}P; ⊤; Eq(⊤&δ^{∗}π^{∗}P); Eq⊤; Eq⊤&π^{∗}P; Eq⊤; ⊤&δ^{∗}π^{∗}P; Eq(⊤&δ^{∗}π^{∗}P); Eq(⊤&δ^{∗}π^{∗}P); Eq⊤&π^{∗}P; ♮; Eq(⊤&δ^{∗}π^{∗}P); Eq⊤&π^{∗}P; Frob; ⊤&δ^{∗}π^{∗}P; δ^{∗}π^{∗}P; Eq(⊤&δ^{∗}π^{∗}P); Eq(δ^{∗}π^{∗}P); Eq(⊤&δ^{∗}π^{∗}P); π^{∗}P; Eq⊤&π^{∗}P; π^{∗}P; δ^{∗}π^{∗}P; π^{∗}P; π^{∗}P; P; δ^{∗}π^{∗}P; P; δ^{∗}π^{∗}P; Eq(δ^{∗}π^{∗}P); Eq(δ^{∗}π^{∗}P); EqP; P; EqP; A×B; A×B×B; δ; A×B×B; A×B; π]

[figure: ⊤; b=b′&⊤; ⊤&P; ⊤; b=b′&(⊤&P); b=b′&⊤; (b=b′&⊤)&P; b=b′&⊤; ⊤&P; b=b′&(⊤&P); b=b′&(⊤&P); (b=b′&⊤)&P; ♮; b=b′&(⊤&P); (b=b′&⊤)&P; Frob; ⊤&P; P; b=b′&(⊤&P); b=b′&P; b=b′&(⊤&P); P; (b=b′&⊤)&P; P; P; P; P; P; P; P; P; b=b′&P; b=b′&P; b=b′&P; P; b=b′&P; a, b; a, b, b′; a, b, b′; a, b]

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.

Dependent equality from simple equality

[figure: ⊤; π_{2}^{∗}⊤; ♮; ⊤; π_{2}^{∗}⊤; P⊤; ⊤; δ^{∗}π_{23}^{∗}Eq⊤; π_{2}^{∗}⊤; π_{2}^{∗}δ^{∗}Eq⊤; δ^{∗}π_{23}^{∗}Eq⊤; π_{2}^{∗}δ^{∗}Eq⊤; ⊤; δ^{∗}Eq⊤; π_{2}^{∗}⊤; ⊤; π_{2}^{∗}δ^{∗}Eq⊤; δ^{∗}Eq⊤; ⊤; Eq_{δ′}⊤_{A×B}; ⊤; Eq⊤; δ^{∗}π_{23}^{∗}Eq⊤; π_{23}^{∗}Eq_{δ}⊤_{B}; δ^{∗}Eq⊤; Eq⊤; π_{23}^{∗}Eq_{δ}⊤_{B}; Eq⊤; Eq⊤; Eq⊤; id; Eq_{δ′}⊤_{A×B}; π_{23}^{∗}Eq_{δ}⊤_{B}; ♮; Eq_{δ′}⊤_{A×B}; π_{23}^{∗}Eq_{δ}⊤_{B}; BCC∃; A×B; B; π_{2}; A×B; A×B×B; δ′; B; B×B; δ; A×B×B; B×B; π_{23}]

[figure: ⊤; ⊤; ♮; ⊤; ⊤; P⊤; ⊤; b = b; ⊤; b = b; b = b; b = b; ⊤; b = b; ⊤; ⊤; b = b; b = b; ⊤; b=b′; ⊤; b=b′; b = b; b=b′; b = b; b=b′; b=b′; b=b′; b=b′; b=b′; id; b=b′; b=b′; ♮; b=b′; b=b′; BCC∃; a, b; b; a, b; a, b, b′; b; b, b′; a, b, b′; b, b′]

Transitivity of equality

[figure: δ^{′∗}π_{24}^{∗}Eq_{δ}⊤; Eq_{δ′}δ^{′∗}π_{24}^{∗}Eq_{δ}⊤; δ^{′∗}π_{24}^{∗}Eq_{δ}⊤; δ^{′∗}π_{24}^{∗}Eq_{δ}⊤; id; Eq_{δ′}δ^{′∗}π_{24}^{∗}Eq_{δ}⊤; π_{24}^{∗}Eq_{δ}⊤; δ^{′∗}π_{24}^{∗}Eq_{δ}⊤; π_{24}^{∗}Eq_{δ}⊤; ⊤; Eq_{δ}⊤; π_{24}^{∗}Eq_{δ}⊤; Eq_{δ}⊤; (A×B)×B; ((A×B)×B)×B; δ′; A×B; (A×B)×B; δ; ((A×B)×B)×B; (A×B)×B; π_{24}; b=b′; b′=b′′&b=b′; b=b′; b=b′; id; b′=b′′&b=b′; b=b′′; b=b′; b=b′′; ⊤; b=b′′; b=b′′; b=b′′; (a, b), b′; ((a, b), b′), b′′; b′′:=b′; a, b; (a, b), b′′; b′′:=b; ((a, b), b′), b′′; (a, b), b′′]

Hyperdoctrines: substitution, quantifiers, reflexivity The substitution rule:

[figure: (\begin{matrix}P \\ a, c \end{matrix}); (\begin{matrix}P \\ b, c \end{matrix}); (\begin{matrix}P \\ a, c \end{matrix}); (\begin{matrix}P \\ b, c \end{matrix}); □; (\begin{matrix}P \\ a, c \end{matrix}); _{(\begin{matrix}Q \\ b, c \end{matrix})}; a,c;P ⊢Q; (\begin{matrix}P \\ b, c \end{matrix}); _{(\begin{matrix}Q \\ b, c \end{matrix})}; b,c;P ⊢Q; _{(\begin{matrix}Q \\ b, c \end{matrix})}; _{(\begin{matrix}Q \\ b, c \end{matrix})}; _{(\begin{matrix}Q \\ b, c \end{matrix})}; _{(\begin{matrix}Q \\ b, c \end{matrix})}; □; a, c; b, c; a, c; a; b, c; b; a; b; a⊢b]

The ‘(∀I)’ and ‘(∀E)’ rules:

[figure: (\begin{matrix}P \\ a, c \end{matrix}); (\begin{matrix}P \\ b, c \end{matrix}); (\begin{matrix}P \\ a, c \end{matrix}); (\begin{matrix}P \\ b, c \end{matrix}); □; (\begin{matrix}P \\ a, c \end{matrix}); _{(\begin{matrix}Q \\ b, c \end{matrix})}; a,b;P ⊢Q; (\begin{matrix}P \\ b, c \end{matrix}); _{(\begin{matrix}∀b.Q \\ b, c \end{matrix})}; a;P ⊢∀b.Q; _{(\begin{matrix}Q \\ b, c \end{matrix})}; _{(\begin{matrix}∀b.Q \\ b, c \end{matrix})}; a, b; a; (\begin{matrix}P \\ a \end{matrix}); (\begin{matrix}P \\ a, b \end{matrix}); (\begin{matrix}P \\ a \end{matrix}); (\begin{matrix}P \\ a, b \end{matrix}); □; (\begin{matrix}P \\ a, b \end{matrix}); (\begin{matrix}P \\ a \end{matrix}); (\begin{matrix}P \\ a, b \end{matrix}); (\begin{matrix}P \\ a \end{matrix}); □; (\begin{matrix}P \\ a \end{matrix}); _{(\begin{matrix}Q \\ a \end{matrix})}; a;Q⊢R; (\begin{matrix}P \\ a, b \end{matrix}); _{(\begin{matrix}Q \\ a, b \end{matrix})}; (\begin{matrix}P \\ a \end{matrix}); _{(\begin{matrix}∀b.Q \\ a \end{matrix})}; a;Q⊢∀b.R; _{(\begin{matrix}Q \\ a \end{matrix})}; _{(\begin{matrix}Q \\ a, b \end{matrix})}; _{(\begin{matrix}Q \\ a \end{matrix})}; _{(\begin{matrix}Q \\ a, b \end{matrix})}; □; _{(\begin{matrix}Q \\ a, b \end{matrix})}; _{(\begin{matrix}∀b.Q \\ a \end{matrix})}; a; a, b; a⊢b; a, b; a]

The ‘(∃E)’ and ‘(∃I)’ rules:

[figure: (\begin{matrix}P \\ a, b \end{matrix}); (\begin{matrix}∃b.P \\ a \end{matrix} ); (\begin{matrix}P \\ a, b \end{matrix}); (\begin{matrix}∃b.P \\ a \end{matrix} ); co□; (\begin{matrix}P \\ a, b \end{matrix}); _{(\begin{matrix}Q \\ b, c \end{matrix})}; a,b;P ⊢Q; (\begin{matrix}∃b.P \\ a \end{matrix} ); _{(\begin{matrix}Q \\ a, b \end{matrix})}; a;∃b.P ⊢Q; _{(\begin{matrix}Q \\ b, c \end{matrix})}; _{(\begin{matrix}Q \\ a, b \end{matrix})}; _{(\begin{matrix}Q \\ b, c \end{matrix})}; _{(\begin{matrix}Q \\ a, b \end{matrix})}; □; a, b; a; (\begin{matrix}P \\ a \end{matrix}); (\begin{matrix}P \\ a, b \end{matrix}); (\begin{matrix}P \\ a \end{matrix}); (\begin{matrix}P \\ a, b \end{matrix}); □; (\begin{matrix}P \\ a, b \end{matrix}); (\begin{matrix}∃b.P \\ a \end{matrix} ); (\begin{matrix}P \\ a, b \end{matrix}); (\begin{matrix}∃b.P \\ a \end{matrix} ); co□; (\begin{matrix}P \\ a \end{matrix}); _{(\begin{matrix}∃b.P \\ a \end{matrix} )}; a;P ⊢∃b.P; (\begin{matrix}P \\ a, b \end{matrix}); _{(\begin{matrix}∃b.P \\ a, b \end{matrix} )}; (\begin{matrix}∃b.P \\ a \end{matrix} ); _{(\begin{matrix}∃b.P \\ a \end{matrix} )}; id; _{(\begin{matrix}∃b.P \\ a \end{matrix} )}; _{(\begin{matrix}∃b.P \\ a, b \end{matrix} )}; _{(\begin{matrix}∃b.P \\ a \end{matrix} )}; _{(\begin{matrix}∃b.P \\ a, b \end{matrix} )}; □; _{(\begin{matrix}∃b.P \\ a, b \end{matrix} )}; _{(\begin{matrix}∃b.P \\ a \end{matrix} )}; _{(\begin{matrix}∃b.P \\ a, b \end{matrix} )}; _{(\begin{matrix}∃b.P \\ a \end{matrix} )}; □; a; a, b; a⊢b; a, b; a]

The “reflexivity” rule for equality (on variables):

[figure: (\begin{matrix}⊤ \\ a, b \end{matrix}); (\begin{matrix}b=b′ \\ a, b, b′ \end{matrix}); (\begin{matrix}⊤ \\ a, b \end{matrix}); (\begin{matrix}b=b′ \\ a, b, b′ \end{matrix}); co□; (\begin{matrix}⊤ \\ a, b \end{matrix}); _{(\begin{matrix}b=b \\ a, b \end{matrix})}; a,b;⊤⊢(b=b); (\begin{matrix}b=b′ \\ a, b, b′ \end{matrix}); _{(\begin{matrix}b=b′ \\ a, b, b′ \end{matrix})}; id; _{(\begin{matrix}b=b \\ a, b \end{matrix})}; _{(\begin{matrix}b=b′ \\ a, b, b′ \end{matrix})}; _{(\begin{matrix}b=b \\ a, b \end{matrix})}; _{(\begin{matrix}b=b′ \\ a, b, b′ \end{matrix})}; □; a, b; a, b, b′; b′:=b]

Hyperdoctrines: symmetry, transitivity The “symmetry” rule for equality (on variables):

[figure: (\begin{matrix}⊤ \\ a, b \end{matrix}); (\begin{matrix}b=b′ \\ a, b, b′ \end{matrix}); (\begin{matrix}⊤ \\ a, b \end{matrix}); (\begin{matrix}b=b′ \\ a, b, b′ \end{matrix}); co□; (\begin{matrix}⊤ \\ a, b \end{matrix}); _{(\begin{matrix}b=b \\ a, b \end{matrix})}; refl; (\begin{matrix}b=b′ \\ a, b, b′ \end{matrix}); _{(\begin{matrix}b′=b \\ a, b, b′ \end{matrix})}; a,b,b′;(b=b′)⊢(b′=b); _{(\begin{matrix}b=b \\ a, b \end{matrix})}; _{(\begin{matrix}b′=b \\ a, b, b′ \end{matrix})}; _{(\begin{matrix}b=b \\ a, b \end{matrix})}; _{(\begin{matrix}b′=b \\ a, b, b′ \end{matrix})}; □; _{(\begin{matrix}b′=b \\ a, b, b′ \end{matrix})}; _{(\begin{matrix}b′=b \\ a, b′, b \end{matrix})}; _{(\begin{matrix}b′=b \\ a, b, b′ \end{matrix})}; _{(\begin{matrix}b′=b \\ a, b′, b \end{matrix})}; □; _{(\begin{matrix}⊤ \\ a, b′ \end{matrix})}; _{(\begin{matrix}b′=b \\ a, b′, b \end{matrix})}; _{(\begin{matrix}⊤ \\ a, b′ \end{matrix})}; _{(\begin{matrix}b′=b \\ a, b′, b \end{matrix})}; co□; a, b; a, b, b′; b′:=b; a, b, b′; a, b′, b; a, b′; a, b′, b; b′:=b]

The “transitivity” rule for equality (on variables):

[figure: (\begin{matrix}b=b′ \\ a, b, b′ \end{matrix}); (\begin{matrix}b′=b′′&b=b′ \\ a, b, b′, b′′ \end{matrix}); (\begin{matrix}b=b′ \\ a, b, b′ \end{matrix}); (\begin{matrix}b′=b′′&b=b′ \\ a, b, b′, b′′ \end{matrix}); co□; (\begin{matrix}b=b′ \\ a, b, b′ \end{matrix}); _{(\begin{matrix}b=b′ \\ a, b, b′ \end{matrix})}; id; (\begin{matrix}b′=b′′&b=b′ \\ a, b, b′, b′′ \end{matrix}); _{(\begin{matrix}b=b′′ \\ a, b, b′, b′′ \end{matrix})}; a,b,b′,b′′;(b′=b′′)&(b=b′)⊢(b=b′′); _{(\begin{matrix}b=b′ \\ a, b, b′ \end{matrix})}; _{(\begin{matrix}b=b′′ \\ a, b, b′, b′′ \end{matrix})}; _{(\begin{matrix}b=b′ \\ a, b, b′ \end{matrix})}; _{(\begin{matrix}b=b′′ \\ a, b, b′, b′′ \end{matrix})}; □; _{(\begin{matrix}b=b′′ \\ a, b, b′, b′′ \end{matrix})}; _{(\begin{matrix}b=b′′ \\ a, b′, b′′ \end{matrix})}; _{(\begin{matrix}b=b′′ \\ a, b, b′, b′′ \end{matrix})}; _{(\begin{matrix}b=b′′ \\ a, b′, b′′ \end{matrix})}; □; _{(\begin{matrix}⊤ \\ a, b \end{matrix})}; _{(\begin{matrix}b=b′′ \\ a, b′, b′′ \end{matrix})}; _{(\begin{matrix}⊤ \\ a, b \end{matrix})}; _{(\begin{matrix}b=b′′ \\ a, b′, b′′ \end{matrix})}; co□; a, b, b′; a, b, b′, b′′; b′′:=b′; a, b, b′, b′′; a, b′, b′′; a, b; a, b′, b′′; b′′:=b]

Weak and strong exists-elim 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:

\begin{matrix}∃b.P (a, b) & [P (a, b)]^{1} Q(a) ; ⋮ . ; R(a) \\ R(a) \end{matrix} ; 1; (∃E^{+})  {a, b; P (a, b), Q(a) ⊢ R(a) \atop a; ∃b.P (a, b), Q(a) ⊢ R(a)} (∃E^{+})

\begin{matrix}∃b.P (a, b) & [P (a, b)]^{1} ; ⋮ . ; Q(a) \\ Q(a) \end{matrix} ; 1; (∃E^{−})  {a, b; P (a, b) ⊢ Q(a) \atop a; ∃b.P (a, b) ⊢ Q(a)} (∃E^{−})

(∃E^{−}) is a particular case of (∃E^{+}) — take Q(a) := ⊤ in (∃E^{+}).

In the presence of ( [figure]) the rule (∃E^{−}) implies (∃E^{+}):

\begin{aligned}Q(a) & \begin{matrix}∃b.P (a, b) & [P (a, b)]^{2} [Q(a)]^{1} ; ⋮ . ; R(a) ; Q(a) [figure]R(a) ; 1; ( [figure]I) \\ Q(a) [figure]R(a) \end{matrix} ; 2; (∃E^{+}) \\ & R(a) \end{aligned} ; ( [figure]E)

(∃E^{−}), categorically:

[figure: P (a, b); ∃b.P (a, b); P (a, b); Q(a); ∃b.P (a, b); Q(a); Q(a); Q(a); a, b; a]

(∃E^{+}), categorically:

P (a, b)&Q(a)  P (a, b) [figure] P (a, b)  ∃b.P (a, b) [figure] ∃b.P (a, b)  (∃b.P (a, b))&Q(a) [figure] P (a, b)&Q(a) R(a) [figure]  P (a, b) Q(a) [figure]R(a) [figure]  ∃b.P (a, b) Q(a) [figure]R(a) [figure]  (∃b.P (a, b))&Q(a) R(a) [figure] [figure]  [figure]  [figure] R(a)  Q(a) [figure]R(a) [figure] Q(a) [figure]R(a)  Q(a) [figure]R(a) [figure] Q(a) [figure]R(a)  R(a) [figure] a, b  a, b a, b  a [figure] a  a

Note that O[(\begin{matrix}Q(a) [figure]R(a) \\ a, b \end{matrix})] has two constructions,

with a hidden iso between them.

Rules in ND and sequent calculus The rules, in natural deduction form ((∀E) is wrong):

\begin{matrix}\begin{matrix}P ; ⋮ . ; Q & P ; ⋮ . ; R \\ Q&R \end{matrix} (&I) & P {Q&R \atop Q} (&E_{1}) ; ⋮ . ; S  P {Q&R \atop R} (&E_{2}) ; ⋮ . ; S \\ P [Q]^{1} ; ⋮ . ; R ; Q [figure]R1; ( [figure]I) & \begin{aligned}P ; ⋮ . ; Q & P ; ⋮ . ; Q [figure]R \\ & R \end{aligned} ( [figure]E) \\ P (a) ; ⋮ . ; Q(a, b) ; ∀b.Q(a, b) (∀I) & \begin{matrix}a ; ⋮ . ; f(a) & Q(a) ; ⋮ . ; ∀b.R(a, b) \\ R(a, f(a)) \end{matrix} (∀E) \\ Q(a) ; ⋮ . ; P (a, f(a)) ; ∃b.P (a, b) (∃I) & \begin{matrix}∃b.P (a, b) & [P (a, b)]^{1} Q(a) ; ⋮ . ; R(a) \\ R(a) \end{matrix} ; (∃E) \end{matrix}

The rules, in sequent calculus form ((∀E) is wrong):

\begin{matrix}\begin{matrix}P ⊢ Q & P ⊢ R \\ P ⊢ Q&R \end{matrix} (&I) & {P, Q ⊢ S \atop P, Q&R ⊢ S} (&E_{1}) {P, R ⊢ S \atop P, Q&R ⊢ S} (&E_{2}) \\ {P, Q ⊢ R \atop P ⊢ Q [figure]R} ( [figure]I) & \begin{aligned}P ⊢ Q & P ⊢ Q [figure]R \\ & P ⊢ R \end{aligned} ( [figure]E) \\ {a, b; P (a) ⊢ Q(a, b) \atop a; P (a) ⊢ ∀b.Q(a, b)} (∀I) & \begin{matrix}a ⊢ f(a) & a; Q(a) ⊢ ∀b.R(a, b) \\ a; Q(a) ⊢ R(a, f(a)) \end{matrix} (∀E) \\ {a; Q(a) ⊢ P (a, f(a)) \atop a; Q(a) ⊢ ∃b.P (a, b)} (∃I) & {a, b; P (a, b), Q(a) ⊢ R(a) \atop a; ∃b.P (a, b), Q(a) ⊢ R(a)} (∃E) \end{matrix}

Rules, categorically The rules, categorically ((&E) needs explanations, (∀E) is wrong):

[figure: P; Q; P; Q&R; P; R; Q; Q&R; π; Q&R; R; π′; Q; Q&R; π; Q&R; R; π′; Q; P &Q; Q&R; P &Q&R; R; P &R; P &Q; P &Q&R; P &Q&R; P &R]

P &Q  P [figure] P &Q R[figure]  P Q [figure]R [figure] [figure] R  Q [figure]R [figure]  P Q [figure] [figure] P (Q [figure]R)&Q [figure] P  Q [figure]R [figure] [figure] Q  (Q [figure]R)&Q [figure]_{π′} (Q [figure]R)&Q Q [figure]R_{π} [figure] (Q [figure]R)&Q Q [figure]R [figure] (Q [figure]R)&Q R[figure]  Q [figure]R Q [figure]R_{id} [figure] [figure] R  Q [figure]R [figure]

[figure: Q(a); Q(a); Q(a); R(a, b); Q(a); ∀b.R(a, b); R(a, b); ∀b.R(a, b); a, b; a; Q(a); Q(a); Q(a); Q(a); Q(a); R(a, f(a)); Q(a); R(a, b); Q(a); ∀b.R(a, b); R(a, f(a)); R(a, b); R(a, b); ∀b.R(a, b); a; a, b; b:=f(a); a, b; a]

[figure: P (a, f(a)); P (a, b); P (a, b); ∃b.P (a, b); P (a, f(a)); ∃b.P (a, b); P (a, b); ∃b.P (a, b); ∃b.P (a, b); ∃b.P (a, b); ∃b.P (a, b); ∃b.P (a, b); ∃b.P (a, b); ∃b.P (a, b); a; a, b; b:=f(a); a, b; a]  (see next page)