Log In

W-types in homotopy type theory

Files

w_types_in_homotopy_type_theory.pdf (168.32 KB)

Publication date

2015-06-30

Authors

van den Berg, B.ISNI 0000000387014378
Moerdijk, IekeISNI 0000000115731023

Editors

Advisors

Supervisors

DOI

https://doi.org/10.1017/S0960129514000516

Document Type

Article

Metadata

Show full item record

Collections

Utrecht University Repository
Open Access logo

License

taverne

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

Taverne, Mathematics (miscellaneous), Computer Science Applications

Citation

Van Den Berg, B & Moerdijk, I 2015, 'W-types in homotopy type theory', Mathematical Structures in Computer Science, vol. 25, no. 5, pp. 1100-1115. https://doi.org/10.1017/S0960129514000516

URI

https://dspace.library.uu.nl/handle/1874/419650