2018/02/03 by Steve Awodey, Awodey, Steve, Clive Newstead +1 · 2 citations
Computer Science · Mathematics · #03G30 #18C15 (Primary) #18D05 #18D15 #18D25 (Secondary) #Advanced Topics in Algebra #Category Theory (math.CT) #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO) #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1802.00997
openalex publication_date 2018/02/03 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.