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

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/path type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
completely presented setdiscrete object/0-truncated objecth-level 2-type/set/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
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}


  • P. J. Freyd, A. Scedrov, Categories, Allegories , North-Holland Amsterdam 1990.

  • Peter Johnstone, Topos Theory , Academic Press New York (1977). (Also available as Dover Reprint, Mineola 2014, p.202f)

  • Peter Johnstone, Sketches of an Elephant vol.2 , Oxford UP 2002. (D1.1.7(e), p.813, D1.3.4, p.833)

  • Peter Johnstone, Gavin Wraith, Algebraic Theories in Toposes , pp.141-242 in Johnstone, Paré (eds.), Indexed Categories and Their Applications , Springer LNM 661 Heidelberg 1978.

  • F. W. Lawvere, Functorial Semantics of Algebraic Theories , Ph.D. thesis, Columbia University New York 1963. (With an author’s comment and a supplement in: Reprints in Theory and Applications of Categories, no.5 (2004) pp.1-121 (pdf))

  • F. W. Lawvere, The Category of Categories as a Foundation for Mathematics , pp.1-20 in Eilenberg, Harrison, MacLane, Röhrl (eds.), Proceedings of the Conference on Categorical Algebra - La Jolla 1965, Springer Heidelberg 1966.

  • Myles Tierney, Forcing Topologies and Classifying Toposes , pp.211-219 in Heller, Tierney (eds.), Algebra, Topology and Category Theory , Academic Press New York 1976.

  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 October 2, 2020 at 17:54:33. See the history of this page for a list of all contributions to it.