W-types in Homotopy Type Theory
arXiv:1307.2765
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.
arXiv commentWe have corrected the statement of Theorem 3.4. We thank Christian Sattler for alerting us to the error in the original version