W-types in Homotopy Type Theory
Benno van den Berg, Ieke Moerdijk
TL;DR
This paper demonstrates that the simplicial sets model of the univalence axiom also supports W-types, extending the understanding of models in Homotopy Type Theory and their applications.
Contribution
It provides a detailed account of why the simplicial sets model supports W-types and explores their role in categories of simplicial presheaves and set theory models.
Findings
Simplicial sets model supports W-types in Homotopy Type Theory.
Extension of W-types to categories of simplicial presheaves.
Application of W-types in models of set theory.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsHomotopy and Cohomology in Algebraic Topology · Advanced Topology and Set Theory · Rings, Modules, and Algebras