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 |
|
| 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
(Final published version)
|
| Permalink to this page | |