relation between type theory and category theory



Type theory

Category theory



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.


flavor of type theory\;equivalent to\;flavor of category theory
intuitionistic propositional logic/simply-typed lambda calculuscartesian closed category
multiplicative intuitionistic linear logicsymmetric closed monoidal category(various authors since ~68)
first-order logichyperdoctrine(Seely 1984a)
classical linear logicstar-autonomous category(Seely 89)
extensional dependent type theorylocally cartesian closed category(Seely 1984b)
homotopy type theory without univalence (intensional M-L dependent type theory)locally cartesian closed (∞,1)-category(Cisinski 12-(Shulman 12)
homotopy type theory with higher inductive types and univalenceelementary (∞,1)-topossee here
dependent linear type theoryindexed monoidal category (with comprehension)(Vákár 14)

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

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty 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


We discuss here formalizations and proofs of the relation/equivalence between various flavors of type theories and the corresponding flavors of categories.

First-order logic and hyperdoctrines


The functors

constitute an equivalence of categories

FirstOrderTheoriesContLangHyperdoctrines. FirstOrderTheories \stackrel{\overset{Lang}{\leftarrow}}{\underset{Cont}{\to}} Hyperdoctrines \,.

(Seely, 1984a)

Dependent type theory and locally cartesian closed categories

We discuss here how dependent type theory is the syntax of which locally cartesian closed categories provide the semantics. For a dedicated discussion of this (and the subtle coherence issues involved) see also at categorical model of dependent types.


There are 2-functors

that constitute an equivalence of 2-categories

MLDependentTypeTheoriesContLangLocallyCartesianClosedCategories. MLDependentTypeTheories \underoverset {\underset{Cont}{\longrightarrow}} {\overset{Lang}{\longleftarrow}} {\simeq} LocallyCartesianClosedCategories \,.

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, see also (Curien-Garner-Hofmann). Another approach to this which also works with intensional identity types and hence with homotopy type theory is in (Lumsdaine-Warren 13).

We now indicate some of the details.

Type theories

For definiteness, self-containedness and for references below, we say what a dependent type theory is, following (Seely, def. 1.1).


A Martin-Löf dependent type theory TT is a theory with some signature of dependent function symbols with values in types and in terms (…) subject to the following rules

  1. type formation rules

    1. 11 is a type (the unit type);

    2. if a,ba, b are terms of type AA, then (a=b)(a = b) is a type (the equality type);

    3. if AA and B[x]B[x] are types, BB depending on a free variable of type AA, then the following symbols are types

      1. a:AB[a]\prod_{a : A} B[a] (dependent product), written also (AB)(A \to B) if B[x]B[x] in fact does not depend on xx;

      2. a:AB[a]\sum_{a : A} B[a] (dependent sum), written also A×BA \times B if B[x]B[x] in fact does not depend on xx;

  2. term formation rules

    1. *1* \in 1 is a term of the unit type;

    2. (…)

  3. equality rules

    1. (…)

Category of contexts


Given a dependent type theory TT, its category of contexts Con(T)Con(T) is the category whose

Composition is given in the evident way.


Con(T)Con(T) has finite limits and is a cartesian closed category.

(Seely, prop. 3.1)


Constructions are straightforward. We indicated some of them.

Notice that all finite limits (as discussed there) are induced as soon as there are all pullbacks and equalizers. A pullback in Con(T)Con(T)

P A f B g C \array{ P &\to& A \\ \downarrow && \downarrow^{\mathrlap{f}} \\ B &\stackrel{g}{\to}& C }

is given by

P a:A bB(f(a)=g(b)). P \simeq \sum_{a : A} \sum_{b \in B} (f(a) = g(b)) \,.

The equalizer

PAgfB P \to A \stackrel{\overset{f}{\to}}{\underset{g}{\to}} B

is given by

P= a:A(f(a)=g(a)). P = \sum_{a : A} (f(a) = g(a)) \,.

Next, the internal hom/exponential object is given by function type

[A,B](AB). [A,B] \simeq (A \to B) \,.

Con(T)Con(T) is a locally cartesian closed category.

(Seely, theorem 3.2)


Define the Con(T)Con(T)-indexed hyperdoctrine P(T)P(T) by taking for ACon(T)A \in Con(T) the category P(T)(A)P(T)(A) to have as objects the AA-dependent types and as morphisms (a:AX(a):type)(a:AY(a):type)(a : A \vdash X(a) : type) \to (a : A \vdash Y(a) : type) the terms of dependent function type (a:At:(X(a)Y(a)))(a : A \vdash t : (X(a) \to Y(a))).

This is cartesian closed by the same kind of argument as in the previous proof. It is now sufficient to exhibit a compatible equivalence of categories with the slice category Con(T) /ACon(T)_{/A}.

Con(T) /AP(T)(A). Con(T)_{/A} \simeq P(T)(A) \,.

In one direction, send a morphism f:XAf : X \to A to the dependent type

a:Af 1(a) x:X(a=f(x)). a : A \vdash f^{-1}(a) \coloneqq \sum_{x : X} (a = f(x)) \,.

Conversely, for a:AX(a)a : A \vdash X(a) a dependent type, send it to the projection a:AX(a)A\sum_{a : A} X(a) \to A.

One shows that this indeed gives an equivalence of categories which is compatible with base change (Seely, prop. 3.2.4).


For TT a dependent type theory and CC a locally cartesian closed category, an interpretation of TT in CC is a morphism of locally cartesian closed categories

Con(T)C. Con(T) \to C \,.

An interpretation of TT in another dependent type theory TT' is a morphism of locally cartesian closed categories

Con(T)Con(T). Con(T) \to Con(T') \,.

Internal language


Given a locally cartesian closed category CC, define the corresponding dependent type theory Lang(C)Lang(C) as follows

  • the non-dependent types of Lang(C)Lang(C) are the objects of CC;

  • the AA-dependent types are the morphisms BAB \to A;

  • a context x 1:X 1,x 2:X 2,,x n:X nx_1 : X_1 , x_2 : X_2, \cdots , x_n : X_n is a tower of morphisms

    X n X 2 X 1 \array{ X_n \\ \downarrow \\ \cdots \\ \downarrow \\ X_2 \\ \downarrow \\ X_1 }
  • the terms t[x A]:B[x A]t[x_A] : B[x_A] are the sections ABA \to B in C /AC_{/A}

  • the equality type (x A=y A)(x_A = y_A) is the diagonal AA×AA \to A \times A

Homotopy type theory and locally cartesian closed (,1)(\infty,1)-categories

All of the above has an analog in (∞,1)-category theory and homotopy type theory.


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).

This includes in particular all (∞-stack-) (∞,1)-toposes (which should in addition satisfy univalence). See also at internal logic of an (∞,1)-topos.

Some form of this statement was originally formally conjectured in (Joyal 11), following (Awodey 10). For more details see at locally cartesian closed (∞,1)-category.

Univalent homotopy type theory and elementary (,1)(\infty,1)-toposes

More precise information can be found on the homotopytypetheory wiki.

A (locally presentable) locally Cartesian closed (∞,1)-category (as above) which in addition has a system of object classifiers is an ((∞,1)-sheaf-)(∞,1)-topos.

It has been conjectured in (Awodey 10) that this object classifier is the categorical semantics of a univalent type universe (type of types), hence that homotopy type theory with univalence has categorical semantics in (∞,1)-toposes. This statement was proven for the canonical (,1)(\infty,1)-topos ∞Grpd in (Kapulkin-Lumsdaine-Voevodsky 12), and more generally for (∞,1)-presheaf (,1)(\infty,1)-toposes over elegant Reedy categories in (Shulman 13).

In these proofs the type-theoretic model categories which interpret the homotopy type theory syntax are required to provide type universes that behave strictly under pullback. This matches the usual syntactically convenient universes in type theory (either a la Russell or a la Tarski), but more difficult to implement in the categorical semantics. More flexibly, one may consider syntactic type universes weakly à la Tarski (Luo 12, Gallozzi 14). These are more complicated to work with syntactically, but should have interpretations in a (type-theoretic model categories presenting) any (∞,1)-topos. Discussion of univalence in this general flexible sense is in (Gepner-Kock 12). For the general syntactic issue see at

While (∞,1)-sheaf (∞,1)-toposes are those currently understood, the basic type theory with univalent universes does not see or care about their local presentability as such (although it is used in other places, such as the construction of higher inductive types). It is to be expected that there is a decent concept of elementary (∞,1)-topos such that homotopy type theory with univalent type universes and some supply of higher inductive types has categorical semantics precisely in elementary (∞,1)-toposes (as conjectured in Awodey 10). But the fine-tuning of this statement is currently still under investigation.

Notice that this statement, once realized, makes (or would make) Univalent HoTT+HITs a sort of homotopy theoretic refinement of foundations of mathematics in topos theory as proposed by William Lawvere. It could be compared to his elementary theory of the category of sets, although being a type theory rather than a theory in first-order logic, it is more analogous to the internal type theory of an elementary topos.


An elementary exposition of in terms of the Haskell programming language is in

The equivalence of categories between first order theories and hyperdoctrines is discussed in

  • R. A. G. Seely, Hyperdoctrines, natural deduction, and the Beck condition, Zeitschrift für Math. Logik und Grundlagen der Math. (1984) (pdf)

The categorical model of dependent types and initiality is discussed in

  • Simon Castellan, Dependent type theory as the initial category with families, 2014 (pdf)

which was formalized inside type theory with set quotients of higher inductive types in:

Surveys inclue

  • Tom Hirschowitz, Introduction to categorical logic (2010) (pdf)

    (see the discussion building up to the theorem on slide 96)

  • Roy Crole, Deriving category theory from type theory, Theory and Formal Methods 1993 Workshops in Computing 1993, pp 15-26

  • Maria Maietti, Modular correspondence between dependent type theories and categories including pretopoi and topoi, Mathematical Structures in Computer Science archive Volume 15 Issue 6, December 2005 Pages 1089 - 1149 (pdf)

The equivalence between linear logic and star-autonomous categories is due to

  • R. A. G. Seely, Linear logic, *\ast-autonomous categories and cofree coalgebras, Contemporary Mathematics 92, 1989. (pdf, ps.gz)

and reviews/further developments are in

  • G. M. Bierman, What is a Categorical Model of Intuitionistic Linear Logic? (web)

  • Andrew Graham Barber, Linear Type Theories, Semantics and Action Calculi, 1997 (web, pdf)

  • Paul-André Melliès , Categorial Semantics of Linear Logic, in Interactive models of computation and program behaviour, Panoramas et synthèses 27, 2009 (pdf)

For dependent linear type theory see

An adjunction between the category of type theories with product types and toposes is discussed in chapter II of

  • Joachim Lambek, P. Scott, Introduction to higher order categorical logic, Cambridge University Press (1986) .

The equivalence of categories between locally cartesian closed categories and dependent type theories was originally claimed in

  • R. A. G. Seely, Locally cartesian closed categories and type theory, Math. Proc. Camb. Phil. Soc. (1984) 95 (pdf)

following a statement earlier conjectured in

  • Per Martin-Löf, An intuitionistic theory of types: predicative part, In Logic Colloquium (1973), ed. H. E. Rose and J. C. Shepherdson (North-Holland, 1974), 73-118. (web)

The problem with strict substitution compared to weak pullback in this argument was discussed and fixed in

  • Pierre-Louis Curien, Substitution up to isomorphism, Fundamenta Informaticae, 19(1,2):51–86 (1993)

  • Martin Hofmann, On the interpretation of type theory in locally cartesian closed categories, Proc. CSL ‘94, Kazimierz, Poland. Jerzy Tiuryn and Leszek Pacholski, eds. Springer LNCS, Vol. 933 (CiteSeer)

but in the process the equivalence of categories was lost. This was finally all rectified in

  • Pierre Clairambault, Peter Dybjer, The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories, in Typed lambda calculi and applications, Lecture Notes in Comput. Sci. 6690, Springer 2011 (arXiv:1112.3456)


Another version of this which also applies to intensional identity types and hence to homotopy type theory is in

The analogous statement relating homotopy type theory and locally cartesian closed (infinity,1)-categories was formally conjectured around

following earlier suggestions by Steve Awodey. Explicitly, the suggestion that with the univalence axiom added this is refined to (∞,1)-topos theory appears around

Details on this higher categorical semantics of homotopy type theory are in

with lecture notes in

See also

Models specifically in (constructive) cubical sets are discussed in

  • Marc Bezem, Thierry Coquand, Simon Huber, A model of type theory in cubical sets, 2013 (web, pdf)

  • Ambrus Kaposi, Thorsten Altenkirch, A syntax for cubical type theory (pdf)

  • Simon Docherty, A model of type theory in cubical sets with connection, 2014 (pdf)

A precise definition of elementary (infinity,1)-topos inspired by giving a natural equivalence to homotopy type theory with univalence was then proposed in

Categorical semantics of univalent type universes is discussed in

Discussion of weak Tarskian homotopy type universes is in

A discussion of the correspondence between type theories and categories of various sorts, from lex categories to toposes is in

  • Maria Emilia Maietti, Modular correspondence between dependent type theories and categories including pretopoi and topoi, Math. Struct. in Comp. Science (2005), vol. 15, pp. 1089–1149 (gzipped ps) (doi)

Last revised on September 15, 2018 at 13:37:40. See the history of this page for a list of all contributions to it.