Index of the slides:

The BiCCC structure and the classifier axiom . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 The pre-hyperdoctrine structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Two CCompC structures in a topos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Basic constructions with NNOs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 NNOs: the morphism κ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 The BiCCC structure and the classifier axiom

CCC: [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]

HA: 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]

Topos:

[figure: (a, b)|_{c}; b; (a, b)|_{c}; a; b; c; a; c; a|_{P}; ∗; a|_{P}; a; ∗; ω; ⊤; a; ω; P]

The pre-hyperdoctrine structure Hyperdoctrine:

[figure: _{(\begin{matrix}P \\ a \end{matrix})}; _{(\begin{matrix}P \\ b \end{matrix} )}; _{(\begin{matrix}P \\ a \end{matrix})}; _{(\begin{matrix}P \\ b \end{matrix} )}; □; a; b; (\begin{matrix}P \\ a, b \end{matrix}); (\begin{matrix}b=b′&P \\ a, b, b′ \end{matrix} ); (\begin{matrix}P \\ a, b \end{matrix}); (\begin{matrix}b=b′&P \\ a, b, b′ \end{matrix} ); co□; _{(\begin{matrix}Q[b, b] \\ a, b \end{matrix})}; _{(\begin{matrix}Q[b, b′] \\ a, b, b′ \end{matrix})}; _{(\begin{matrix}Q[b, b] \\ a, b \end{matrix})}; _{(\begin{matrix}Q[b, b′] \\ a, b, b′ \end{matrix})}; □; (\begin{matrix}P \\ a, b \end{matrix}); _{(\begin{matrix}Q[b, b] \\ a, b \end{matrix})}; (\begin{matrix}b=b′&P \\ a, b, b′ \end{matrix} ); _{(\begin{matrix}Q[b, b′] \\ a, b, b′ \end{matrix})}; a, b; a, b, b′; (\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}Q \\ a, b \end{matrix})}; _{(\begin{matrix}Q \\ a \end{matrix})}; _{(\begin{matrix}Q \\ a, b \end{matrix})}; _{(\begin{matrix}Q \\ a \end{matrix})}; □; _{(\begin{matrix}R \\ a, b \end{matrix})}; _{(\begin{matrix}∀b.R \\ a \end{matrix})}; (\begin{matrix}P \\ a, b \end{matrix}); _{(\begin{matrix}Q \\ a, b \end{matrix})}; (\begin{matrix}∃b.P \\ a \end{matrix} ); _{(\begin{matrix}Q \\ a \end{matrix})}; _{(\begin{matrix}Q \\ a, b \end{matrix})}; _{(\begin{matrix}R \\ a, b \end{matrix})}; _{(\begin{matrix}Q \\ a \end{matrix})}; _{(\begin{matrix}∀b.R \\ a \end{matrix})}; a, b; a]

LCCC:

[figure: _{(\begin{matrix}c \\ a \end{matrix})}; _{(\begin{matrix}c \\ b \end{matrix})}; _{(\begin{matrix}c \\ a \end{matrix})}; _{(\begin{matrix}c \\ b \end{matrix})}; □; a; b; (\begin{matrix}c \\ a, b \end{matrix}); (\begin{matrix}(b=b′), c \\ a, b, b′ \end{matrix}); (\begin{matrix}c \\ a, b \end{matrix}); (\begin{matrix}(b=b′), c \\ a, b, b′ \end{matrix}); co□; _{(\begin{matrix}d \\ a, b \end{matrix})}; _{(\begin{matrix}d \\ a, b, b′ \end{matrix})}; _{(\begin{matrix}d \\ a, b \end{matrix})}; _{(\begin{matrix}d \\ a, b, b′ \end{matrix})}; □; (\begin{matrix}c \\ a, b \end{matrix}); _{(\begin{matrix}d \\ a, b \end{matrix})}; (\begin{matrix}(b=b′), c \\ a, b, b′ \end{matrix}); _{(\begin{matrix}d \\ a, b, b′ \end{matrix})}; a, b; a, b, b′; (\begin{matrix}c \\ a, b \end{matrix}); (\begin{matrix}b, c \\ a \end{matrix}); (\begin{matrix}c \\ a, b \end{matrix}); (\begin{matrix}b, c \\ a \end{matrix}); co□; _{(\begin{matrix}d \\ a, b \end{matrix})}; _{(\begin{matrix}d \\ a \end{matrix})}; _{(\begin{matrix}d \\ a, b \end{matrix})}; _{(\begin{matrix}d \\ a \end{matrix})}; □; _{(\begin{matrix}e \\ a, b \end{matrix})}; _{(\begin{matrix}b↦e \\ a \end{matrix})}; (\begin{matrix}c \\ a, b \end{matrix}); _{(\begin{matrix}d \\ a, b \end{matrix})}; (\begin{matrix}b, c \\ a \end{matrix}); _{(\begin{matrix}d \\ a \end{matrix})}; _{(\begin{matrix}d \\ a, b \end{matrix})}; _{(\begin{matrix}e \\ a, b \end{matrix})}; _{(\begin{matrix}d \\ a \end{matrix})}; _{(\begin{matrix}b↦e \\ a \end{matrix})}; a, b; a]

Two CCompC structures in a topos The two CCompC structures in a topos:

[figure: (\begin{matrix}P \\ a \end{matrix}); (\begin{matrix}⊤ \\ b \end{matrix}); (\begin{matrix}⊤ \\ b \end{matrix}); (\begin{matrix}Q \\ c \end{matrix}); (\begin{matrix}P \\ a \end{matrix}); a; (\begin{matrix}⊤ \\ b \end{matrix}); b; (\begin{matrix}Q \\ c \end{matrix}); c|_{Q}; a; b; b; c|_{Q}; (\begin{matrix}b \\ a \end{matrix}); (\begin{matrix}∗ \\ c \end{matrix}); (\begin{matrix}∗ \\ c \end{matrix}); (\begin{matrix}e \\ d \end{matrix}); (\begin{matrix}b \\ a \end{matrix}); a; (\begin{matrix}∗ \\ c \end{matrix}); c; (\begin{matrix}e \\ d \end{matrix}); d, e; a; c; c; d, e]

Cartesian morphisms project into pullbacks:

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

Cocartesian morphisms induce isos and epis:

[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}); a, b|_{P}; (\begin{matrix}P \\ a, b \end{matrix}); a, b; _{(\begin{matrix}∃b.P \\ a \end{matrix} )}; a|_{∃b.P}; _{(\begin{matrix}∃b.P \\ a \end{matrix} )}; a; a, b|_{P}; a, b; a, b|_{P}; a|_{∃b.P}; a, b; a; a|_{∃b.P}; a; (\begin{matrix}P \\ a, b \end{matrix}); _{(\begin{matrix}b=b′&P \\ a \end{matrix} )}; (\begin{matrix}P \\ a, b \end{matrix}); _{(\begin{matrix}b=b′&P \\ a \end{matrix} )}; co□; (\begin{matrix}P \\ a, b \end{matrix}); a, b|_{P}; (\begin{matrix}P \\ a, b \end{matrix}); a, b; _{(\begin{matrix}b=b′&P \\ a \end{matrix} )}; a, b, b′|_{b=b′&P}; _{(\begin{matrix}b=b′&P \\ a \end{matrix} )}; a, b, b′; a, b|_{P}; a, b; a, b|_{P}; a, b, b′|_{b=b′&P}; a, b; a, b, b′; a, b, b′|_{b=b′&P}; a, b, b′]

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

Basic constructions with NNOs

[figure: ∗; 0; 0; 1; 1; 2; ∗; (n ↦ n); (n ↦ n); (n ↦ n+1); (n ↦ n+1); (n ↦ n+2); 0; (n ↦ n); 1; (n ↦ n+1); 2; (n ↦ n+2); m; n ↦ n+m]

[figure: ∗; 0; 0; 1; 1; 2; ∗; (n ↦ 0); (n ↦ 0); (n ↦ n); (n ↦ n); (n ↦ 2n); 0; (n ↦ 0); 1; (n ↦ n); 2; (n ↦ 2n); m; n ↦ mn]

[figure: ∗; 0; 0; 1; 1; 2; ∗; (n ↦ 1); (n ↦ 1); (n ↦ n); (n ↦ n); (n ↦ n^{2}); 0; (n ↦ 1); 1; (n ↦ n); 2; (n ↦ n^{2}); m; n ↦ n^{m}]

[figure: ∗; 0; 0; 1; 1; 2; ∗; (n ↦ n); (n ↦ n); (n ↦ n−^{.}1); (n ↦ n−^{.}1); (n ↦ n−^{.}2); 0; (n ↦ n); 1; (n ↦ n−^{.}1); 2; (n ↦ n−^{.}2); m; n ↦ n−^{.}m]

NNOs: the morphism p′ Fact: in a topos with NNO the map [0, s] : 1+N → N is an iso.

First we need to define the arrow s′ : 1+N → 1+N, using a factorization through a coproduct. Note that s′ takes the ‘∗’ in ‘∗ ⊔ n’ to 0, not to ∗′. s′ := [0; κ′, s; κ′].

[figure: 1; 1+N; κ; 1+N; N; κ′; 1; N; 0; N; 1+N; κ′; 1+N; 1+N; s′; N; N; s; N; 1+N; κ′; ∗; ∗ ⊔ n; ∗ ⊔ n; n; ∗; 0; 0; ∗′ ⊔ n+1; ∗ ⊔ n; ∗′ ⊔ n+1; n; n+1; n+1; ∗′ ⊔ n+1]

Now we can define p′ : N → 1 + N by factoring (κ, s′) through the NNO. It is possible to show that p′ and [0, s] are inverses.

[figure: 1; N; 0; N; N; s; N; N; s; 1+N; 1+N; s′; 1+N; 1+N; s′; N; N; s; N; N; s; 1; 1+N; κ; N; 1+N; p′; N; 1+N; p′; N; 1+N; p′; N; 1+N; p′; 1; N; 0; 1+N; N; [0,s]; 1+N; N; [0,s]; 1+N; N; [0,s]; 1+N; N; [0,s]]

[figure: ∗; 0; 0; 1; 1; 2; ∗ ⊔ 0′; ∗′ ⊔ 1′; ∗′ ⊔ 1′; ∗′′ ⊔ 2′; 0; 1; 1; 2; ∗; ∗ ⊔ 0′; 0; ∗ ⊔ 0′; 1; ∗′ ⊔ 1′; 2; ∗′′ ⊔ 2′; n; ∗ ⊔ n−1; ∗; 0; ∗ ⊔ 0′; 0; ∗′ ⊔ 1′; 1; ∗′′ ⊔ 2′; 2; ∗ ⊔ n−1; n]

Define n ↦ n−^{.}1 as p′; [0, id], The arrow m ↦ (n −^{.} m) of the previous page