nLab first-order hyperdoctrine



Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

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

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) 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

homotopy levels


(0,1)(0,1)-Category theory



A first-order hyperdoctrine is a hyperdoctrine with respect to lattices that are Heyting algebras.


We denote by HeytAlg AdjCylHeytAlg_{AdjCyl} the category whose objects are Heyting algebras, and whose morphisms are Heyting algebra morphisms having both left and right adjoints. (The adjoints are not required to be Heyting algebra morphisms, but can be arbitrary monotone maps.)

A first-order hyperdoctrine consists of a category with finite products C TC_T, along with a functor

P:C T opHeytAlg AdjCyl P \colon C_T^{op} \to HeytAlg_{AdjCyl}

such that the following Beck-Chevalley condition is satisfied: for every object AA, the left adjoints to P(π)P(\pi) for the projections π:A×\pi : A \times - \to - comprise a natural transformation from P(A×)P(A \times -) to P()P(-), and so do the right adjoints. This expresses the Beck-Chevalley condition for pullback squares of the form

A×B π B B 1 A×f f A×C π C C\array{ A \times B & \stackrel{\pi_B}{\to} & B \\ ^\mathllap{1_A \times f} \downarrow & & \downarrow^\mathrlap{f} \\ A \times C & \underset{\pi_C}{\to} & C }

An element of P(A)P(A) is often called a predicate over AA (with respect to the hyperdoctrine).

For any first-order hyperdoctrine, an equality predicate can be defined for each type AOb(C T)A \in Ob(C_T) as

(δ A)( P(A))P(A×A)\exists(\delta_A)(\top_{P(A)}) \in P(A \times A)

where for any morphism ff in C TC_T, we use (f)\exists (f) to denote the left adjoint of P(f)P(f), and H\top_H denotes the top element in a Heyting algebra HH.

However, to get good properties for equality, we need to assume a little more. A first-order hyperdoctrine with equality is a first-order hyperdoctrine such that the Beck-Chevalley condition is satisfied for pullback diagrams of the form

A×B A×f A×C δ A×B δ A×C A×A×B A×A×f A×A×C,\array{ A\times B & \stackrel{A\times f}{\to} & A \times C \\ ^\mathllap{\delta_A\times B} \downarrow & & \downarrow^\mathrlap{\delta_A \times C} \\ A \times A \times B& \underset{A\times A\times f}{\to} & A \times A \times C },

i.e. that P(A×A×f)(δ A×B)=(δ A×C)P(A×f)P(A\times A \times f) \circ \exists (\delta_A \times B) = \exists (\delta_A \times C) \circ P(A\times f).

This assures that the equality predicate is well behaved in the sense that it allows a sound interpretation of first order logic with equality in the hyperdoctrine.

Additionally one may require the condition for pullbacks of the form

A δ A A×A δ A 1 A×δ A A×A δ A×1 A A×A×A,\array{ A & \stackrel{\delta_A}{\to} & A \times A \\ ^\mathllap{\delta_A} \downarrow & & \downarrow^\mathrlap{1_A \times \delta_A} \\ A \times A & \underset{\delta_A \times 1_A}{\to} & A \times A \times A },

which is a kind of Frobenius law. By taking right adjoints, a similar equation holds for (f)\forall (f) in place of (f)\exists (f), where P(f)(f)P(f) \dashv \forall (f).

As an Internal Heyting Algebra

Similar to the natural models formulation of a category with families, a first-order hyperdoctrince can be defined concisely using the internal language of presheaf categories. That is, a first-order hyperdoctrine is equivalently defined as a category C TC_T with finite products and PP an internal Heyting algebra in the category of presheaves on C TC_T that additionally has

  1. For every AC TA \in C_T internal YAYA-meets and joins where YAYA is the representable presheaf of AA.
  2. For every AC TA \in C_T, PP internally has an YAYA-equality predicate, i.e., a least reflexive binary relation on YAYA valued in PP. In more detail, this is an internal function = AP YA×YA=_A \in P^{YA \times YA} such that for every fP YA×YAf \in P^{YA\times YA} we have x,y.x= Ayf(x,y)\forall x,y. x =_A y \leq f(x,y) if and only if xA.f(x,x)\forall x\in A. \top \leq f(x,x).

Here the Beck-Chevalley conditions on the quantifiers and equality arises from the fact that the operations are internal and therefore natural in CC. Unraveling the internal language, this definition is the same as the formulation given by Lawvere that requires only equality predicates and adjoints to substitution along projections.


With this, we have enough structure to interpret multi-sorted first-order intuitionistic logic with equality, taking the objects of C TC_T to be sorts and its morphisms to be terms, PP to assign to each sort the Lindenbaum algebra of predicates upon that sort and to each term the operation of substitution of that term into predicates, and the left and right adjoints to PP upon projections to provide existential and universal quantification, respectively, with the existence of the further adjoints providing the ability to interpret equality, and the Beck-Chevalley condition ensuring that quantification commutes appropriately with substitution (just as the propositional connectives do).


There are, of course, many variants on this, corresponding straightforwardly to modifications of the kind of logic one wishes to represent. For instance, to represent specifically classical logic, one should use Boolean algebras instead of Heyting algebras. To represent first-order logic without equality, one should no longer require left and right adjoints to every morphism in the range of PP, but rather only those given by the natural transformations yielding the quantifiers (i.e., only requiring adjoints to substitution along projections). Various higher-order constructs can be added by adding new ways of forming objects in C TC_T (e.g., adding cartesian closedness). Etc.

One can even extend this into the realm not just of provability, but furthermore of proof theory, by taking the objects in the codomain of PP to be categories rather than mere preorders (e.g., by using bicartesian closed categories rather than Heyting algebras); in this case, the objects in a category P(σ)P(\sigma) would still represent predicates on the sort σ\sigma, but the morphisms in P(σ)P(\sigma) would represent proofs (rather than mere provability) of entailments between these predicates, with the possibility that not all such proofs would be equal.

categoryfunctorinternal logictheoryhyperdoctrinesubobject posetcoverageclassifying topos
finitely complete categorycartesian functorcartesian logicessentially algebraic theory
lextensive categorydisjunctive logic
regular categoryregular functorregular logicregular theoryregular hyperdoctrineinfimum-semilatticeregular coverageregular topos
coherent categorycoherent functorcoherent logiccoherent theorycoherent hyperdoctrinedistributive latticecoherent coveragecoherent topos
geometric categorygeometric functorgeometric logicgeometric theorygeometric hyperdoctrineframegeometric coverageGrothendieck topos
Heyting categoryHeyting functorintuitionistic first-order logicintuitionistic first-order theoryfirst-order hyperdoctrineHeyting algebra
De Morgan Heyting categoryintuitionistic first-order logic with weak excluded middleDe Morgan Heyting algebra
Boolean categoryclassical first-order logicclassical first-order theoryBoolean hyperdoctrineBoolean algebra
star-autonomous categorymultiplicative classical linear logic
symmetric monoidal closed categorymultiplicative intuitionistic linear logic
cartesian monoidal categoryfragment {&,}\{\&, \top\} of linear logic
cocartesian monoidal categoryfragment {,0}\{\oplus, 0\} of linear logic
cartesian closed categorysimply typed lambda calculus

Last revised on June 15, 2023 at 01:01:50. See the history of this page for a list of all contributions to it.