|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination? for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
The notion of a hyperdoctrine is essentially an axiomatization of the collection of slices of a locally cartesian closed category (or something similar): a category together with a functorial assignment of “slice-like”-categories to each of its objects, satisfying some conditions.
In its use in mathematical logic (“categorical logic” (Lawvere 69)) a hyperdoctrine is thought of (under categorical semantics of logic/type theory) as a collection of contexts together with the operations of context extension/substitution and quantification on the categories of propositions or types in each context. Therefore specifying the structure of a hyperdoctrine over a given category is a way of equipping that with a given kind of logic.
Specifically, a hyperdoctrine on a category for a given notion of logic is a functor
In the most classical case, is propositional logic, and is a 2-category of posets (e.g. lattices, Heyting algebras, or frames). A hyperdoctrine is then an incarnation of first-order predicate logic. A canonical class of examples of this case is where sends to the poset of subobjects of . The predicate logic we obtain in this way is the usual sort of internal logic of .
We generally require also that for every morphism the morphism has both a left adjoint as well as a right adjoint, typically required to satisfy Frobenius reciprocity and the Beck-Chevalley condition. These adjoints are regarded as the action of quantifiers along . Thus, a hyperdoctrine can also be regarded as a way of “adding quantifiers” to a given kind of logic.
More precisely, one thinks of
the left adjoint to gives the application of the existential quantifier;
the right adjoint to gives the application of the universal quantifier (see there for the interpretation of quantifiers in terms of adjoints).
The Beck-Chevalley condition ensures that quantification interacts with substitution of variables as expected
Frobenius reciprocity expresses the derivation rules.
The general concept of hyperdoctrines does for predicate logic precisely what Lindenbaum-Tarski algebras do for propositional logic, positioning the categorical formulation of logic as a natural extension of the algebraicization of logic.
constitute an equivalence of categories
= the category of contexts, is the category of formulas. “Given any theory (several sorted, intuitionistic or classical) …”
(“or one may take suitable ‘homotopy classes’ of deductions”).
= the category of small sets, … “This hyperdoctrine may be viewed as a kind of set-theoretical surrogate of proof theory”
“honest proof theory would presumably yield a hyperdoctrine with nontrivial , but a syntactically presented one”.
= Cat, the category of small categories,
= Cat the category of small categories,
= Grpd the category of small groupoids,
The notion was introduced in
and developed in
Bill Lawvere, Equality in hyperdoctrines and comprehension schema as an adjoint functor, Proceedings of the AMS Symposium on Pure Mathematics XVII (1970), 1-14.
Surveys and reviews include
A string diagram calculus for monoidal hyperdoctrines is discussed in