Polynomial pseudomonads and dependent type theory

Abstract

We assemble polynomials in a locally cartesian closed category into a tricategory, allowing us to define the notion of a polynomial pseudomonad and polynomial pseudoalgebra. Working in the context of natural models of type theory, we prove that dependent type theories admitting a unit type and dependent sum types give rise to polynomial pseudomonads, and that those admitting dependent product types give rise to polynomial pseudoalgebras.

26 pages

Cited by in corpus (2)

• Polynomial Functors and Shannon Entropy
• Algebraic models of simple type theories: a polynomial approach