nLab Michael Warren

Selected writings

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):

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

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.