W-types in Homotopy Type Theory
Category Theory
2015-11-26 v3 Logic
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.
Keywords
Cite
@article{arxiv.1307.2765,
title = {W-types in Homotopy Type Theory},
author = {Benno van den Berg and Ieke Moerdijk},
journal= {arXiv preprint arXiv:1307.2765},
year = {2015}
}
Comments
We have corrected the statement of Theorem 3.4. We thank Christian Sattler for alerting us to the error in the original version