134 citations · 234 across the 10 of their papers we have counts for
15 papers
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…
Sheaf Representations and Duality in Logic
Steve Awodey
The fundamental duality theories relating algebra and geometry that were discovered in the mid-20th century can also be applied to logic via its algebraization under categorical lo…
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 proposition is the (homotopy) type of its proofs
Steve Awodey
An introduction and survey of homotopy type theory in honor of W.W. Tait.
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…
Homotopy-initial algebras in type theory
Steve Awodey, Nicola Gambino, Kristina Sojakova
We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion…