Polynomial pseudomonads and dependent type theory
Category Theory
2018-02-06 v1 Logic
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.
Cite
@article{arxiv.1802.00997,
title = {Polynomial pseudomonads and dependent type theory},
author = {Steve Awodey and Clive Newstead},
journal= {arXiv preprint arXiv:1802.00997},
year = {2018}
}
Comments
26 pages