An Invitation to Geometric Type Theory

Owen Lynch

Joint work with: David Jaz Myers

Geometric Type Theory is a conjectured type theory that would provide an internal language for the 2-category of topoi [6]. In this talk, we give a direct construction of a category with familes (CwF, [1]) permitting interpretation of such a type theory. This is inspired by a close reading of the Elephant [3]; Johnstone defines a geometric theory over a fixed topos $\mathcal{S}$ to be a 2-functor $\mathcal{T}$ from $(\mathsf{BTop}/\mathcal{S})^{\mathrm{op}}$ to $\mathsf{Cat}$ that is built by applying a sequence of PIE limits to the object classifier $T_{0}(\mathcal{E})=\mathcal{E}$ . From this, we define a CwF:

CwF sort	Interpretation
Context $\Gamma$	Geometric theory $\Gamma\colon\mathsf{Top}^{\mathrm{op}}\to\mathsf{Cat}$
Substitution $\Delta\vdash\gamma\colon\Gamma$	2-natural transformation $\gamma\colon\Delta\Rightarrow\Gamma$
Type $\Gamma\vdash A\,\mathsf{type}$	Geometric theory over $\Gamma$ , that is $A\colon\int\Gamma\to\mathsf{Cat}$
Term $\Gamma\vdash a\colon A$	Natural section $a(\mathcal{E},M)\in A(\mathcal{E},M)$ for $(\mathcal{E},M)\in\int\Gamma$

Note that $\int\Gamma$ is equivalent to topoi sliced over the classifying topos for $\Gamma$ , by representability of geometric theories. This CwF then supports a rich variety of type formers.

Example 1.

There is a type $\Gamma\vdash\mathsf{Sort}\,\mathsf{type}$ that is is given semantics by the object classifier $\int\Gamma\to\mathsf{Cat}$ defined by $(\mathcal{E},M)\mapsto\mathcal{E}$ . Given $\Gamma\vdash A\colon\mathsf{Sort}$ , we have another type $\Gamma\vdash\mathsf{Elt}\,A\,\mathsf{type}$ defined by $(\mathcal{E},M)\mapsto\mathcal{E}(1,A(\mathcal{E},M))$ , so $\mathsf{Sort}$ acts as a “universe of small types”. The object classifier $\mathsf{Sort}$ serves a dual role: it helps us build up theories, but additionally when we work internally to $\mathsf{Sort}$ in a fixed context $\Gamma$ we get the positive fragment of the internal language for the classifying topos for $\Gamma$ .

Example 2.

There is a “ $\Pi$ -type with small codomain” $(x\colon A)\to B$ defined for $\Gamma\vdash A\colon\mathsf{Sort}$ and $\Gamma,x\colon\mathsf{Elt}\,A\vdash B\,\mathsf{type}$ . The interpretation of $(x\colon A)\to B$ on $(\mathcal{E},M)\in\int\Gamma$ is given by interpreting $B[x]$ in the slice topos $\mathcal{E}/A(\mathcal{E},M)$ , where $x$ is the global element of $A$ in $\mathcal{E}/A(\mathcal{E},M)$ given by the identity.

We also have $\Sigma$ -types, both globally and within the $\mathsf{Sort}$ universe.

In fact, this construction scales beyond just topoi/geometric theories. From Garner and Lack [2], we know that various fragments of geometric logic correspond to sub 2-monads of $\mathsf{Psh}\colon\mathsf{Lex}\to\mathsf{Lex}$ given by completion under various classes of weighted colimits. Type theoretically, this corresponds to allowing different kinds of (strictly positive) type formers. For instance, regular logic corresponds to adding propositional truncation, with the elimination principle as given in the HoTT book [4]. Especially interesting for us is the setting of arithmetic universes [5], which interprets quotient inductive inductive types.

[1] Peter Dybjer. Internal type theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs, pages 120–134, Berlin, Heidelberg, 1996. Springer. doi:10.1007/3-540-61780-9_66.
[2] Richard Garner and Stephen Lack. Lex colimits. Journal of Pure and Applied Algebra, 216(6):1372–1396, June 2012. doi:10.1016/j.jpaa.2012.01.003.
[3] P. T. Johnstone. Sketches of an Elephant: A Topos Theory Compendium. Number 43 in Oxford Logic Guides. Oxford University Press, Oxford ; New York, 2002.
[4] The Univalent Foundations Project. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute of Advanced Study, 2013. URL: https://homotopytypetheory.org/book/.
[5] Steven Vickers. Sketches for arithmetic universes. Journal of Logic and Analysis, 11(0), June 2019. doi:10.4115/jla.2019.11.FT4.
[6] Johannes Schipp von Branitz and Ulrik Buchholtz. Propositional Geometric Type Theory, April 2025. URL: https://hott-uf.github.io/2025/slides/Schipp_von_Branitz.pdf.