|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-level 1-type/h-prop|
|classical type theory?||internal logic||classical type theory?, logic programming?|
|cut elimination?||counit||beta reduction|
|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 monad||modal type theory, monad (in computer science)|
Type theory and certain kinds of category theory are closely related. By a syntax-semantics duality one may view type theory as a formal syntactic language or calculus for category theory, and conversely one may think of category theory as providing semantics for type theory. The flavor of category theory used depends on the flavor of type theory; this also extends to homotopy type theory and certain kinds of (∞,1)-category theory.
multiplicative intuitionistic linear logic? | | symmetric closed monoidal category | | |first-order logic | | hyperdoctrine | (Seely 1984a) | classical linear logic | | star-autonomous category | (Seely 89) | |Martin-Löf dependent type theory| | locally cartesian closed category | (Seely 1984b) | |homotopy type theory| | locally cartesian closed (∞,1)-category | (conjectural) | |homotopy type theory with higher inductive types and univalence | | elementary (∞,1)-topos | (conjectural) |
We discuss here formalizations and proofs of the relation/equivalence between various flavors of type theories and the corresponding flavors of categories.
constitute an equivalence of categories
There are 2-functors
that constitute an equivalence of 2-categories
This was originally claimed as an equivalence of categories (Seely, theorem 6.3). However, that argument did not properly treat a subtlety central to the whole subject: that substitution of terms for variables composes strictly, while its categorical semantics by pullback is by the very nature of pullbacks only defined up to isomorphism. This problem was pointed out and ways to fix it were given in (Curien) and (Hofmann); see categorical model of dependent types for the latter. However, the full equivalence of categories was not recovered until (Clairambault-Dybjer) solved both problems by promoting the statement to an equivalence of 2-categories.
We now indicate some of the details.
type formation rules
is a type (the unit type);
if are terms of type , then is a type (the equality type);
if and are types, depending on a free variable of type , then the following symbols are types
([dependent product]), written also if in fact does not depend on ;
(dependent sum), written also if in fact does not depend on ;
term formation rules
is a term of the unit type;
Composition is given in the evident way.
Constructions are straightforward. We indicated some of them.
is given by
is given by
In one direction, send a morphism to the dependent type
Conversely, for a dependent type, send it to the projection .
One shows that this indeed gives an equivalence of categories which is compatible with base change (Seely, prop. 3.2.4).
For a dependent type theory and a locally cartesian closed category, an interpretation of in is a morphism of locally cartesian closed categories
An interpretation of in another dependent type theory is a morphism of locally cartesian closed categories
Every presentable and locally cartesian closed (∞,1)-category has a presentation by a type-theoretic model category. This provides the categorical semantics for homotopy type theory (without, possibly, the univalence axiom).
For more on this see at [locally cartesian closed (∞,1)-category]] in the section on internal logic.
A lecture reviewing aspects involved in this equivalence is (see the discussion building up to the theorem on slide 96)
and reviews/further developments are in
following a statement earlier conjectured in
The problem with strict substitution compared to weak pullback in this argument was discussed and fixed in
but in the process the equivalence of categories was lost. This was finally all rectified in
A discussion of the correspondence between type theories and categories of various sorts, from lex categories to toposes is in