W-types in homotopy type theory

Authors
Publication date 2015
Journal Mathematical Structures in Computer Science
Volume | Issue number 25 | 5
Pages (from-to) 1100-1115
Organisations
  • Faculty of Science (FNWI)
  • Interfacultary Research - Institute for Logic, Language and Computation (ILLC)
Abstract We will give a detailed account of why the simplicial sets model of the univalence axiom due to Voevodsky also models W-types. In addition, we will discuss W-types in categories of simplicial presheaves and an application to models of set theory.
Document type Article
Language English
Published at https://doi.org/10.1017/S0960129514000516
Permalink to this page
Back