nLab theory of categories



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


Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory




The geometric theory of categories 𝕂\mathbb{K} is a first-order axiomatisation of the concept of a category. 𝕂\mathbb{K} is (morally) an essentially algebraic theory, and literally a cartesian theory i.e. grosso modo a regular theory where existential quantification is provably unique.

Historically, the first axiomatisation was given by F. William Lawvere in his dissertation in 1963 as part of a formalisation of the category of categories (cf. Lawvere (1963) or ETCC for further information).


The signature Σ 𝕂\Sigma_\mathbb{K} has two sorts OO and AA for objects and arrows, respectively, three function symbols d 0:AOd_0:A\to O , d 1:AOd_1:A\to O and id:OAid:O\to A, assiging to morphisms their domain, respectively, codomain and to the objects their identity morphisms, as well as a relation symbol CA×A×AC\rightarrowtail A\times A\times A expressing composition of morphisms.

The theory of categories is the theory 𝕂\mathbb{K} over the signature Σ 𝕂\Sigma_\mathbb{K} with the following sequents:1

  • d 0(id(x))=xd 1(id(x))=x\top\vdash d_0(id(x))=x\wedge d_1(id(x))=x\quad ,

  • C(f 1,f 2,f 3)d 0(f 1)=d 0(f 3)d 1(f 1)=d 0(f 2)d 1(f 2)=d 1(f 3)C(f_1,f_2,f_3)\vdash d_0(f_1)=d_0(f_3)\wedge d_1(f_1)=d_0(f_2)\wedge d_1(f_2)=d_1(f_3)\quad ,

  • C(f 1,f 2,f 3)C(f 1,f 2,f 4)f 3=f 4C(f_1,f_2,f_3)\wedge C(f_1,f_2,f_4)\vdash f_3=f_4\quad ,

  • d 1(f 1)=d 0(f 2)f 3C(f 1,f 2,f 3)d_1(f_1)=d_0(f_2)\vdash\exists f_3 C(f_1,f_2,f_3)\quad ,

  • C(f,id(d 1(f)),f)C(id(d 0(f)),f,f)\top \vdash C(f,id(d_1(f)),f)\wedge C(id(d_0(f)),f,f)\quad ,

  • C(f 1,f 2,f 4)C(f 2,f 3,f 5)C(f 4,f 3,f 6)C(f 1,f 5,f 7)f 6=f 7C(f_1,f_2,f_4)\wedge C(f_2,f_3,f_5)\wedge C(f_4,f_3,f_6)\wedge C(f_1,f_5,f_7)\vdash f_6=f_7\quad .


The third axiom implies that the existential quantification occurring in the fourth axioms is unique thus 𝕂\mathbb{K} is indeed cartesian. Since the chosen signature uses a composition relation instead of a partial composition operation the theory as given here is not literally essentially algebraic in the syntactic sense, though, of course, it is Morita equivalent to an essentially algebraic axiomatisation. Other signatures, like a single sorted “arrows only” one, are also possible, the one used here (taken from Johnstone 1977) leans on the so called elementary theory of abstract categories as presented in Lawvere (1966).


Foremost, we have


Let \mathcal{E} be a Grothendieck topos. Then Mod 𝕂()=cat()Mod_{\mathbb{K}}(\mathcal{E})=cat(\mathcal{E}) with cat()cat(\mathcal{E}) the category of (small) internal categories in \mathcal{E} with internal functors as morphisms.\qed


The classifying topos Set[𝕂]Set[\mathbb{K}] is the presheaf topos on the opposite of the category of finitely presentable categories in SetSet.

This follows from the fact that the classifying toposes of cartesian theories are generally given as the presheaf toposes on the opposite of the category of finitely presentable models in SetSet (cf. Johnstone 2002, p.891).2 The proposition holds more generally with SetSet replaced by an arbitrary topos \mathcal{E} with a natural numbers object (cf. Johnstone-Wraith 1978, p.226).\qed

  • The theory 𝕂 2 \mathbb{K}^2 of 𝕂 \mathbb{K} -model homomorphisms is the theory of functors.

  • Recall that a discrete opfibration is an internal functor F:FCF\,:\,\mathbf{F}\to \mathbf{C} with the property that the following diagram

    F 1 d 0 F 0 γ 1 γ 0 C 1 d 0 C 0 \array{ & & \\ F_1 &\overset{d_0}{\longrightarrow}& F_0 \\ {}^{\mathllap{\gamma_1}} \downarrow & & \downarrow^{\mathrlap{\gamma_0}} \\ C_1 &\underset{d_0}{\longrightarrow}& C_0 \\ & & }

    is pullback. Whence by adding the appropriate geometric axiom to the theory 𝕂 2\mathbb{K}^2 of functors one obtains as a quotient the theory of discrete opfibrations 𝕂 2\mathbb{K}^2_\downarrow.

    Let Ccat()\mathbf{C}\in cat(\mathcal{E}) be an internal category. By pulling back its classifying morphism C¯:[𝕂]\overline{\mathbf{C}}\,:\,\mathcal{E}\to \mathcal{E}[\mathbb{K}] along the geometric morphism d 1:[𝕂 2][𝕂]d_1\,:\,\mathcal{E}[\mathbb{K}^2_\downarrow]\to \mathcal{E}[\mathbb{K}] that classifies the codomain of the generic discrete opfibration as an internal category

    [𝕂 C ] [𝕂 2] d 1 C¯ [𝕂] \array{ \mathcal{E}[\mathbb{K}^\downarrow_\mathbf{C}] &\longrightarrow &\mathcal{E}[\mathbb{K}^2_{\downarrow}] \\ \downarrow & & \downarrow^{d_1} \\ \mathcal{E} &\underset{\overline{\mathbf{C}}}{\longrightarrow}& \mathcal{E}[\mathbb{K}] \\ & & }

    one obtains the classifying topos [𝕂 C ]\mathcal{E}[\mathbb{K}^{\downarrow}_\mathbf{C}] for discrete opfibrations on C\mathbf{C}, or, equivalently, internal diagrams (=copresheaves) on C\mathbf{C}. Since an internal profunctor CD\mathbf{C} ⇸ \mathbf{D} is by definition an internal diagram on C op×D\mathbf{C}^{op}\times\mathbf{D}\,, one can use this construction to obtain the classifying topos for internal profunctors from C\mathbf{C} to D\mathbf{D} by pulling back along the classifying morphism for C op×D\mathbf{C}^{op}\times\mathbf{D} (cf. Johnstone 1977, p.209).

  • By adding the following sequents to the theory 𝕂\mathbb{K} of categories one obtains the theory of filtered categories 𝕂 >\mathbb{K}^\gt with models the internal filtered categories (cf. Johnstone 1977, p.203):

    x(x=x) f 1f 2(d 0(f 1)=xd 0(f 2)=yd 1(f 1)=d 1(f 2)) d 0(f 1)=d 0(f 2)d 1(f 1)=d 1(f 2)f 3f 4(C(f 1,f 3,f 4)C(f 2,f 3,f 4))\array{\\ \top\vdash \exists x (x=x) \\ \\ \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\top\vdash \exists f_1\exists f_2 (d_0(f_1)=x\wedge d_0(f_2)=y\wedge d_1(f_1)=d_1(f_2)) \\ d_0(f_1)=d_0(f_2)\wedge d_1(f_1)=d_1(f_2)\vdash \exists f_3\exists f_4\big (C(f_1,f_3,f_4)\wedge C(f_2,f_3,f_4)\big )\quad}


  1. Here and in the following x,yx,y are variables ranging over O, whereas the f 1,f 2,f_1,f_2,\dots range over A; the contexts are assumed to be canonical i.e. consisting of all free distinct variables occurring in a sequent listed in order of first appearance.

  2. Apparently Set[𝕂]Set[\mathbb{K}] made its first appearance in Johnstone’s 1974 Cambridge dissertation on “Internal category Theory” (cf. Tierney 1976).

Last revised on April 27, 2023 at 13:41:50. See the history of this page for a list of all contributions to it.