Polynomial pseudomonads and dependent type theory

Steve Awodey, Clive Newstead

Research output: Contribution to journalArticlepeer-review

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.

Original languageEnglish (US)
JournalUnknown Journal
StatePublished - Feb 3 2018
Externally publishedYes

ASJC Scopus subject areas

  • General

Fingerprint Dive into the research topics of 'Polynomial pseudomonads and dependent type theory'. Together they form a unique fingerprint.

Cite this