web page (under construction)
On the categorical semantics of W-types by initial algebras over an endofunctor in homotopy type theory:
On a version of the Homotopy Type System with application to semi-simplicial types in homotopy type theory:
On the fibration category of semi-simplicial sets:
On homotopy canonicity for cubical type theory:
Thierry Coquand, Simon Huber, Christian Sattler: Homotopy canonicity for cubical type theory, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) [doi:10.4230/LIPIcs.FSCD.2019.11, arXiv:1902.06572]
Thierry Coquand, Simon Huber, Christian Sattler: Canonicity and homotopy canonicity for cubical type theory, Logical Methods in Computer Science 18 1 (2022) lmcs:9043 [doi:10.46298/lmcs-18%281%3A28%292022, arXiv:1902.06572]
On the constructive model structure on simplicial sets:
On the Joyal-type model structure for cubical quasi-categories on cubical sets with connections:
A constructive model of homotopy type theory in a Quillen model category of cubical sets that classically presents the usual homotopy theory of spaces:
On the universal fibration of (infinity,1)-categories:
Last revised on April 10, 2026 at 08:09:21. See the history of this page for a list of all contributions to it.