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.
Original language | English |
---|---|
Pages (from-to) | 1100-1115 |
Number of pages | 16 |
Journal | Mathematical Structures in Computer Science |
Volume | 25 |
Issue number | 5 |
DOIs | |
Publication status | Published - 30 Jun 2015 |
Externally published | Yes |
Bibliographical note
Publisher Copyright:© 2014 Cambridge University Press.