Polynomial universes and natural models
polynomial functors
type theory
Abstract
In this post, I summarize the work I conducted over the summer of 2024 at the Topos Institute, together with David Spivak, wherein we have aimed to extend, refine, and generalize the treatment of models of type theory in terms of polynomial functors via the concept of polynomial universes. We shall see how the language of polynomial functors can be used to elegantly capture all of the usual constructs of dependent type theory, and moreover, how interpreting this language in homotopy type theory reveals striking properties of these structures.
Dependent types are ubiquitous in mathematics, pure and applied. When we say “let v be a vector of length n,” we make the collection of values to which v may belong dependent upon the value of n. Such dependency of types-of-things on values-of-things is fundamental to our ability to express complex mathematical ideas and build up sophisticated abstractions. By taking this essential idea to heart, dependent type theory provides all of the following:
An elegant syntax for expressing mathematical ideas.
Computational interpretations that allow automation and formal verification of mathematical proofs.
A robust categorical semantics that allow type theoretic syntax to be used in order to work in the internal languages of well-structured categories, and even more exotic structures, such as \infty-categories.
Of these, it is the categorical semantics of dependent type theory that shall be the focus of this blog post. Specifically, although these categorical semantics are evidently quite powerful, they are also notoriously subtle and difficult to get right, owing mainly to the issue of strictness. As we shall see, one often needs to strictify various identities that typically hold only up to isomorphism in arbitrary categories, but that must hold strictly in order for such a category to soundly model the type-theoretic syntax.
Perhaps surprisingly – or unsurprisingly to regular readers of this blog – a key device in resolving this difficulty turns out to be the categorical machinery of polynomial functors. Awodey – and later Newstead – have shown that there is a strong connection between dependent type theory and polynomial functors, via their concept of natural models, which cleanly solves the strictification problem for the categorical semantics of dependent type theory. In particular, the solution to this problem offered by Awodey and Newstead makes use of the type-theoretic concept of a universe. Such universes turn out to naturally be regarded as polynomial functors on a suitably-chosen category of presheaves.
In this post, I will summarize the work I conducted over the summer at Topos, together with David Spivak, wherein we have aimed to extend, refine, and generalize this treatment of models of type theory by studying properties of such polynomial universes. We shall see how the language of polynomial functors can be used to elegantly capture all of the usual constructs of dependent type theory, and moreover, how interpreting this language in homotopy type theory reveals striking properties of these structures.
1 Recap of dependent type theory and natural models
In Martin-Löf Type Theory (MLTT) we have the primitive judgments:
\Gamma ~ \mathsf{Ctx} \qquad \Gamma \vdash A ~ \mathsf{Type} \qquad \Gamma \vdash a : A \qquad \Gamma \vdash a_0 \equiv a_1 : A which are then subject to the following rules:\frac{~}{\epsilon ~ \mathsf{Ctx}} \qquad \frac{\Gamma ~ \mathsf{Ctx}\qquad \Gamma \vdash A ~ \mathsf{Type}}{\Gamma, x : A ~ \mathsf{Ctx}} \frac{~}{\Gamma \vdash 1 ~ \mathsf{Type}} \qquad \frac{~}{\Gamma \vdash () : 1} \qquad \frac{\Gamma \vdash u : 1}{\Gamma \vdash u = () : 1} \frac{\Gamma \vdash A ~ \mathsf{Type}\qquad \Gamma, x : A \vdash B ~ \mathsf{Type}}{\Gamma \vdash \Sigma x : A . B ~ \mathsf{Type}} \qquad \frac{\Gamma \vdash a : A \qquad \Gamma \vdash b : B[a/x]}{\Gamma \vdash (a,b) : \Sigma x : A . B} \frac{\Gamma \vdash p : \Sigma x : A . B}{\Gamma \vdash \pi_1(p) : A} \qquad \frac{\Gamma \vdash p : \Sigma x : A . B}{\Gamma \vdash \pi_2(p) : B[\pi_1(p)/x]} \frac{\Gamma \vdash a : A\qquad \Gamma \vdash b : B[a/x]}{\Gamma \vdash \pi_1(a,b) \equiv a : A} \qquad \frac{\Gamma \vdash a : A\qquad \Gamma \vdash b : B[a/x]}{\Gamma \vdash \pi_2(p) \equiv b : B[a/x]} \frac{\Gamma \vdash p \in \Sigma x : A . B}{\Gamma \vdash p \equiv (\pi_1(p), \pi_2(p)) : \Sigma x : A . B} \frac{\Gamma \vdash A ~ \mathsf{Type}\qquad \Gamma, x : A \vdash B ~ \mathsf{Type}}{\Gamma \vdash \Pi x : A . B ~ \mathsf{Type}} \qquad \frac{\Gamma, x : A \vdash f : B}{\Gamma \vdash \lambda x . f : \Pi x : A . B} \frac{\Gamma \vdash f : \Pi x : A . B\qquad \Gamma \vdash a : A}{\Gamma \vdash f(a) : B[a/x]} \qquad \frac{\Gamma \vdash f : \Pi x : A . B\qquad \gamma \vdash a : A}{\Gamma \vdash (\lambda x . f)(a) \equiv f[a/x] : B[a/x]} \frac{\Gamma \vdash f \in \Pi x : A . B}{\Gamma \vdash f \equiv \lambda x . f(x) : \Pi x : A . B} where the operation of substitution is defined as follows: \begin{array}{rcl} 1[a/x] & = & 1\\ ()[a/x] & = & ()\\ (\Sigma y : A . B)[a/x] & = & \Sigma y : A[a/x] . B[a/x]\\ (b,c)[a/x] & = & (b[a/x], c[a/x])\\ \pi_1(p)[a/x] & = & \pi_1(p[a/x])\\ \pi_2(p)[a/x] & = & \pi_2(p[a/x])\\ (\Pi y : A . B)[a/x] & = & \Pi y : A[a/x] . B[a/x]\\ (\lambda y . f)[a/x] & = & \lambda y . f[a/x]\\ f(b)[a/x] & = & f[a/x](b[a/x]) \end{array}
Although contexts may seem rather trivial from a syntactic perspective, they are key to understanding the categorical semantics of dependent type theory. In particular, when modeling a dependent type theory as a category, it is the contexts which form the objects of this category, with morphisms between contexts being substitutions of terms in the domain context for the variables of the codomain context. A type A dependent upon variables in a context \Gamma is then interpreted as a morphism (i.e. substitution) \Gamma, x : A \to \Gamma, called a display map, whose domain represents the context \Gamma extended with a variable of type A. We then interpret a term a of type A in context \Gamma as a section of the display map representing A, i.e.
Hence for each context \Gamma, there is a category \mathbf{Ty}[\Gamma], which is the full subcategory of the slice category \mathcal{C}/\Gamma consisting of all display maps, wherein objects correspond to types in context \Gamma, and morphisms correspond to terms.
In typical categorical semantics, given a substitution f : \Gamma \to \Delta, and a display map A : \Delta, x : A \to \Delta, we then interpret the action of applying the substitution f to A as a pullback:
In particular, then, any display map A : \Gamma, x : A \to \Gamma induces a functor \mathbf{Ty}[\Gamma] \to \mathbf{Ty}[\Gamma, x : A] by substitution along A, which corresponds to weakening a context by adding a variable of type A. The left and right adjoints to the weakening functor (if they exist) then correspond to \Sigma and \Pi types, respectively.
In order for the operation of forming \Sigma and \Pi types to be stable under substitution (i.e. pullback), these must additionally satisfy the Beck-Chevalley condition:
So far, we have told a pleasingly straightforward story of how to interpret the syntax of dependent type theory categorically. Unfortunately, this story is a fantasy, and the interpretation of type-theoretic syntax into categorical semantics sketched above is unsound, as it stands. The problem in essentials is that, in the syntax of type theory, substitution is strictly associative, and strictly satisfies the Beck-Chevalley condition. However, in the above categorical semantics, substitution by pullback, which is in general only associative up to isomorphism, and likewise for the Beck-Chevalley condition. It is precisely this problem which natural models exist to solve.
As mentioned previously, the key insight in formulating the notion of a natural model is that the problem of strictness in the semantics of type theory has, in a sense, already been solved by the notion of type universes. A universe is a type \mathcal{U} whose elements can themselves be regarded as types, as follows: \frac{~}{\Gamma \vdash \mathcal{U} ~ \mathsf{Type}} \qquad \frac{\Gamma \vdash A : \mathcal{U}}{\Gamma \vdash \mathcal{U}_\bullet(A) ~ \mathsf{Type}} In categorical semantics, we interpret such a universe as a display map u : \mathcal{U}_\bullet \to \mathcal{U}. A type in context \Gamma may then be instead represented as a morphism A : \Gamma \to \mathcal{U}, whereby we obtain the corresponding display map for A as the pullback:
Conversely, we say that a display map \Gamma, x : A \to \Gamma is classified by \mathcal{U} if there are morphisms forming a pullback square as above.
Hence given a universe of types \mathcal{U}, rather than representing substitution as pullback, we can simply represent the action of applying a substitution f : \Gamma \to \Delta to a family of types A : \Delta \to \mathcal{U} as the precomposition A \circ f : \Gamma \to \mathcal{U}, which is automatically strictly associative, and strictly satisfies the Beck-Chevalley condition for \Sigma types/\Pi types if \mathcal{U} is suitably closed under \Sigma types / \Pi types, respectively.
To interpret the syntax of dependent type theory in a category \mathcal{C} of contexts and substitutions, it therefore suffices to embed \mathcal{C} into a category whose type-theoretic internal language possesses such a universe whose types correspond to those of \mathcal{C}. And what better embedding of a category \mathcal{C} into a larger category with a well-understood type-theoretic language than the Yoneda embedding \mathbf{y} : \mathcal{C} \to \mathbf{Set}^{\mathcal{C}^{op}}?
Hence we can work in the category of presheaves \mathbf{Set}^{\mathcal{C}^{op}}, whose type-theoretic internal language is already well-understood, to study that of \mathcal{C}. The universe \mathcal{U} is then given by:
an object of \mathbf{Set}^{\mathcal{C}^{op}}, i.e. a contravariant functorial assignment, to each context \Gamma, of a set \mathcal{U}(\Gamma) of types in context \Gamma, together with
an object u \in \mathbf{Set}^{\mathcal{C}^{op}}/\mathcal{U}, i.e. a natural transformation u : \mathcal{U}_\bullet \to \mathcal{U}, where for each context \Gamma, \mathcal{U}_\bullet(\Gamma) is the set of terms in context \Gamma, and u_\Gamma : \mathcal{U}_\bullet(\Gamma) \to \mathcal{U}(\Gamma) assigns each term to its type.
The condition that all types in \mathcal{U} “belong to \mathcal{C}” can then be expressed by requiring u to be representable in the following sense: for any representable \gamma \in \mathbf{Set}^{\mathcal{C}^{op}} with \alpha : \gamma \to \mathcal{U}, the pullback
is representable. In particular, this says that, given a context \Gamma and a type A \in \mathcal{U}[\Gamma], there is a context \Gamma, A together with a substitution \Gamma, A \to A that corresponds to the above pullback under the Yoneda embedding. Type-theoretically, this corresponds to the operation of context extension.
The question, then, is how to express that \mathcal{C} has \Sigma types, \Pi types, etc., in terms of the structure of u. Toward answering this question, we may note that u gives rise to an endofunctor (indeed, a polynomial endofunctor) P_u : \mathbf{Set}^{\mathcal{C}^{op}} \to \mathbf{Set}^{\mathcal{C}^{op}}, defined by X \mapsto \sum_{A : \mathcal{U}} X^{\mathcal{U}_\bullet[A]} (This notation will be made precise momentarily). As it turns out, much of the type-theoretic structure of u (and by extension \mathcal{C}) can be accounted for in terms of this functor. For instance, u is closed under unit and \Sigma types if and only if \overline{u} carries the structure of a Cartesian pseudomonad on \mathbf{Set}^{\mathcal{C}^{op}}. To see why this is the case, and to expand this account to other type-formers, such as \Pi types, we will need the theory of polynomial functors on a Locally Cartesian Closed category.
2 Polynomial arithmetic and dependent types
2.1 Polynomial functors
Recall that a category \mathcal{C} is Locally Cartesian Closed (LCC) if \mathcal{C}, and all slices of \mathcal{C} are Cartesian closed.
In particular, if \mathcal{C} is Locally Cartesian Closed, then \mathcal{C} has all pullbacks, and the pullback functors f^* : \mathcal{C}/A \to \mathcal{C}/B for any f : B \to A have both left and right adjoints \Sigma_f and \Pi_f. Hence (up to strictness issues) every LCCC has a form of Martin-Löf Type Theory as its internal type-theoretic language. In what follows, it will therefore be productive to consider polynomial functors and related constructions both as structures on an LCCC \mathcal{C}, and as structures in the internal type-theoretic language of \mathcal{C}.
Given any morphism f : B \to A \in \mathcal{C}, we may define the corresponding polynomial endofunctor P_f as the composite \mathcal{C} \simeq \mathcal{C}/1 \xrightarrow{!^*_B} \mathcal{C}/B \xrightarrow{\Pi_f} \mathcal{C}/A \xrightarrow{\Sigma_{!_A}} \mathcal{C}/1 \simeq \mathcal{C} Type-theoretically, we think of f : B \to A as an A-indexed family B[a] for all a : A. Then, in the internal language of \mathcal{C}, P_f maps a type y to the type \Sigma x : A . y^{B[x]}
In general, polynomial functors P_f can be characterized by the following universal property:
Proof. \begin{array}{rl} & Hom_\mathcal{C}(C,P_f(D))\\ = & Hom_\mathcal{C}(C, \Sigma_{!_A} \Pi_f (!_B^*(D)))\\ \cong & \sum_{g : C \to A} Hom_{\mathcal{C}/A}(g,\Pi_f(!_B^*(D)))\\ \cong & \sum_{g : C \to A} Hom_{\mathcal{C}/B}(f^*(g), !_B^*(D))\\ \cong & \sum_{g : C \to A} (B[g] \to D) \end{array}
In particular, we obtain natural transformations p^f : P_f(-) \Rightarrow A \quad \text{and} \quad \mathsf{app}^f : B[p^f_{(-)}] \Rightarrow \text{Id}(-) by plugging in \text{id}_{P_f(X)} on the right hand side for each X \in \mathcal{C}, yielding following diagram:
2.1.1 Morphisms of polynomial functors
For f : B \to A and g : D \to C, a diagram as below
induces a natural transformation \phi : P_f \Rightarrow P_g whose components \phi_X : P_f(X) \to P_g(X) are derived by the above equivalence from the following data
One may then wonder: are all natural transformations P_f \Rightarrow P_g induced in this way? Gambino & Kock (2009) answer this question in the affirmative for strength-preserving natural transformations, where polynomial functors are canonically regarded as strong functors in a particular way.
Hence for any locally cartesian closed category \mathcal{C}, we have a category \mathbf{Poly}_\mathcal{C} whose objects are families f : B \to A \in \mathcal{C}, regarded as polynomial functors, and whose morphisms are diagrams as above, regarded as (strength-preserving) natural transformations.
Cartesian morphisms of polynomial endofunctors. A morphism of polynomial functors \phi : P_f \Rightarrow P_g as above is called cartesian if \phi^\sharp is an isomorphism. Equivalently, a Cartesian morphism P_f \Rightarrow P_g consists of a pullback square
Hence there is a wide subcategory \mathbf{Poly_\mathcal{C}^{Cart}} \hookrightarrow \mathbf{Poly}_\mathcal{C} consisting of polynomial functors and Cartesian morphisms between them.
Type theoretically, thinking of f and g as families of types, the existence of a Cartesian morphism \phi : P_f \Rightarrow P_g essentially shows that, for each a : A there is an element \phi_1(a) : C such that B[a] \simeq D[\phi_1(a)], i.e. every type in the family B[a] corresponds to a type in the family D[c]. So in particular, a Cartesian morphism in \mathbf{Set}^{\mathcal{C}^{op}} from a family f : B \to A into a representable family u : \mathcal{U}_\bullet \to \mathcal{U} suffices to show that types in the internal language of \mathcal{C} are closed under those types encoded by f. Hence to show that \mathcal{C} is closed under \Sigma types, \Pi types, etc., we need only find polynomial functors that suitably represent these types, and ask that there be Cartesian morphisms from these polynomials to u.
2.2 Composition of polynomials and \Sigma types
Proof. By the universal property of polynomial functors, to show that P_f \circ P_g — for f : B \to A and g : D \to C — is polynomial, it suffices to find f \triangleleft g : F \to E such that \begin{array}{rl} & \sum_{k : X \to E} \left( F[k] \to Y \right)\\ \cong & Hom(X,P_{f \triangleleft g}(Y))\\ \cong & Hom(X, P_f(P_g(Y)))\\ \cong & \sum_{k : X \to A} \left( B[k] \to P_g(Y) \right)\\ \cong & \sum_{k : X \to A} \sum_{k' : B \times_{f,k} X \to C} \left( D[k'] \to Y \right)\\ \cong & \sum_{k : X \to A, ~ k' : B \times_{f,k} X \to C} (D[k'] \to Y)\\ \cong & \sum_{k : X \to P_f(C)} \left((\Sigma_{B[p_C^f]}D[\mathsf{app}^f_C])[k] \to Y \right) \end{array} Hence we can satisfy this by taking f \triangleleft g to be the following
It follows that the composition defines a monoidal product on \mathbf{Poly}_\mathcal{C}, whose unit is the identity functor, represented by the identity morphism \text{id}_1 : 1 \to 1 on the terminal object 1.
Type-theoretically, given an A-indexed family of types B[a] for all a : A and a C-indexed family of types D[c] for all c : C, the family representing the composition of B and D, thought of as polynomial functors, is the \Sigma x : A . C^{B[x]}-indexed family that maps a pair (a, f) : \Sigma x : A . C^{B[x]} to the type \Sigma y : B[a] . D[f(y)] From this follows straightforwardly the universal property of f \triangleleft g as an object of \mathbf{Poly}_\mathcal{C}: Hom_{\mathbf{Poly}_\mathcal{C}}(f \triangleleft g, h) \cong \sum_{\phi_1 : P_f(C) \to E} Hom_{\mathcal{C}/P_f(C)}(F[\phi_1], \Sigma_{B[p_C^f]} D[\mathsf{app}^f_C]) and moreover as an object of \mathbf{Poly_\mathcal{C}^{Cart}}: Hom_{\mathbf{Poly_\mathcal{C}^{Cart}}}(f \triangleleft g , h) \cong \sum_{\phi_1 : P_f(C) \to E} \left( F[\phi_1] \cong_{\mathcal{C}/P_f(C)} \Sigma_{B[p^f_C]} D[\mathsf{app}^f_C] \right) So in particular, if we take \mathcal{C} to be \mathbf{Set}^{\mathcal{C}^{op}} and f = g = h = u, we have that a Cartesian morphism P_{u \triangleleft u} \Rightarrow P_u consists of:
A natural transformation \sigma : \left( \sum_{A : \mathcal{U}} \mathcal{U}^{\mathcal{U}_\bullet[A]} \right) \to \mathcal{U} which assigns to each pair A, B consisting of a type A : \mathcal{U} and a family of types B[a] : \mathcal{U} for all a : \mathcal{U}_\bullet[A], a type \sigma(A,B) : \mathcal{U} representing the dependent pair type.
For each (A,B) : \sum_{A : \mathcal{U}} \mathcal{U}^{\mathcal{U}_\bullet[A]}, a natural transformation \psi_{A,B} : \mathcal{U}_\bullet[\sigma(A,B)] \to \sum_{a : \mathcal{U}_\bullet[A]} \mathcal{U}_\bullet[B[a]] which maps an element p : \mathcal{U}_\bullet(\sigma(A,B)) to elements \pi_1(p) : \mathcal{U}_\bullet[A] and \pi_2(p) : \mathcal{U}_\bullet[B[\pi_1(p)]], corresponding to the first and second projections out of p, respectively.
For each A,B as above, a natural transformation \psi_{A,B}^{-1} : \left( \sum_{a : \mathcal{U}_\bullet[A]} \mathcal{U}_\bullet[B[a]] \right) \to \mathcal{U}_\bullet[\sigma(A,B)] which maps a pair consisting of a : \mathcal{U}_\bullet[A] and b : \mathcal{U}_\bullet[B[a]] to an element \langle a , b \rangle : \mathcal{U}_\bullet[\sigma(A,B)], corresponding to the pairing of a and b.
Such that \psi_{A,B} and \psi^{-1}_{A,B} are mutually inverse.
By inspection, we see that these data correspond precisely to the rules for the \Sigma type in Martin-Löf type theory. Similarly, u classifies the unit type iff there is a Cartesian morphism \text{Id}_\mathcal{C} \simeq P_{\text{id}_1} \Rightarrow P_u. Hence an object u \in \mathbf{Poly}, thought of as a universe of types, is closed under unit and \Sigma types iff there are morphisms \text{id}_1 \to u \qquad u \triangleleft u \to u in \mathbf{Poly^{Cart}}. One might notice, at this point, that these morphisms look suspiciously like the unit and multiplication maps of a monad. Whether or not these operations do in fact define a monad will be our topic for the final section of this post. For now, let us turn our attention to \Pi types.
2.3 The \upuparrows functor and \Pi types
We now wish to define an operation on polynomial functors that type-theoretically corresponds to the formation of \Pi-types. I.e., in type-theoretic notation, given an A-indexed family B[a] for all a : A and a C-indexed family D[c] for all c : C – represented by the polynomial functors P_f and P_g for f : B \to A and g : B \to C – we want to find a polynomial functor P_{f \upuparrows g} for some f \upuparrows g : F \to E that corresponds to the \Sigma x : A . C^{B[x]}-indexed family that maps (a,f) : \Sigma x : A . C^{B[x]} to the type \Pi y : B[a] . D[f(y)] By analogy with the definition of composition in terms of \Sigma (i.e. f \triangleleft g = \Sigma_{B[p^f_C]} D[\mathsf{app}^f_C] \in \mathcal{C}/P_f(C)), this should be f \upuparrows g = \Pi_{B[p^f_C]} D[\mathsf{app}^f_C] \in \mathcal{C}/P_f(C) Unlike f \triangleleft g, however, this definition does not straightforwardly define a functor {\upuparrows} : \mathbf{Poly} \times \mathbf{Poly} \to \mathbf{Poly}. The problem is essentially due to the contravariance of \Pi in its first argument. If we try to define in type-theoretic notation a functorial action of \upuparrows in its first argument, we face the following problem, given:
An A-indexed family B[a] for all a : A
An A'-indexed family B'[a'] for all a' : A'
A C-indexed family D[c] for all c : C
A function \phi_1 : A \to A'
A function \phi^\sharp : (x : A) \to B'[\phi_1(x)] \to B[x]
define a function (\phi \upuparrows D)^\sharp : (a : A, ~ f : C^{B[a]}) \to (\Pi b' : B'[\phi_1(a)] . D[f(\phi^\sharp(a,b'))]) \to \Pi b : B[a] . D[f(b)]. And this is not generally possible, since given b : B[a] and g : \Pi b' : B'[\phi_1(a)] . D[f(\phi^\sharp(a,b'))], we have no given way of obtaining a value b' : B'[\phi_1(a)] from b to supply as input to g.
It is possible, however, if we additionally assume that \phi^\sharp(a,-) is invertible for all a : A, i.e. \phi is Cartesian. Then we can define (\phi \upuparrows D)^\sharp(a,f) = \lambda g . \lambda b . g({\phi^\sharp}^{-1}(a,b)) Hence we can view \upuparrows as a functor \mathbf{Poly^{Cart}} \times \mathbf{Poly} \to \mathbf{Poly}.
We can in fact define a more compact representation of f \upuparrows g, due to the following theorem:
Proof. Hom_{\mathcal{C}/P_f(C)}(h, P_f(g)) is isomorphic to those k_1:F\to A, k^\sharp:B[k_1]\to D such that
which is isomorphic to \begin{array}{rl} & Hom_{\mathcal{C}/C}(\Sigma_{\mathsf{app}_C^f}(B[p_C^f][h]), g)\\ \cong & Hom_{\mathcal{C}/B[p^f_C]}(B[p^f_C][h], D[\mathsf{app}^f_C])\\ \cong & Hom_{\mathcal{C}/P_f(C)}(h, \Pi_{B[p^f_C]}(D[\mathsf{app}^f_C])) \end{array}
Using this, we can further characterize \upuparrows as follows:
Definition.
A (left-)action of a monoidal category (\mathcal{M}, \otimes, I) on a category \mathcal{C} is a functor \odot : \mathcal{M} \times \mathcal{C} \to \mathcal{C} together with natural isomorphisms:
\eta_A : I \odot A \cong A
\mu : (M \otimes N) \odot A \cong M \odot (N \odot A)
such that the triangles
and the pentagon
formed from these and the associator and unitors of \mathcal{M} all commute.
Proof. (Sketch) Since f \upuparrows g \cong P_f(g) we have
\text{id}_1 \upuparrows g \cong P_{\text{id}_1}(g) \cong g
(f \triangleleft g) \upuparrows h \cong P_{f \triangleleft g}(h) \cong P_f(P_g(h)) \cong f \upuparrows (g \upuparrows h)
and it is straightforward to verify that these satisfy the pentagon and triangle identities.
Finally, to see that \upuparrows has the desired property of classifying \Pi types on natural models, we first note that the definition of f \upuparrows g as \Pi_{B[p^f_C]} D[\mathsf{app}^f_C] straightforwardly yields the following universal property of f \upuparrows g as an object of \mathbf{Poly}: Hom_{\mathbf{Poly}_\mathcal{C}}(f \upuparrows g, h) \cong \sum_{\phi_1 : P_f(C) \to E} Hom_{\mathcal{C}/P_f(C)}(F[\phi_1], \Pi_{B[p_C^f]} D[\mathsf{app}^f_C]) and moreover as an object of \mathbf{Poly_\mathcal{C}^{Cart}}: Hom_{\mathbf{Poly_\mathcal{C}^{Cart}}}(f \upuparrows g , h) \cong \sum_{\phi_1 : P_f(C) \to E} \left( F[\phi_1] \cong_{\mathcal{C}/P_f(C)} \Pi_{B[p^f_C]} D[\mathsf{app}^f_C] \right) Then as before, working over \mathbf{Set}^{\mathcal{C}^{op}} with f = g = h = u, a Cartesian morphism P_{u \upuparrows u} \Rightarrow P_u consists of:
A natural transformation \pi : \left( \sum_{A : \mathcal{U}} \mathcal{U}^{\mathcal{U}_\bullet[A]} \right) \to \mathcal{U} which assigns to each pair (A,B) consisting of a type A : \mathcal{U} and a family of types B[a] : \mathcal{U} for each a : \mathcal{U}_\bullet[A], a type \pi(A,B) : \mathcal{U}, corresponding to the \Pi type of A and B.
For each pair A,B as above, a natural transformation \alpha_{A,B} : \mathcal{U}_\bullet[\pi(A,B)] \to \prod_{a : \mathcal{U}_\bullet[A]} \mathcal{U}_\bullet[B[a]] which, given f : \mathcal{U}_\bullet[\pi(A,B)] and a : \mathcal{U}_\bullet[A], produces \alpha(f)(a) : \mathcal{U}_\bullet[B[a]] corresponding to the result of applying f to a.
For each pair A,B as above, a natural transformation \lambda_{A,B} : \left( \prod_{a : \mathcal{U}_\bullet[A]} \mathcal{U}_\bullet[B[a]] \right) \to \mathcal{U}_\bullet[\pi(A,B)] which maps a function f : \prod_{a : \mathcal{U}_\bullet[A]} \mathcal{U}_\bullet[B[a]] to a term \lambda(f) : \mathcal{U}_\bullet[\pi(A,B)] representing the \lambda-abstraction of f,
Such that \alpha_{A,B} and \lambda_{A,B} are mutually inverse.
Once again, by inspection we see that these data correspond precisely with the rules for \Pi types in Martin-Löf type theory. Hence we can compactly represent a natural model of MLTT as a representable natural transformation u : \mathcal{U}_\bullet \to \mathcal{U} equipped with morphisms \mathsf{id}_1 \to u \quad u \triangleleft u \to u \quad u \upuparrows u \to u in \mathbf{Poly^{Cart}}. But what sort of structure do these morphisms define on u? Perhaps surprisingly, answering this question satisfactorily requires us to leave the 1-dimensional universe of set theory, and instead reformulate the notion of polynomial universes we have developed in the context of Homotopy Type Theory (HoTT).
3 Polynomial universes in HoTT
In order to understand the higher-dimensional identities and coherences of type formers in natural models, we now change our setting from the extensional internal language of \mathbf{Set}^{\mathcal{C}^{op}} to the intensional internal language of \mathbf{\infty Grpd}^{\mathcal{C}^{op}}, which is a form of HoTT. All the constructions on polynomial functors we considered previously carry over to this setting – mutatis mutandis – by replacing the term “category” with “\infty-category”, etc. Hence we now have \infty-categories \mathbf{Poly} and \mathbf{Poly}^{\mathbf{Cart}}, defined essentially the same as before.
For any polynomial u, we say that u is univalent if it is a subterminal object in \mathbf{Poly^{Cart}}, i.e. for any other polynomial p, the (homotopy) type of Cartesian morphisms p \to u is a mere proposition in HoTT, i.e. it has at most one inhabitant, up to homotopy.
We call this property of polynomials univalence by analogy with the usual univalence axiom. Indeed, the statement that an LCC \infty-Category has enough univalent universes is equivalent to the existence of a terminal family in \mathbf{Poly^{Cart}}, i.e. a set of subterminal objects u_i \in \mathbf{Poly^{Cart}} such that every p \in \mathbf{Poly^{Cart}} has a Cartesian morphism to some u_i.
If u is univalent and has (e.g.) Cartesian morphisms \eta : \text{id}_1 \to u and \mu : u \triangleleft u \to u exhibiting that u is closed under unit and \Sigma-types, then the following diagrams necessarily commute (up to homotopy)
One may recognize these as the usual diagrams for a monoid in a monoidal category, hence (since \triangleleft corresponds to composition of polynomial endofunctors) for a monad as typically defined. Moreover, since the types of Cartesian morphisms into u are contractible, any higher-dimensional diagram one may draw with these also commutes, ensuring that u additionally satisfies all the coherences of an \infty-monad.
For \Pi-types, the situation is somewhat more complex. What David and I established in our work together is that closure of u under \Pi-types (in addition to unit and \Sigma types) corresponds to a special kind of distributive law of the above monad over itself.
The notion of a distributive law of one monad over another can be viewed as an answer to the question “when is the composition of two monads also a monad?” Given monads m,n (we may assume, for present purposes, that m,n are polynomial) with unit \eta_m : \mathsf{id}_1 \to m and \eta_n : \mathsf{id}_1 \to n and multiplication \mu_m : m \triangleleft m \to m and \mu_n : n \triangleleft n \to n, we can straightforwardly define a putative unit for m \triangleleft n as the composite \mathsf{id}_1 \simeq \mathsf{id}_1 \triangleleft \mathsf{id}_1 \xrightarrow{\eta_m \triangleleft \eta_n} m \triangleleft n However, when we attempt to define a multiplication (m \triangleleft n) \triangleleft (m \triangleleft n), we have no direct way to apply \mu_m or \mu_n, since neither of the two occurrences of m and n in the domain occur next to each other. This difficulty could be resolved if we had an additional map \delta : n \triangleleft m \to m \triangleleft n Then indeed, if one reverse-engineers what equations such a map \delta must satisfy in order for m \triangleleft n to be a monad with the resulting unit and multiplication, this gives rise to the definition of a distributive law. The (1-dimensional) diagrams required to commute in order for \delta to be a distributive law are then as follows:
Note that, in the case where m = n = u, the morphisms identified by these diagrams are not morphisms into u (nor are they generally Cartesian), so we cannot immediately apply univalence to these as we did for the monad laws.
The solution is to define a class of morphisms \delta as above that correspond to Cartesian morphisms into u.
Definition.
A jump-structure on a morphism in \phi : f \triangleleft g \to h \triangleleft f in \mathbf{Poly}, given by \phi_1 : P_f(C) \to P_h(A) and \phi^\sharp : (\Sigma_{F[p^h_A]} B[\mathsf{app}^h_A])[\phi_1] \to \Sigma_{B[p^f_C]} D[\mathsf{app^f_C}], consists of paths making the following diagrams commute
essentially, these state that the action of \phi on its p-components is the identity. This sort of structure was previously considered by David in his blog post on “jump monads”, whence the name.
We then leverage the following theorem:
We say that a jump structure is Cartesian if its corresponding morphism f \upuparrows g \to h is Cartesian. The proof that a morphism u \triangleleft u \to u \triangleleft u equipped with a Cartesian jump structure automatically satisfies the laws of a (\infty-)distributive law then works essentially by showing that Cartesian jump structures are closed under all of the constructions appearing in the diagrams for a distributive law (though note that the definitions/theorems in our paper are a bit more general than what is presented above, in order to accommodate all of the constructions appearing in these diagrams).
Hence, just as a univalent polynomial is closed under \Sigma and unit types if and only if it possesses the structure of a Cartesian \infty-monad, so too is it closed under \Pi types if and only if this \infty-monad additionally possesses a distributive law over itself which carries a Cartesian jump structure.
3.1 Examples of polynomial universes
For a univalent universe \mathcal{U}, the corresponding polynomial functor looks like X \mapsto \sum_{A : \mathcal{U}} X^A If we specialize this to the case where \mathcal{U} = \mathbf{Prop}, the type of propositions, this gives X \mapsto \sum_{\phi : \mathbf{Prop}} X^\phi This monad is well-known in type theory by another name – the partiality monad. Specifically, this is the monad M whose Kleisli morphisms A \to M(B) correspond to partial functions A \rightharpoonup B, i.e. functions that associate to each element a : A a proposition \mathsf{def}_f(a) stating whether f is defined at input a, such that if \mathsf{def}_f(a) is true, then one can obtain a value f(a) : B.
It follows that one can more generally consider the polynomial monads derived from polynomial universes as proof-relevant partiality monads.
3.1.1 Rezk completion
Additionally, we can show that any polynomial functor p can be quotiented to a corresponding univalent polynomial, using a familiar construct from the theory of categories in HoTT – the Rezk Completion.
We obtain the Rezk completion of p as the image factorization in \mathbf{Poly^{Cart}} of the classifying morphism p \to u_i given by the subterminal family mentioned above. p \twoheadrightarrow \mathsf{Rezk}(p) \rightarrowtail u_i and since \mathsf{Rezk}(p) is a subobject of a subterminal object, it follows that it is itself subterminal.
Question/Food for Thought. Both \mathsf{List} and \mathsf{Rezk}(\mathsf{List}) are Cartesian monads, hence closed under unit and \Sigma. However, although \mathsf{List} does not have a self-distributive law corresponding to \Pi types, \mathsf{Rezk}(\mathsf{List}) does by the above theorem relating \Pi types to self-distributive laws of univalent polynomials, since finite sets are closed under finite products. Moreover, although \mathsf{List} doesn’t quite have such a distributive law, it almost does, where the pertinent morphism \mathsf{List} \triangleleft \mathsf{List} \to \mathsf{List} \triangleleft \mathsf{List} \in \mathbf{Poly} is the “Cartesian Product” operation on lists that maps a list-of-lists xss = [[x_{11}, \dots, x_{1i_1}], \dots, [x_{j1}, \dots, x_{ji_j}]] to the list of all j-element lists consisting of one element from each list in xss, ordered lexicographically by their occurrence in xss. This operation fails to satisfy some of the equational laws of a distributive law. However, passing to the Rezk completion of \mathsf{List} essentially forces this operation to satisfy these equations – up to homotopy. It is therefore interesting to consider what structure on a base (non-univalent) polynomial suffices to guarantee that its Rezk completion will be closed under \Sigma types / \Pi types.
A potentially related question concerns characterizing the monads of the form u \triangleleft u for u a polynomial universe with \Pi, \Sigma, and unit types. Discussions I’ve had with Steve Awodey, Mathieu Anel & Reid Barton on this point upon my return to CMU this Fall lead me to believe that \mathsf{Rezk}(\mathsf{List}) \triangleleft \mathsf{Rezk}(\mathsf{List}) is a kind of higher-dimensional analgoue of the free commutative ring monad – a surprising result, considering that the ordinary, set-based free commutative ring monad is not polynomial, whereas \mathsf{Rezk}(\mathsf{List}) \triangleleft \mathsf{Rezk}(\mathsf{List}) is. If this result holds, it serves as a further indication that the sheer power of the language of polynomial functors can yet be carried to even greater heights by interpreting this language in the context of HoTT.
4 Conclusion
This post has outlined some of the main results David and I were able to work out during my time at Topos. However, in some sense, this summary barely scratches the surface of how rewarding and intellectually stimulating my time at Topos this Summer truly was. I greatly appreciated the opportunities I had to regularly exchange ideas with David and others at Topos, and to conduct research on topics of deep interest to me in such an environment. Since my return to CMU, I have continued to build upon the research I conducted at Topos this summer, and I am excited to continue exploring these and related topics further. In particular, I am interested in exploring how the type-theoretic semantics outlined above can be developed and generalized to provide internal languages for various notions of interacting processes and dynamical systems that arise in programming, applied math, etc., and to develop a “logic of systems” around these. As this goal seems closely aligned with the mission and interests of the Topos Institute, I anticipate that pursuing it shall keep me in close contact with Topos well into the future, which, based on my experience this Summer, I very much look forward to!
Lastly, I would like to thank David and all the others I had the pleasure of meeting and interacting with on a daily basis at Topos for helping to make my time there so fulfilling!