134 citations · 234 across the 10 of their papers we have counts for
4 papers · 1 filter
Cartesian cubical model categories
Steve Awodey
The category of Cartesian cubical sets is introduced and endowed with a Quillen model structure using ideas coming from recent constructions of cubical systems of univalent type th…
Polynomial pseudomonads and dependent type theory
Steve Awodey, Clive Newstead
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. Workin…
A cubical model of homotopy type theory
Steve Awodey
We construct an algebraic weak factorization system on the cartesian cubical sets, in which the canonical path object factorization induced by th…
Type theory and homotopy
Steve Awodey
The purpose of this survey article is to introduce the reader to a connection between Logic, Geometry, and Algebra which has recently come to light in the form of an interpretation…