3 papers
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.
math.AT2024
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…