W-types in homotopy type theory

Benno Van Den Berg, Ieke Moerdijk

Research output: Contribution to journalArticleAcademicpeer-review

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.

Original languageEnglish
Pages (from-to)1100-1115
Number of pages16
JournalMathematical Structures in Computer Science
Volume25
Issue number5
DOIs
Publication statusPublished - 30 Jun 2015
Externally publishedYes

Bibliographical note

Publisher Copyright:
© 2014 Cambridge University Press.

Fingerprint

Dive into the research topics of 'W-types in homotopy type theory'. Together they form a unique fingerprint.

Cite this