# Dependent type theory is a monad and an algebra

I recently uploaded a paper to the arXiv entitled Polynomial pseudomonads and dependent type theory, joint work with Steve Awodey. It is a rather technical paper—the goal of this post is to provide some intuition behind the ideas. I assume some familiarity with dependent type theory and category theory.

Our main result is that, in a suitable sense, dependent type theory is a monad and an algebra.

More specifically, given a dependent type theory $\mathbb{T}$, we can interpret $\mathbb{T}$ into a suitably structured category $\mathbb{C}$. Under this interpretation, each syntactic rule of $\mathbb{T}$ corresponds with a certain feature of $\mathbb{C}$. What we prove in the paper is that the rules for a unit type $\mathbb{1}$, dependent sum types $\sum_{x : A} B(x)$ and dependent product types $\prod_{x:A} B(x)$ together describe the structure of a polynomial (pseudo)monad which is, in a suitable sense, a (pseudo)algebra over itself.

Let’s see what this all means.

### Natural models

In this paper, Steve introduces the notion of a natural model, which is a category $\mathbb{C}$ equipped with a representable natural transformation $p : \dot{\mathcal{U}} \to \mathcal{U}$ between presheaves $\mathcal{U}, \dot{\mathcal{U}} : \mathbb{C}^{\mathrm{op}} \to \mathbf{Set}$.

We think of $\mathbb{C}$ as being the category whose objects are the contexts $\Gamma, \Delta, \dots$ of a type theory $\mathbb{T}$ and whose morphisms are the substitutions $\sigma : \Delta \to \Gamma$.

The presheaf $\mathcal{U}$ can be thought of as the presheaf of types-in-context. Thus an element $A \in \mathcal{U}(\Gamma)$ is a type $\Gamma \vdash A \text{ type}$. The action of $\mathcal{U}$ on morphisms provides the behaviour of types under substitutions: given a type $\Gamma \vdash A \text{ type}$ and a substitution $\sigma : \Delta \to \Gamma$, we obtain a type $\Delta \vdash A\sigma \text{ type}$.

The presheaf $\dot{\mathcal{U}}$ can be thought of as the presheaf of terms-in-context. Thus an element $a \in \mathcal{U}(\Gamma)$ is a term $\Gamma \vdash a : \dots$ wait, what’s the type of $a$? Well that’s what $p$ tells you: to say $\Gamma \vdash a : A$ is to say that $a \in \dot{\mathcal{U}}(\Gamma)$ and $p_{\Gamma}(a) = A \in \mathcal{U}(\Gamma)$.

Naturality of $p$ tells us that subtitutions on terms match up with substitutions on types, namely if $\sigma : \Delta \to \Gamma$ and $\Gamma \vdash a : A$, then $\Delta \vdash a\sigma : A\sigma$.

Representability of $p$ tells us that we can extend a context by any type in that context: given $\Gamma \vdash A \text{ type}$, there is an extended context $\Gamma.A$, together with a projection $\mathsf{p}_A : \Gamma.A \to A$ and a term $\mathsf{q}_A \in \dot{\mathcal{U}}(\Gamma.A)$.

If you know the definition of a category with families, this may look familiar: that’s because the two notions are equivalent!

### Polynomials

In any locally cartesian closed category $\mathcal{E}$, we can regard a morphism $f : B \to A$ as a polynomial, which induces a polynomial functor $P_f : \mathcal{E} \to \mathcal{E}$ defined by $$P_f(X) = \sum_{a : A} X^{B_a}$$

The map $p : \dot{\mathcal{U}} \to \mathcal{U}$ lives in the presheaf category $\mathcal{E} = [\mathbb{C}^{\mathrm{op}}, \mathbf{Set}]$, which is locally cartesian closed; regarding $p$ as a polynomial, we obtain a polynomial functor $P=P_p : \mathcal{E} \to \mathcal{E}$ as before.

The polynomial functor $P$ turns out to be useful for describing the features of the natural model $(\mathbb{C},p)$ corresponding with syntactic rules of a dependent type theory $\mathbb{T}$. For example, the object $P(\mathcal{U})$ is described in the internal language of $\mathcal{E}$ by $\sum_{A:\mathcal{U}} \mathcal{U}^{[A]}$, where I’m writing $[A]=\dot{\mathcal{U}}_A$ for readability. Internally, the elements of $P(\mathcal{U})$ are pairs $\langle A,B \rangle$, where $A$ is a type and $B : A \to \mathcal{U}$ is a dependent type over $A$. Thus morphisms $P(\mathcal{U}) \to \mathcal{U}$ correspond with formation rules in type theory of the form $$\cfrac{\Gamma \vdash A \text{ type} \qquad \Gamma, x:A \vdash B(x) \text{ type}}{\Gamma \vdash C(A,B) \text{ type}}$$

### A monad and an algebra (kind of)

In Steve’s paper on natural models, he describes the conditions on a natural model $(\mathbb{C}, p)$ which correspond with the syntactic rules for a unit type $\mathbf{1}$, dependent sum types $\sum_{x:A} B(x)$ and dependent product types $\prod_{x:A} B(x)$.

In each case, the condition on the natural model is simply the existence of a pullback square. These conditions can be translated into the language of polynomial functors in the following way:

• The rules for a unit type correspond with the existence of a cartesian, strong natural transformation $\eta : 1 \Rightarrow P$;
• The rules for dependent sum types correspond with the existence of a cartesian, strong natural transformation $\mu : P \circ P \Rightarrow P$;
• The rules for dependent product types correspond with the existence of a cartesian morphism of polynomials $\zeta : P(p) \Rightarrow p$.

Having made this observation, any self-respecting category theorist would ask the following questions:

• Is $(P,\eta,\mu)$ a monad?
• Is $(p,\zeta)$ an algebra for this monad in any sense?

The answer to each question is… almost.

Remember, everything we do in the natural model reflects some kind of syntactic rule of the type theory. As such, the monad and algebra laws should mean something in the syntax. The following table shows the translation from the monad and algebra laws to the syntax at the level of types:

 Monad laws Type theory Associativity $\sum\limits_{\langle x,y \rangle \sum\limits_{x:A}B(x)} C(x,y) = \sum\limits_{x:A} \sum\limits_{y:B(x)} C(x,y)$ Left unit $\mathbf{1} \times A = A$ Right unit $A \times \mathbf{1} = A$ Algebra laws Type theory Associativity $\prod\limits_{\langle x,y \rangle \sum\limits_{x:A}B(x)} C(x,y) = \prod\limits_{x:A} \prod\limits_{y:B(x)} C(x,y)$ Unit $A^{\mathbf{1}} = A$

The rules in the column on the right do not hold strictly in general. Rather, they hold up to canonical isomorphism. Thus at best we may hope for $(P,\eta,\mu)$ to be a pseudomonad and for $(p,\zeta)$ to be a pseudoalgebra over this pseudomonad.

What we do in our paper is to define the appropriate notion of equivalence, called adjustment, to state what it means to be a pseudomonad and pseudoalgebra in this sense. With this done, we prove that this is indeed what we have. I will not go into the details in this post, since that would amount to repeating what you can already read in the paper!

### Conclusion

Our result elucidates a structure in type theory that, to our knowledge, has not been noticed before. In part this is because what was needed was the right point of view: in this case, what was needed was to use natural models to view dependent type theory through the lens of polynomial functors.

The result is also an interesting and perhaps unexpected connection between logic and abstract algebra, which raises the question of what other connections there may be out there!