nLab relation between type theory and category theory

Idea

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.

Overview

internal logic/type theory (syntax)	$\;$equivalent to$\;$	category of contexts (semantics)
propositional logic		Lindenbaum-Tarski algebra
intuitionistic propositional logic		Heyting algebra
classical propositional logic		Boolean algebra
dual intuitionistic propositional logic		co-Heyting algebra
first-order logic		hyperdoctrine	Seely 1984a
regular logic		regular hyperdoctrine/regular category
coherent logic		coherent hyperdoctrine/coherent category
intuitionistic predicate logic		first-order hyperdoctrine/Heyting category
classical predicate logic		Boolean hyperdoctrine/Boolean category
modal logic		modal hyperdoctrine
linear logic		linear hyperdoctrine
simply-typed lambda calculus		cartesian closed category	Lambek & Scott 1986, Part I
extensional dependent type theory		locally cartesian closed category	Seely 1984b
bunched logic		doubly closed monoidal category	O’Hearn & Pym 1999
homotopy type theory without univalence (intensional M-L dependent type theory)		locally cartesian closed (∞,1)-category	Cisinski 2012 & Shulman 2012
homotopy type theory with higher inductive types and univalence		elementary (∞,1)-topos	see here
multiplicative intuitionistic linear logic		symmetric closed monoidal category	various authors since ~68
classical linear logic		star-autonomous category	Seely 1989
dependent linear type theory		indexed monoidal category (with comprehension)	Riley 2022

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

logic	set theory (internal logic of)	category theory	type theory
proposition	set	object	type
predicate	family of sets	display morphism	dependent type
proof	element	generalized element	term/program
cut rule		composition of classifying morphisms / pullback of display maps	substitution
introduction rule for implication		counit for hom-tensor adjunction	lambda
elimination rule for implication		unit for hom-tensor adjunction	application
cut elimination for implication		one of the zigzag identities for hom-tensor adjunction	beta reduction
identity elimination for implication		the other zigzag identity for hom-tensor adjunction	eta conversion
true	singleton	terminal object/(-2)-truncated object	h-level 0-type/unit type
false	empty set	initial object	empty type
proposition, truth value	subsingleton	subterminal object/(-1)-truncated object	h-proposition, mere proposition
logical conjunction	cartesian product	product	product type
disjunction	disjoint union (support of)	coproduct ((-1)-truncation of)	sum type (bracket type of)
implication	function set (into subsingleton)	internal hom (into subterminal object)	function type (into h-proposition)
negation	function set into empty set	internal hom into initial object	function type into empty type
universal quantification	indexed cartesian product (of family of subsingletons)	dependent product (of family of subterminal objects)	dependent product type (of family of h-propositions)
existential quantification	indexed disjoint union (support of)	dependent sum ((-1)-truncation of)	dependent sum type (bracket type of)
logical equivalence	bijection set	object of isomorphisms	equivalence type
	support set	support object/(-1)-truncation	propositional truncation/bracket type
		n-image of morphism into terminal object/n-truncation	n-truncation modality
equality	diagonal function/diagonal subset/diagonal relation	path space object	identity type/path type
completely presented set	set	discrete object/0-truncated object	h-level 2-type/set/h-set
set	set with equivalence relation	internal 0-groupoid	Bishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
	equivalence class/quotient set	quotient	quotient type
induction		colimit	inductive type, W-type, M-type
higher induction		higher colimit	higher inductive type
-		0-truncated higher colimit	quotient inductive type
coinduction		limit	coinductive type
	preset		type without identity types
	set of truth values	subobject classifier	type of propositions
domain of discourse	universe	object classifier	type universe
modality		closure operator, (idempotent) 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

Theorems

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

• Dependent type theory and locally cartesian closed categories

• Homotopy type theory and locally cartesian closed (∞,1)-categories

• Univalent homotopy type theory and elementary (∞,1)-toposes

First-order logic and hyperdoctrines

Theorem

The functors

• $Cont$, that form a category of contexts of a first-order theory;

• $Lang$, that forms the internal language of a hyperdoctrine

constitute an equivalence of categories

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

Theorem

There are 2-functors

• $Cont$, that forms a category of contexts of a Martin-Löf dependent type theory;

• $Lang$ that forms the internal language of a locally cartesian closed category

that constitute an equivalence of 2-categories

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

Definition

A Martin-Löf dependent type theory $T$ 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. $1$ is a type (the unit type);

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

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

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

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

2. term formation rules

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

   2. (…)

3. equality rules

   1. (…)

Category of contexts

Definition

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

• objects are the types of $T$;

• morphisms$f : A \to B$ are the terms $f$ of function type $A \to B$.

Composition is given in the evident way.

Proposition

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

(Seely, prop. 3.1)

Proof

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

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

is given by

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

The equalizer

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

is given by

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

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

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

Proposition

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

(Seely, theorem 3.2)

Proof

Define the $Con(T)$-indexed hyperdoctrine $P(T)$ by taking for $A \in Con(T)$ the category $P(T)(A)$ to have as objects the $A$-dependent types and as morphisms $(a : A \vdash X(a) : type) \to (a : A \vdash Y(a) : type)$ the terms of dependent function type $(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)_{/A}$.

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

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

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

Conversely, for $a : A \vdash X(a)$ a dependent type, send it to the projection $\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).

Definition

For $T$ a dependent type theory and $C$ a locally cartesian closed category, an interpretation of $T$ in $C$ is a morphism of locally cartesian closed categories

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

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

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

Internal language

Proposition

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

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

• the $A$-dependent types are the morphisms $B \to A$;

• a context $x_1 : X_1 , x_2 : X_2, \cdots , x_n : X_n$ is a tower of morphisms

  $$\array{ X_n \\ \downarrow \\ \cdots \\ \downarrow \\ X_2 \\ \downarrow \\ X_1 }$$

• the terms $t[x_A] : B[x_A]$ are the sections $A \to B$ in $C_{/A}$

• the equality type $(x_A = y_A)$ is the diagonal $A \to A \times A$

• …

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

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

Proposition

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 $(\infty,1)$-toposes

For more details see model of type theory in an (infinity,1)-topos.

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 $(\infty,1)$-topos ∞Grpd in (Kapulkin-Lumsdaine-Voevodsky 12), and more generally for (∞,1)-presheaf $(\infty,1)$-toposes over elegant Reedy categories in (Shulman 13). The general case is proven in Shulman 19.

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

• model of type theory in an (infinity,1)-topos

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.

Related concepts

• initiality conjecture

• categorical model of dependent types

• syntax-semantics duality

• computational trinitarianism

• Awodey's conjecture

References

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

• WikiBooks, Haskell/The Curry–Howard isomorphism

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:

• Thorsten Altenkirch, Ambrus Kaposi, Type Theory in Type Theory using Quotient Inductive Types, (2015) (pdf), (formalisation in Agda).

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 categorical semantics of linear logic in star-autonomous categories is due to

• R. A. G. Seely, Linear logic, $\ast$-autonomous categories and cofree coalgebras, in Categories in Computer Science and Logic, Contemporary Mathematics 92 (1989) [pdf, ps.gz, ISBN:978-0-8218-5100-5]

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:

• Matthijs Vákár, Syntax and Semantics of Linear Dependent Types [arXiv:1405.0033]

• Mitchell Riley, Eric Finster, Daniel Licata, Synthetic Spectra via a Monadic and Comonadic Modality [arXiv:2102.04099]

• Mitchell Riley, Extending Homotopy Type Theory with Linear Type Formers, talk at The ForML Lab (2021) [web, video]

• Mitchell Riley, A Bunched Homotopy Type Theory for Synthetic Stable Homotopy Theory, PhD Thesis (2022) [doi:10.14418/wes01.3.139, ir:3269, pdf]

  (using ideas from bunched logic)

• Mitchell Riley, Linear Homotopy Type Theory, talk at: HoTTEST Event for Junior Researchers 2022 (Jan 2022) [slides: pdf, video: YT]

The relation between typed lambda-calculus and cartesian closed categories is discussed in part I, and the adjunction between the category of type theories with product types and toposes is discussed in chapter II of:

• Joachim Lambek, Philip J. Scott, Introduction to higher order categorical logic, Cambridge Studies in Advanced Mathematics 7 (1986) [ISBN: 0-521-24665-2, pdf]

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. 95 (1984) 33-48 [doi:10.1017/S0305004100061284, 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 (1993) 51-86 [doi:10.5555/175469.175471] and: Diagrammes 23 (1990) 43-66 [numdam:DIA_1990__23__43_0]

• Martin Hofmann, On the interpretation of type theory in locally cartesian closed categories, in Computer Science Logic. CSL 1994, Lecture Notes in Computer Science 933 (1994) 427–441 [doi:10.1007/BFb0022273]

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, doi:10.1007/978-3-642-21691-6_10]

and

• Pierre-Louis Curien, Richard Garner, Martin Hofmann, Revisiting the categorical interpretation of dependent type theory, Theoretical Computer Science 546 21 (2014) 99-119 [doi:10.1016/j.tcs.2014.03.003, pdf]

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

• Peter LeFanu Lumsdaine, Michael Warren, An overlooked coherence construction for dependent type theory, CT2013 (pdf)

• Peter LeFanu Lumsdaine, Michael Warren, The local universes model: an overlooked coherence construction for dependent type theories (arXiv:1411.1736)

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

• André Joyal, Remarks on homotopical logic, Oberwolfach (2011) (pdf)

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

• Steve Awodey, Type theory and homotopy (pdf)

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

• Michael Shulman, Univalence for inverse diagrams and homotopy canonicity (From type theory and homotopy theory to Univalent Foundations of Mathematics), Mathematical Structures in Computer Science 25 5 (2015) [arXiv:1203.3253, doi:/10.1017/S0960129514000565]

with lecture notes in

• Mike Shulman, Categorical models of homotopy type theory, April 13, 2012 (pdf)

• André Joyal, Remarks on homotopical logic, Oberwolfach (2011) (pdf)

• André Joyal, Categorical homotopy type theory, March 17, 2014 (pdf)

See also

• Chris Kapulkin, Type theory and locally cartesian closed quasicategories, Oxford 2014 (video)

• Chris Kapulkin, Peter LeFanu Lumsdaine, The homotopy theory of type theories, Advances in Mathematics 337 (2018) 1-38 (arXiv:1610.00037, doi:10.1016/j.aim.2018.08.003)

• Chris Kapulkin, Karol Szumilo, Internal Language of Finitely Complete $(\infty,1)$-categories (arXiv:1709.09519)

• Valery Isaev, Algebraic Presentations of Dependent Type Theories (arXiv:1602.08504)

• Valery Isaev, Morita equivalences between algebraic dependent type theories (arXiv:1804.05045)

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

• Mike Shulman, Inductive and higher inductive types (2012) (pdf)

Categorical semantics of univalent type universes is discussed in

• Steve Awodey, Type theory and homotopy (2010) (pdf)

• Chris Kapulkin, Peter LeFanu Lumsdaine, Vladimir Voevodsky, The Simplicial Model of Univalent Foundations (arXiv:1211.2851)

• Michael Shulman, The univalence axiom for elegant Reedy presheaves (arXiv:1307.6248)

• David Gepner, Joachim Kock, Univalence in locally cartesian closed ∞-categories (arXiv:1208.1749)

• Denis-Charles Cisinski, Univalent universes for elegant models of homotopy types (arXiv:1406.0058)

Proof of Awodey's conjecture, that all ∞-stack (∞,1)-topos have presentations by model categories which interpret (provide categorical semantics) for homotopy type theory with univalent type universes:

• Michael Shulman, All $(\infty,1)$-toposes have strict univalent universes (arXiv:1904.07004).

Introduction and review in:

• Emily Riehl, On the $\infty$-topos semantics of homotopy type theory, lecture at Logic and higher structures CIRM (Feb. 2022) [pdf, pdf]

Discussion of weak Tarskian homotopy type universes is in

• Zhaohui Luo, Notes on Universes in Type Theory, 2012 (pdf)

• Cesare Gallozzi, Constructive Set Theory from a Weak Tarski Universe, MSc thesis (2014) (pdf)

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)