Reference. Polynomial Universes in Homotopy Type Theory
Awodey, later with Newstead, showed how polynomial functors with extra structure (termed “natural models”) hold within them the categorical semantics for dependent type theory. Their work presented these ideas clearly but ultimately led them outside of the usual category of polynomial functors to a particular tricategory of polynomials in order to explain all of the structure possessed by such models. This paper builds off that work – explicating the categorical semantics of dependent type theory by axiomatizing them entirely in terms of the usual category of polynomial functors. In order to handle the higher-categorical coherences required for such an explanation, we work with polynomial functors in the language of Homotopy Type Theory (HoTT), which allows for higher-dimensional structures to be expressed purely within this category. The move to HoTT moreover enables us to express a key additional condition on polynomial functors – univalence – which is sufficient to guarantee that models of type theory expressed as univalent polynomials satisfy all higher coherences of their corresponding algebraic structures, purely in virtue of being closed under the usual constructors of dependent type theory. We call polynomial functors satisfying this condition polynomial universes. As an example of the simplification to the theory of natural models this enables, we highlight the fact that a polynomial universe being closed under dependent product types implies the existence of a distributive law of monads, which witnesses the usual distributivity of dependent products over dependent sums.
Cite
Cites 15 works (3 here)
With notes (3)
All -toposes have strict univalent universes shulman-2019-all
We prove the conjecture that any Grothendieck -topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can be used as a formal language for reasoning internally to -toposes, just as higher-order logic is used for 1-toposes. As part of the proof, we give a new, more explicit, characterization of the fibrations in injective model structures on presheaf categories. In particular, we show that they generalize the coflexible algebras of 2-monad theory.
Univalent categories and the Rezk completion ahrens_etal_2015
We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of ‘category’ for which equality and equivalence of categories agree. Such categories satisfy a version of the univalence axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects; we call them ‘saturated’ or ‘univalent’ categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.
External (12)
- A Polynomial Construction of Nerves for Higher Categories (2024)
- Categorical Systems Theory (2023)
- All Concepts are Cat# (2023)
- No-go theorems for distributive laws (2022)
- Natural models of homotopy type theory (2018)
- Polynomial pseudomonads and dependent type theory (2018)
- Monadic containers and universes (talk slides) (2018)
- Polynomial functors and polynomial monads (2009)
- The formal theory of monads II (2002)
- Locally cartesian closed categories and type theory (1984)
- An Intuitionistic Theory of Types: Predicative Part (1975)
- Polynomial Functors: A Mathematical Theory of Interaction