GATs and the semantics of dependent type theory
Berkeley Seminar
2023-09-11
Warmup
% https://tex.stackexchange.com/a/269194
First, syntax of ATs…
An algebraic theory (AT) is expressed in a syntax that has the judgments:
\[\begin{align*} A\ \mathtt{type}&& \Gamma\ \mathtt{context}&& t:A\dashv \Gamma&& t=s:A\dashv \Gamma \end{align*}\]
Context is short for “context of variables”, so that given some variables of some types we may be able to construct a term of another type, or assert that two such terms are equal.
Example: Monoid actions
The theory of a set with a monoid action has \(S,M\ \mathtt{type}\) with operators
- \(e:M\dashv\)
- \(\mu(m,n):M\dashv m,n : M\)
- \(\mu_S(m,s):S\dashv m:M,s:S\)
and equations expressing that \((M,\mu,e)\) is a monoid and \(\mu_S\) gives an action of \((M,\mu,e)\) on \(S.\)
Semantics of ATs…
Plain algebraic theories have models in any category with finite products (cartesian category) \(\mathsf{C}\).
A model of an AT
- Types \(A,B\) are interpreted in a model \(X\) as chosen objects \(A_X,B_X\) in \(\mathsf{C}\)
- Contexts such as \(x:A,y:B\) are interpreted as products \(A_X\times B_X.\)
- Terms such as \(t(x,y):C\dashv x:A,y:B\) are interpreted as morphisms \(t_X:A_X\times B_X\to C_X.\)
- Equations are interpreted as equalities between morphisms.
Fancier: Every AT presents a category \(\mathsf{F}\) with finite products.
- The objects are the types one can prove must exist
- The morphisms are the terms one can prove must exist
- The relations are the equations one can prove must hold
A model of the theory is nothing but a finite product-preserving functor \(\mathsf{F}\to \mathsf{C}.\)
Fancy semantics for monoid actions
The cartesian category representing monoid actions
The theory of monoid actions generates the category \(\mathsf{F}\) with…
- Objects including \(S,M,(),M^2,M\times S,\) but also \(S^3\times M^2\times S\times M\) etc.
- Morphisms including \(e:()\to M, \mu:M\times M\to M,\mu_S:M\times S\to S,\) but also \((m\cdot n\cdot o)\cdot s:M^3\times S\to S,\) etc.
- Relations generated by associativity and unitality constraints. (Unless you give a cleverer presentation!)
Finite product-preserving functors out of \(\mathsf{F}\) are naturally identified with models of the theory of monoid actions in \(\mathsf{C}\):
\[\mathsf{Cart}(\mathsf{F},\mathsf{C})=\mathsf{MonAct}(\mathsf{C}).\]
The identity functor \(\mathsf{F}\to \mathsf{F}\), corresponding to the model \(S_X=S,M_X=M,\mu_X=\mu,\ldots\), exhibits \(\mathsf{F}\) as the initial category-with-finite-products-and-a-monoid-action.
A takeaway
Categorical semantics of type theories is usually like this:
- You have some kind of type-theoretic language, like the ones sketched for ATs and about to be sketched for GATs
- You figure out the kind of categorical gadget needed to model that syntax
- You (try to) show the syntax presents an initial gadget-with-a-model-of-the-syntax.
More on ATs: Owen’s Berkeley seminar from May 30
More on type theory, especially on building initial gadgets out of syntax: (Shulman 2016)
On to GATs!
Syntax of GATs
GATs generalize ATs by adding the ability to have types depend on a context:
\[F(x,y)\ \mathtt{type}\dashv x:A,y:B\]
Example: 2-categories
The GAT of a 2-category has types
- \(\mathop{\mathrm{Ob}}\dashv\)
- \(\mathop{\mathrm{Hom}}(a,b)\dashv a,b:\mathop{\mathrm{Ob}}\)
- \(\mathop{\mathrm{Hom}}_2(f,g)\dashv a,b:\mathop{\mathrm{Ob}}, f,g:\mathop{\mathrm{Hom}}(a,b)\)
operators
- \(g\circ f:\mathop{\mathrm{Hom}}(a,c)\dashv a,b,c:\mathop{\mathrm{Ob}},f:\mathop{\mathrm{Hom}}(a,b),g:\mathop{\mathrm{Hom}}(b,c)\)
- \(\beta\circ\alpha:\mathop{\mathrm{Hom}}_2(f,h)\dashv f,g,h:\mathop{\mathrm{Hom}}(a,b),\alpha:\mathop{\mathrm{Hom}}_2(f,g),\beta:THom(g,h)\)
plus operators for units and horizontal composition and equations for unitality and associativity.
What are the semantics of GATs?
Not so clear what kind of category allows for models of GATs. Prototypical question:
How to interpret \(\mathop{\mathrm{Hom}}(a,b)\ \mathtt{type}\dashv a,b:\mathop{\mathrm{Ob}}\)?
A standard answer: sum all the homs up into \(s,t:\mathop{\mathrm{Hom}}\rightrightarrows \mathop{\mathrm{Ob}}.\) Then the composition operator \(g\circ f:\mathop{\mathrm{Hom}}(a,c)\dashv f:\mathop{\mathrm{Hom}}(a,b),g:\mathop{\mathrm{Hom}}(b,c)\) must be interpreted with domain the pullback:
Not quite the right answer. In \(\mathsf{Set}, \mathop{\mathrm{Hom}}\) is equivalently a function \(\mathop{\mathrm{Ob}}\times\mathop{\mathrm{Ob}}\to \mathsf{Set}.\)
Other categories can have a notion of “family of objects dependent on an object” that is not equivalent to the notion of “an arrow”!
Categories with families
Many axiomatizations of categories equipped with some notion of dependent family.
Oldest: (1) Categories with attributes and (2) contextual categories, both due to (Cartmell 1986).
Equivalent to categories with attributes: categories with families. (Dybjer 1996)
Basic idea
A category with families (cwf) is a category \(\mathsf{C}\) plus:
- The vibe that objects of \(\mathsf{C}\) are some kind of contexts
- A set \(\mathop{\mathrm{Ty}}(c)\) for every \(c\in \mathsf{C}\) of “types in context \(c\)”
- For every type \(x\) in context \(c\), a set \(\mathop{\mathrm{Tm}}(x,c)\) thought of as “terms of type \(x\)”.
- Morphisms \(f:c'\to c\) feel like “substitutions” and in particular produce functorial maps \[\begin{align*} \mathop{\mathrm{Ty}}(c)\to \mathop{\mathrm{Ty}}(c'),x\mapsto f^*x && \mathop{\mathrm{Tm}}(x,c)\to\mathop{\mathrm{Tm}}(f^*x,c'), t\mapsto f^*t. \end{align*}\]
The key example of a cwf
\(\mathbf{Set}\) has a cwf structure such that \(\mathop{\mathrm{Ty}}(X)=\{A:X\to \mathbf{Set}\}\) is the set of all families of sets over \(X\) and \(\mathop{\mathrm{Tm}}(A,X)=\{(a_x\in A_x)_{x\in X}\}\). If \(f:Y\to X\) in \(\mathbf{Set}\) and \(A\in \mathop{\mathrm{Ty}}(X)\), then \(f^*A(y)=A(f(y))\) and similarly for terms.
Example:
Let \(\mathbf{K}\) be some 2-category. We can describe \(\mathbf{K}\) in terms of the cwf \(\mathbf{Set}\):
- The objects, say \(X\), of \(\mathbf{K}\) form an object of \(\mathbf{Set}\)
- \(\mathop{\mathrm{Hom}}:X\times X\to \mathbf{Set}\) is a type over \(X\times X,\) i.e. a type in context \(x,y:X\)
- Given the type \((x,y,z,f,g)\mapsto \mathop{\mathrm{Hom}}(x,z)\) over \(\sum_{(x,y,z)\in X^3}\mathop{\mathrm{Hom}}(x,y)\times \mathop{\mathrm{Hom}}(y,z)\), composition is the term \((x,y,z,f,g)\mapsto g\circ f.\)
- \(\mathop{\mathrm{Hom}}_2:\sum_{(x,y)\in X\times X}\mathop{\mathrm{Hom}}(x,y)\times\mathop{\mathrm{Hom}}(x,y) \to \mathbf{Set}\) is a type in context \(x,y:X,f,g:\mathop{\mathrm{Hom}}(x,y)\).
…and so on.
This nearly explains how to model a GAT in a cwf. There’s only one thing missing…
An accidentally illuminating detail
The context for \(\mathop{\mathrm{Hom}}_2\) was \(x,y:X,f,g:\mathop{\mathrm{Hom}}(x,y).\) In a general cwf \(\mathsf{C},\) we’d have \(X:\mathsf{C}\) and \(\mathop{\mathrm{Hom}}:\mathop{\mathrm{Ty}}(X\times X).\) So \(\mathop{\mathrm{Hom}}\) is not yet inside of \(\mathsf{C}\) at all!
To build some analogue of this context in a cwf, we need context extension.
Context extension
In a cwf \(\mathsf{C}\) with a context \(\Gamma\) and \(A\in \mathop{\mathrm{Ty}}(\Gamma),\) there is always a terminal choice of a substitution \(\gamma:\Delta\to \Gamma\) together with a term \(t:\mathop{\mathrm{Tm}}(\gamma^*A,\Delta)\), which we call \(\pi_A:\Gamma.A\to \Gamma\) and \(q_A:\mathop{\mathrm{Tm}}(\pi_A^*A,\Gamma.A)\).
We think of the new context \(\Gamma.A\) as “extending \(\Gamma\) by a new variable from \(A\),” the substitution \(\pi_A\) as “throwing that variable away”, and the term \(q_A\) as “mapping \((x,a\in A(x))\) to \(a\)”.
Note that
- The set of sections \(s:\Gamma\to \Gamma.A\) of \(\pi_A\) is identified with \(\mathop{\mathrm{Tm}}(A,\Gamma).\)
- If \(A\in \mathop{\mathrm{Ty}}(\Gamma)\) and \(\gamma:\Delta\to \Gamma\) then for any \(\Xi\) we have \[\begin{align*} &\mathsf{C}(\Xi,\Delta.(\gamma^*A))= \{(\delta:\Xi\to \Delta,t:\delta^*\gamma^*A)\}\\ &=\{(\delta:\Xi\to \Delta,\xi:\Xi\to \Gamma,t:\xi^*A)\mid \xi=\gamma\circ \delta\}\\ &=\{\delta:\Xi\to \Delta,\eta:\Xi\to \Gamma.A\mid \gamma\circ\delta=\pi_A\circ\eta\} \end{align*}\]
The special pullbacks
The identification \[\mathsf{C}(\Xi,\Delta.\gamma^*A)=\{\delta:\Xi\to \Delta,\eta:\Xi\to \Gamma.A\mid \gamma\circ\delta=\pi_A\circ\eta\}\]
means that we have a pullback:
To interpret syntax, substitution must be strictly functorial, implying that
Pullbacks won’t act this way in most natural categories!
Coherence
We can get these strictly functorial chosen pullbacks in \(\mathsf{Set}\) only because we have the pre-existing notion of function \(X\to \mathsf{Set},\) which is not quite interchangeable with the notion of function \(A\to X\).
In particular, you can’t just start from some abstract category \(\mathsf{C}\) and construct a cwf such that families of objects over \(X\) are morphisms \(A\to X\) and substitution is implemented by an arbitrary choice of pullbacks.
This coherence problem is one of the key problems in modern semantics of type theory.
Many citations in the nLab article on categorical semantics of dependent type theory (nLab authors 2023a)
Back to GATs
2-categories in a cwf
In any cwf \((\mathsf{C},\mathop{\mathrm{Ty}},\mathop{\mathrm{Tm}})\), we can model the GAT of 2-categories by giving
- A context \(\Gamma\) (the objects)
- A type \(\mathop{\mathrm{Hom}}\) in context \(\Gamma\times \Gamma=\Gamma.\pi^*\Gamma\)
- A type \(\mathop{\mathrm{Hom}}_2\) in a context something like \(\Gamma.\pi^*\Gamma.\mathop{\mathrm{Hom}}.\pi^*\mathop{\mathrm{Hom}}\), which we inevitably have to syntactically sugar with variables as \(x:\Gamma,y:\Gamma,f:\mathop{\mathrm{Hom}}(x,y),g:\mathop{\mathrm{Hom}}(x,y).\)
- A bunch more stuff
In this way, any cwf can contain a model of any GAT!
Initiality
In parallel with the story for ATs:
- Every GAT generates a cwf made out of its contexts, types, and terms.
- This cwf is the initial cwf-with-a-model-of-this-GAT. (Morphisms of cwfs preserve everything in sight, and it doesn’t matter whether you mean that in a strict or a pseudo sense.)
- Thus we can define models of GATs purely semantically, in terms of cwf morphisms, just as we can define models of ATs in terms of cartesian category morphisms.
The free cwf on a 2-category
The cwf-containing-a-2-category generated by the GAT of 2-categories has an object \(\mathop{\mathrm{Ob}}\), which implies an object \(\mathop{\mathrm{Ob}}.\pi^*\mathop{\mathrm{Ob}}\), a type \(\mathop{\mathrm{Hom}}\) in \(\mathop{\mathrm{Ty}}(\mathop{\mathrm{Ob}}.\pi^*\mathop{\mathrm{Ob}})\), a type \(\mathop{\mathrm{Hom}}_2\) in \(\mathop{\mathrm{Ty}}(\mathop{\mathrm{Ob}}.\pi^*\mathop{\mathrm{Ob}}.\mathop{\mathrm{Hom}}.\pi^*\mathop{\mathrm{Hom}})\), and more objects and types required to build the presheaves \(\mathop{\mathrm{Ty}},\mathop{\mathrm{Tm}}\) and allow for context extension.
Plus, if we construct the context \(\Gamma = \mathop{\mathrm{Ob}}.\pi^*\mathop{\mathrm{Ob}}.\pi^*\pi^*\mathop{\mathrm{Ob}}. \pi^*\mathop{\mathrm{Hom}}.\pi^*\pi^*\mathop{\mathrm{Hom}}\) and inevitably introduce the syntactic sugar \(\Gamma=x,y,z:\mathop{\mathrm{Ob}},f:\mathop{\mathrm{Hom}}(x,y),g:\mathop{\mathrm{Hom}}(y,z),\) there’s a type \(\mathop{\mathrm{Hom}}(x,z)\in \mathop{\mathrm{Ty}}(\Gamma)\) and a term \(g\circ f\) of \(\mathop{\mathrm{Hom}}(x,z)\). …And lots more!
Digest of GAT semantics
GATs have semantics in cwfs, in the strong sense that a GAT \(\Sigma\) generates the initial cwf-with-a-model-of-\(\Sigma\).
In fact, (Bezem et al. 2021) defines \(\Sigma\) itself in mutual recursion with the notion of contextual-category-containing-a-model-of -\(\Sigma\). (If you want to add a type in context \(\Gamma\) to your GAT, you must add a type to \(\mathop{\mathrm{Ty}}(\Gamma_M)\) in a model \(M\), and similarly for adding a term or an equation.)
Then \(\Sigma\) itself is just the initial such contextual category, which characterizes what a GAT has to be without any reference to syntax. (Yay!)
Syntax becomes a way to give nice constructions of \(\Sigma\), seen as an initial cwf-with-a-model-of-\(\Sigma\).
The connection with dependent type theory
From GATs to MLTT
The most active work in the semantics of dependent type theory is on much richer languages than GATs, such as the language of Martin-Löf type theory (MLTT).
Recall that a GAT can contain types dependent on variable terms, like \(\mathop{\mathrm{Hom}}(a,b).\) But it cannot contain types dependent on variable types!
Example: Cartesian closed categories
There exists a GAT whose models in a cwf \(\mathsf{C}\) are cartesian-closed-category objects. Beyond \(\mathop{\mathrm{Ob}}\) and \(\mathop{\mathrm{Hom}}(a,b),\) we add term constructors like \[\operatorname{Prod}(a,b):\mathop{\mathrm{Ob}}\dashv a,b:\mathop{\mathrm{Ob}}\text{ and }\operatorname{Fun}(a,b):\mathop{\mathrm{Ob}}\dashv a,b:\mathop{\mathrm{Ob}}\] and, as usual, a bunch more.
But there does not exist a GAT \(\Sigma\) such that cwfs-containing-a-model-of-\(\Sigma\) must, themselves, be cartesian closed! Only term variables can appear in a context in a GAT.
Numerous references on MLTT in Martin-Löf dependent type theory on nLab. (nLab authors 2023b)
What’s different in MLTT
MLTT empowers us to make assertions such as \(A\to B\ \mathtt{context}\dashv A \ \mathtt{context}, B\ \mathtt{context}\), together with further rules stating that \(A\to B\) behaves like an internal hom.
Adding this rule to, say, the theory of categories means that in any such upgraded cwf containing a category object, we must have not only objects such as \(\mathop{\mathrm{Ob}}\) and \(\mathop{\mathrm{Ob}}.\mathop{\mathrm{Ob}}.\mathop{\mathrm{Hom}}\) but also objects like \(\mathop{\mathrm{Ob}}\to \mathop{\mathrm{Ob}}\).
Thus dependent type theory augmented with function types has models only in cwfs that are cartesian closed.
A fancier example
It is sort of possible (Bezem et al. 2021) to give a GAT whose models are locally cartesian closed categories (lcccs). First, define a GAT whose models are cwf objects in a cwf! Extend this GAT until you have one whose models are given by a choice of cwf equipped with a (cwf-containing-an-lccc-category)-object. 😱😱😱
Getting lcc cwfs
In the above example, the outermost cwf is still not forced to be lcc. For that, we need to be allowed to say things like \[\Pi(A)\ \mathtt{context}\dashv (A\ \mathtt{type}\dashv \Gamma).\]
GATs can give you internal models of fully powered dependent type theories, but only MLTT can assert that the whole world is such a model.
Conclusion
Syntactically, a GAT is written in the tiniest possible skeleton of a dependent type theory, with no type formers at all.
Therefore, the semantics of GATs is a small step on the road to the semantics of full Martin-Löf type theory, lying in plain categories with families, rather than cwfs decorated with identity, \(\Sigma\), function, or \(\Pi\)-types, or universes.
Even so, while a plain cwf doesn’t model full MLTT, it can model a model of MLTT!
GATs are the most fundamental organizational principle of Catlab.jl. There’s lots left to exploit there, and the implementation is just seeing a massive upgrade from Owen and Kris.
No release date scheduled yet for an implementation of a fully dependently typed language within Julia as a model of the GAT of models of MLTT. But stay tuned!
References
Extra: the connection with EATs
Cwfs decorated with
- \(\Sigma\)-types and
- Extensional identity types and which are
- democratic in the sense that every context is the extension of some type in the empty context
are the same thing as finitely complete categories. (Clairambault and Dybjer 2014)
Essentially algebraic theories (EATs) are the kinds of type theory that have models in finitely complete categories. So this equivalence reveals exactly the gap between EATs and GATs: only GATs can have models in cwfs that aren’t finitely complete. (To be sure, I have no natural examples of those that aren’t syntactic.)
Extra: the connection with \(\lambda\)-calculus and related categorical logic
There are flavors of cwfs whose categories are equivalent, similarly to the above, to Lawvere theories, cartesian closed categories, locally cartesian closed categories, and probably to \(C\)-monoids, a notion of model of untyped \(\lambda\)-calculus. (Castellan, Clairambault, and Dybjer 2020)