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, 2022 (arXiv:2211.14801)
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 formulated in homotopy type theory (cf. cohomology in homotopy type theory):
On the Mayer-Vietoris sequence in homotopy type theory:
Dissertation on higher inductive types in cubical type theory:
On the directed univalence axiom in simplicial homotopy type theory:
Last revised on July 6, 2026 at 04:51:59. See the history of this page for a list of all contributions to it.