Early discussion of what came to be known as homotopy type theory:

- Michael Warren,
*Homotopy theoretic aspects of constructive type theory*, PhD thesis (2008) [pdf, pdf]

Proof that every simplicial model category in which the cofibrations are monomorphisms provides a sound model for intensional Martin-Löf type theory (i.e. including the identity types used in homotopy type theory):

- Steve Awodey, Michael Warren,
*Homotopy theoretic models of identity type*, Mathematical Proceedings of the Cambridge Philosophical Society**146**1 (2009) [arXiv:0709.0248, doi:10.1017/S0305004108001783]

On the categorical semantics of dependent type theory via comprehension categories:

- Peter LeFanu Lumsdaine, Michael Warren,
*The local universes model: An overlooked coherence construction for dependent type theory*, ACM Trans. Comput. Log.,**16**3 no 23 (2015) 1-31 [arXiv:1411.1736, doi:10.1145/2754931]

category: people

Last revised on February 15, 2023 at 06:59:02. See the history of this page for a list of all contributions to it.