nLab type-theoretic definition of category

Type-theoretic definition of category


Category theory

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

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) 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

homotopy levels


Type-theoretic definition of category


There are two main styles of definition of category in the literature: one which immediately generalises to the usual definition of internal category and one which immediately generalises to the usual definition of enriched category. Here we consider the latter definition, and show how it may naturally be expressed in dependent type theory.

Note that in a type theory without identity types, where types are presets (without an inherent equality predicate), it is not manifestly possible to express concepts that violate the principle of equivalence; in that categories are not necessarily strict. In homotopy type theory, we have identity types, but they are not extensional; thus it is also possible to define non-strict categories there (but there is a subtlety; see below).


In a dependent type theory with dependent record types? we can define a type of categories as follows.

We use a two-dimensional syntax, which is convenient to allow inference of implicit parameters?, and to signify notation. We read the horizontal line as a rule, so for instance the second line means that whenever aa and bb have type Obj\mathrm{Obj}, then we have a type hom(a,b)\hom(a,b) (with equality).

The notation p∶−Pp\coloneq P signifies that pp is a proof of the proposition PP (under propositions as types or propositions as some types, this may be the same as p:Pp\colon P, but many type theories treat propositions as distinct from types).

{ Obj:Type, a,b:Objhom(a,b):Type =, a:Obj1 a:hom(a,a), f:hom(b,c)g:hom(a,b)fg:hom(a,c), g:hom(a,b)left-unit∶−1 bg=g, f:hom(a,b)right-unit∶−f1 a=f, f:hom(c,d)g:hom(b,c)h:hom(a,b)-assoc∶−f(gh)=(fg)h }\begin{aligned} \biggl\{&\mathrm{Obj}\colon\mathrm{Type}, \\ &\frac{a,b\colon\mathrm{Obj}}{\hom(a,b)\colon\mathrm{Type}_=}, \\ &\frac{a\colon\mathrm{Obj}}{1_a\colon\hom(a,a)}, \\ &\frac{f\colon\hom(b,c) \quad g\colon\hom(a,b)}{f\circ g\colon\hom(a,c)}, \\ &\frac{g\colon\hom(a,b)}{\mathrm{left}\text{-}\mathrm{unit}\coloneq 1_b\circ g=g}, \\ &\frac{f\colon\hom(a,b)}{\mathrm{right}\text{-}\mathrm{unit}\coloneq f\circ 1_a=f}, \\ &\frac{f\colon\hom(c,d) \quad g\colon\hom(b,c) \quad h\colon\hom(a,b)}{\circ\text{-}\mathrm{assoc}\coloneq f\circ(g\circ h) = (f\circ g)\circ h} \\ &\!\biggr\} \end{aligned}

Here, Type\mathrm{Type} is a type of types, and Type =\mathrm{Type}_= is a type of types with equality predicates (we may or may not have Type=Type =\mathrm{Type}=\mathrm{Type}_=). Specifically:

  • In extensional type theory (with extensional identity types), we have Type=Type =\mathrm{Type} = \mathrm{Type}_=, and the above definition simply makes no use of the equality predicate on the type of objects. In this case we obtain strict categories, although that is not immediately visible from the definition.

  • In dependent type theory without identity types, basically the only option for Type =\mathrm{Type}_= is the type of setoids. In this case we obtain a notion of non-strict category, since the type of objects has no equality predicate at all.

  • In homotopy type theory, it is natural to take Type =\mathrm{Type}_= to be the type of h-sets: types whose identity/path types behave extensionally. We should also restrict the homotopy level of the type of objects, however, since a true 1-category should have no more than a 1-groupoid of objects; thus Type\mathrm{Type} in the definition above is really the type of h-groupoids instead of the type of all small types. That is, we should take Obj\mathrm{Obj} to be 11-truncated in addition to taking each hom(a,b)\hom(a,b) to be 00-truncated.

    This gives a notion of non-strict category (since there is no equality predicate on a 11-truncated type other than isomorphism). However, it is not quite the right definition of “11-category” in homotopy type theory, because nothing requires that the paths in Obj\mathrm{Obj} are the same as the isomorphisms defined categorically. We need to impose a version of the “completeness” condition on a complete Segal space; in other words, we require that the core of the category be the equivalent as a groupoid to the original type of objects.


The defined type of categories cannot itself be a member of Type\mathrm{Type}, otherwise we run into Girard's paradox. This is related to the size issues for categories.

Last revised on October 4, 2021 at 13:32:10. See the history of this page for a list of all contributions to it.