hyperdoctrine in nLab

Contents

Contents

Idea

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 TT 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 TT for a given notion of logic LL is a functor

P:T op→C P \colon T^{op} \to \mathbf{C}

to some 2-category (or even higher category) C\mathbf{C}, whose objects are categories whose internal logic corresponds to LL. Thus, each object AA of TT is assigned an “LL-logic” (the internal logic of P(A)P(A)).

In the most classical case, LL is propositional logic, and C\mathbf{C} 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 PP sends A∈TA \in T to the poset of subobjects Sub T(A)Sub_T(A) of AA. The predicate logic we obtain in this way is the usual sort of internal logic of TT.

We generally require also that for every morphism f:A→Bf \colon A \to B the morphism P(f)P(f) 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 ff. Thus, a hyperdoctrine can also be regarded as a way of “adding quantifiers” to a given kind of logic.

More precisely, one thinks of

• TT as a category of types or rather contexts;

• PP as assigning

  • to each context X∈TX \in T the lattice of propositions in this context;

  • to each morphism f:X→Yf \colon X \to Y in TT the operation of “substitution of variables” / “extension of contexts” for propositions P(Y)→P(X)P(Y) \to P(X);

• the left adjoint to P(f)P(f) gives the application of the existential quantifier;

• the right adjoint to P(f)P(f) 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.

So, in particular, a hyperdoctrine is a kind of indexed category or fibered category.

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 algebraization of logic.

Properties

This is due to (Seely, 1984a). For more details see relation between type theory and category theory.

Examples

Classes of hyperdoctrines

• first-order hyperdoctrine

• modal hyperdoctrine

• regular hyperdoctrine

• coherent hyperdoctrine

• Boolean hyperdoctrine

• geometric hyperdoctrine

• linear hyperdoctrine

Special cases

• TT = the category of contexts, P(X)P(X) is the category of formulas. “Given any theory (several sorted, intuitionistic or classical) …”

• TT = the category Set of small sets, P(X)=2 X=P(X) = 2^X = the power set functor, assigning the poset of all propositional functions

  (“or one may take suitable ‘homotopy classes’ of deductions”).

• TT = the category of small sets, P(X)=Set XP(X) = Set^X … “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 P(X)P(X), but a syntactically presented one”.

• TT = Cat, the category of small categories, P(B)=2 BP(B) = 2^B

• TT = Cat the category of small categories, P(B)=Set BP(B) = Set^B

• TT = Grpd the category of small groupoids, P(B)=Set BP(B) = Set^B

• comprehension

• tripos

• modal hyperdoctrine

References

The notion was introduced in

• Bill Lawvere, Adjointness in Foundations, (TAC), Dialectica 23 (1969), 281-296

and further 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. (pdf)

and with further emphasis on the role of the Beck-Chevalley condition:

• Robert A. G. Seely, Hyperdoctrines, Natural Deduction and the Beck Condition, Zeitschr. f. math Logik und Grundlagen d. Math. 29 (1983) 505-542 [pdf]

Surveys and reviews include

• Anders Kock, Gonzalo Reyes, Doctrines in categorical logic, in J. Barwise (ed.) Handbook of Mathematical Logic (North Holland, Amsterdam, 1977) 283-313

• Peter Dybjer, (What I know about) the history of the identity type (2006) (pdf slides)

A string diagram calculus for monoidal hyperdoctrines is discussed in

• Geraldine Brady, Todd Trimble, A string diagram calculus for predicate logic

A concise introduction to posetal hyperdoctrines is given in

• Thomas Streicher, Categorical models of constructive logic.