nLab
relation between type theory and category theory

Skip the Navigation Links | Home Page | All Pages | Recently Revised | Authors | Feeds | Export |

under construction

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

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-level 1-type/h-prop
proofgeneralized elementprogram
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 monadmodal type theory, monad (in computer science)

homotopy levels

semantics

Category theory

category theory

Concepts

Universal constructions

Theorems

Extensions

Applications

Contents

Idea

type theory? and certain kinds of category theory are closely related. 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 kind sof (∞,1)-category theory.

Overview

flavor of type theoryequivalent toflavor of category theory
intuitionistic propositional logic?/simply-typed lambda calculus?cartesian closed category
intuitionistic linear logic?monoidal closed category
classical linear logic?star-autonomous category
first-order logichyperdoctrine(Seely 1984a)
Martin-Löf dependent type theorylocally cartesian closed category(Seely 1984b)
homotopy type theorylocally cartesian closed (∞,1)-category(conjectural)
homotopy type theory with higher inductive types and univalenceelementary (∞,1)-topos(conjectural)

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

Theorem

The functors

constitute an equivalence of categories

FirstOrderTheories→Cont←LangHyperdoctrines.FirstOrderTheories \stackrel{\overset{Lang}{\leftarrow}}{\underset{Cont}{\to}} Hyperdoctrines \,.

(Seely, 1984a)

Martin-Löf dependent type theory and locally cartesian closed categories

Theorem

There are 2-functors

that constitute an equivalence of 2-categories

MLDependentTypeTheories→Cont←LangLocallyCartesianClosedCategories.MLDependentTypeTheories \stackrel{\overset{Lang}{\leftarrow}}{\underset{Cont}{\to}} 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.

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. ∏ a:AB[a] (dependent product), written also (A→B) if B[x] in fact does not depend on x;

      2. ∑ a:AB[a] (dependent sum), written also A×B if B[x] in fact does not depend on x;

  2. term formation rules

    1. *∈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

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)

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∑ b∈B(f(a)=g(b)).P \simeq \sum_{a : A} \sum_{b \in B} (f(a) = g(b)) \,.

The equalizer

P→A→g→fBP \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]≃(A→B).[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∈Con(T) the category P(T)(A) to have as objects the A-dependent types and as morphisms (a:A⊢X(a):type)→(a:A⊢Y(a):type) the terms of dependent function type (a:A⊢t:(X(a)→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≃P(T)(A).Con(T)_{/A} \simeq P(T)(A) \,.

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

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

Conversely, for a:A⊢X(a) a dependent type, send it to the projection ∑ a:AX(a)→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)→C.Con(T) \to C \,.

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

Con(T)→Con(T′).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→A;

  • a context x 1:X,x 2:X,⋯,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] are the sections A→B in C /A

  • the equality type (x A=y A) is the diagonal A→A×A

  • …

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

(…)

Homotopy type theory with univalence and elementary (∞,1)-toposes

(…)

References

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)

A lecture reviewing aspects involved in this equivalence is (see the discussion building up to the theorem on slide 96)

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.

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

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

The suggestion that with univalence this is refined to (∞,1)-topos theory appears around

A precise definition of elementary (infinity,1)-topos inspired by giving a natural equivalence to homotopy type theory with univalence was then proposed 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)

Revised on April 18, 2013 16:33:11 by Mike Shulman (192.16.204.218)
Edit | Back in time (16 revisions) | See changes | History | Views: Print | TeX | Source | Linked from: category theory, groupoid, isomorphism, enriched category theory, sheaf and topos theory, anafunctor, morphism, category, group, equivalence, natural isomorphism, natural transformation, functor, topos, composition, epimorphism, presheaf, skeleton, monoid, Cat, Set, set, function, Ab, forgetful functor, category algebra, functor category, monoidal category, enriched category, end, Kan extension, representable functor, subobject, diagram, limit, cone, multicategory, span, opposite category, hom-functor, logic, cartesian monoidal category, extensive category, sieve, simplicial object, zero object, initial object, cartesian closed category, locally cartesian closed category, simplex category, orthogonal factorization system, internal category, arrow category, free functor, projective object, Rel, nerve, image, allegory, geometric realization, regular category, inhabited set, regular epimorphism, Yoneda lemma, fundamental category, coherent category, Heyting category, exact category, pretopos, balanced category, adjoint functor, internally projective object, Yoneda embedding, Cauchy complete category, coproduct, fibration, Grothendieck fibration, concrete category, endofunctor, monomorphism, orthogonality, Galois connection, regular monomorphism, internal logic, finite object, context, colimit, intersection, span trace, reflective subcategory, trace, string diagram, homotopy n-type, profunctor, essentially algebraic theory, Grpd, retract, idempotent, free cocompletion, dagger-category, SimpSet, comma category, weak equivalence, equivalence of categories, homotopy type, 1-groupoid, internal hom, partial order, negation, disjoint union, quotient object, full subcategory, filtered category, pro-object, ind-object, category of elements, FinSet, wedge sum, congruence, accessible category, sketch, locally presentable category, Categories and Sheaves, cogenerator, stuff, structure, property, right adjoint, zero morphism, kernel, cokernel, universal construction, bimorphism, exact functor, Thomason model structure, pre-abelian category, additive and abelian categories, direct product, group object, wide subcategory, injective object, closed monoidal structure on presheaves, type theory, co-Yoneda lemma, exact sequence, sequent calculus, coreflective subcategory, dependent product, exponential object, calculus of fractions, monadic functor, distributive category, category of simplices, flat functor, locally finitely presentable category, algebra for an endofunctor, coimage, higher category theory and physics, split idempotent, coalgebra for an endofunctor, path category, Grothendieck construction, core, computer science, triangle identities, adjoint equivalence, nerve and realization, generalized multicategory, effective epimorphism, noetherian category, Karoubi envelope, Cartesian morphism, internal relation, category theory - contents, type, free groupoid, injective hull, strict category, preset, tensor category, completion, propositions as types, syntax - semantics duality, regular and exact completions, finitely generated object, proposition, extranatural transformation, monadicity theorem, bifibration, codomain fibration, Beck-Chevalley condition, species, cleavage, inhabited object, covering, Grothendieck-Maltsiniotis infinity-category, adjoint triple, semifunctor, theory, free object, dependent type, applications of (higher) category theory, Tannaka duality, Como, idempotent adjunction, semicategory, W-type, category of presheaves, type theory - contents, first-order hyperdoctrine, tripos, identity type, display map, calculus of constructions, finite quantum mechanics in terms of dagger-compact categories, direct category, accessible functor, Hall algebra, forcing, signature (in logic), Horn theory, zigzag, C-star-category, Gabriel-Ulmer duality, sifted category, thin category, Freyd-Mitchell embedding theorem, indexed functor, algebraic model for modal logics, associativity, zigzag category, codiagonal, pure type system, cartesian functor, the logic S4(m), modal logic, Haefliger groupoid, ring object, evaluation map, normal modal logic, indexed category, geometric realization of categories, pure morphism, adjoint lifting theorem, factorization category, term, projection, variable, Frobenius reciprocity, Handbook of Categorical Algebra, geometric category, cartesian logic, hyperdoctrine, two-out-of-three, categorical semantics, lambda-calculus, syntactic category, cartesian theory, axiom, homotopy type theory, fiber functor, type of propositions, theorem, truncated object, unit type, pure subobject, type of types, types and logic - table, axiom UIP, Boolean hyperdoctrine, contents of contents, locally presentable categories - introduction, syntax, product type, quotient type, concrete object, stack semantics, cohesive homotopy type theory, abstract general, concrete general and concrete particular, reflective factorization system, tensor, Mac Lane's proof of the coherence theorem for monoidal categories, M-complete category, stable factorization system, homotopy level, function type, bracket type, (eso+full, faithful) factorization system, (eso, fully faithful) factorization system, dependent product type, filtered object, Coq, empty type, inductive type, Agda, higher inductive type, existential quantifier, universal quantifier, positive type, proofs as programs, proof, HoTT methods for homotopy theorists, univalence axiom, intensional type theory, type-theoretic model category, judgmental equality, dependent type theory, contractible type, extensional type theory, sum type, cartesian closed functor, codiscrete object, semantics, locally cartesian closed (infinity,1)-category, h-set, decidability, h-proposition, equivalence in homotopy type theory, dual object in a closed category, Cartan-Eilenberg category, canonical form, polymorphism, adhesive category, coherent hyperdoctrine, negative type, type formation, beta-reduction, dependent sum type, exactness property, elementary (infinity,1)-topos, Segal condition, exhaustive category, substitution, fixed-point combinator, relation between type theory and category theory, M-type, categorical wreath product, locally bounded category, categorical model of dependent types, sequent, first-order theory, Haskell, permutative category, logical framework, Burali-Forti's paradox, Gallina specification language, judgment, Russell's paradox, distributivity pullback, projective presentation, context extension, function application, Baer's criterion, tower, bifunctor, injective presentation, abelianization, numeral, definition, program, gaunt category, elementary function arithmetic, Brouwer-Heyting-Kolmogorov interpretation, second-order arithmetic, computational trinitarianism, arity class, monad (in computer science), computation, programming language, natural deduction, transfinite construction of free algebras, metalanguage, theory of presheaf type, Practical Foundations for Programming Languages, term in context, Tannakian category, contradiction, inconsistency, modal type, type of h-sets, Bishop set, antecedent, succedent, consequent, looping combinator, deductive system, pointed endofunctor, dependent sum, h-groupoid, coinductive type, practical foundation of mathematics, adjoint triangle theorem, separator, modal type theory, differential homotopy type theory, strict initial object, axiom K, mapping stack, observational type theory, meaning explanation, natural numbers type, equifibered natural transformation, van Kampen colimit