On the type theoretic axiom of replacement:
On the directed univalence axiom in simplicial homotopy type theory:
On cubical type theory based on categories of cubes with reversals:
On the relationship between the univalence axiom and function extensionality:
On algebraic weak factorization systems and the algebraic small object argument:
A constructive model of homotopy type theory in a Quillen model category of equivariantly fibrant cartesian cubical sets that classically presents the usual homotopy theory of spaces:
On the cubical sets over the cube category with cartesian structure and one connection, and the fact that the Quillen model category associated to its model of homotopy type theory classically presents the usual homotopy theory of spaces:
Evan Cavallo, Christian Sattler, Relative elegance and cartesian cubes with one connection, Canadian Journal of Mathematics (2025) 1–64 [arXiv:2211.14801, doi:10.4153/S0008414X25101466]
Evan Cavallo, Cubes with one connection and relative elegance, Homotopy Type Theory Electronic Seminar Talks, 3 November 2022 (slides, video)
On combining parametric dependent type theory with cubical type theory:
On models of homotopy type theory and cubical type theory:
On a schema for higher inductive types in cubical type theory:
On generalized (Eilenberg-Steenrod) cohomology and the Mayer-Vietoris sequence formulated in homotopy type theory (cf. cohomology in homotopy type theory):
Dissertation on higher inductive types and internal parametricity in cubical type theory:
Last revised on July 30, 2026 at 12:35:28. See the history of this page for a list of all contributions to it.