coherent hyperdoctrine

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

Let $C$ be a category with finite limits. A **coherent hyperdoctrine** over $C$ is a functor

$P : C^{op} \to DistLattice$

from the opposite category of $C$ to the category of distributive lattices, such that for every morphism $f : A \to B$ in $C$, the functor $P(A) \to P(B)$ has a left adjoint $\exists_f$ satisfying

The assignment (here) of a coherent hyperdoctrine $S(C)$ to a coherent category $C$ extends to a 2-adjunction

$(A \dashv S)
:
CoherentCat
\stackrel{\overset{A}{\leftarrow}}{\underset{S}{\hookrightarrow}}
CoherentHyperdoctrine$

with the right adjoint being a full and faithful 2-functor, hence exhibiting $CoherentCat$ as a reflective sub-2-category of $CoherentHyperdoctrine$.

(Here $CoherentCat$ has as 2-morphisms those natural transformations that preserve finite products.)

This appears as (Coumans, prop. 8).

Coherent hyperdoctrines are closed under canonical extension $(-)^\delta : DistLattice \to DistLattice$, in that for $P : C^{op} \to DistLattic$ a coherent hyperdoctrine, so is $(-)^\delta \circ P$.

This appears as (Coumans, prop. 9).

The powerset functor

$P := \{0,1\}^{(-)} : Set^{op} \to DistLattice$

(sending a set to its power set and a function to the preimage-assignment) is a coherent hyperdoctrine.

Let $C$ be a coherent category. For every object $A \in C$ the poset of subobjects $Sub_C(A)$ is a distributive lattice.

The corresponding functor

$C^{op} \to DistLattice$

from the opposite category of $C$ to the category of distributive lattices is called the **coherent hyperdoctrine** of $C$.

Accordingly, there is a coherent hyperdoctrine associated with any coherent theory, where the objects of $C$ are lists of free variables in the theory, and the lattice assigned to them is that of propositions of the theory in this context.

- Dion Coumans,
*Generalizing canonical extensions to the categorical setting*(Arxiv)