natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/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 $O$ and $A$ for objects and arrows, respectively, three function symbols $d_0:A\to O$ , $d_1:A\to O$ and $id:O\to A$, assiging to morphisms their domain, respectively, codomain and to the objects their identity morphisms, as well as a relation symbol $C\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}
$\top\vdash d_0(id(x))=x\wedge d_1(id(x))=x\quad$ ,
$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)\wedge C(f_1,f_2,f_4)\vdash f_3=f_4\quad$ ,
$d_1(f_1)=d_0(f_2)\vdash\exists f_3 C(f_1,f_2,f_3)\quad$ ,
$\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)\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_{\mathbb{K}}(\mathcal{E})=cat(\mathcal{E})$ with $cat(\mathcal{E})$ the category of (small) internal categories in $\mathcal{E}$ with internal functors as morphisms.$\qed$
The classifying topos $Set[\mathbb{K}]$ is the presheaf topos on the opposite of the category of finitely presentable categories in $Set$.
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 $Set$ (cf. Johnstone 2002, p.891).^{2} The proposition holds more generally with $Set$ replaced by an arbitrary topos $\mathcal{E}$ with a natural numbers object (cf. Johnstone-Wraith 1978, p.226).$\qed$
The theory $\mathbb{K}^2$ of $\mathbb{K}$-model homomorphisms is the theory of functors.
Recall that a discrete opfibration is an internal functor $F\,:\,\mathbf{F}\to \mathbf{C}$ with the property that the following diagram
is pullback. Whence by adding the appropriate geometric axiom to the theory $\mathbb{K}^2$ of functors one obtains as a quotient the theory of discrete opfibrations $\mathbb{K}^2_\downarrow$.
Let $\mathbf{C}\in cat(\mathcal{E})$ be an internal category. By pulling back its classifying morphism $\overline{\mathbf{C}}\,:\,\mathcal{E}\to \mathcal{E}[\mathbb{K}]$ along the geometric morphism $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
one obtains the classifying topos $\mathcal{E}[\mathbb{K}^{\downarrow}_\mathbf{C}]$ for discrete opfibrations on $\mathbf{C}$, or, equivalently, internal diagrams (=copresheaves) on $\mathbf{C}$. Since an internal profunctor $\mathbf{C} ⇸ \mathbf{D}$ is by definition an internal diagram on $\mathbf{C}^{op}\times\mathbf{D}\,$, one can use this construction to obtain the classifying topos for internal profunctors from $\mathbf{C}$ to $\mathbf{D}$ by pulling back along the classifying morphism for $\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):
$\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.
Here and in the following $x,y$ are variables ranging over O, whereas the $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. ↩
Apparently $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 21:54:33. See the history of this page for a list of all contributions to it.