3 papers
math.AT2026
The equivariant model structure on cartesian cubical sets
Steve Awodey, Evan Cavallo, Thierry Coquand +2
We develop a constructive model of homotopy type theory in a Quillen model category that classically presents the usual homotopy theory of spaces. Our model is based on presheaves…
math.CT2026
Path Types in Algebraic Type Theory
Steve Awodey, Joseph Hua
A new approach to the semantics of identity types in intensional Martin-Löf type theory is proposed, assuming only a category with finite limits and an interval. The specification…
math.CT2025
Algebraic Type Theory, Part 1: Martin-Löf algebras
Steve Awodey
A new algebraic treatment of dependent type theory is proposed using ideas derived from topos theory and algebraic set theory.