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

logic | category theory | type theory |
---|---|---|

true | terminal object/(-2)-truncated object | h-level 0-type/unit type |

proposition(-1)-truncated objecth-proposition, mere proposition

proofgeneralized elementprogram

cut rulecomposition of classifying morphisms / pullback of display mapssubstitution

cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction

introduction rule for implicationunit for hom-tensor adjunctioneta conversion

logical conjunctionproductproduct type

disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)

implicationinternal homfunction type

negationinternal hom into initial objectfunction type into empty type

universal quantificationdependent productdependent product type

existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)

equivalencepath space objectidentity type

equivalence classquotientquotient type

inductioncolimitinductive type, W-type, M-type

higher inductionhigher colimithigher inductive type

completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set

setinternal 0-groupoidBishop set/setoid

universeobject classifiertype of types

modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)

linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation

proof netstring diagramquantum circuit

(absence of) contraction rule(absence of) diagonalno-cloning theorem

synthetic mathematicsdomain specific embedded programming language

</table>

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)

Last revised on May 24, 2013 at 00:46:08. See the history of this page for a list of all contributions to it.