W-types in homotopy type theory

Benno Van Den Berg; Ieke Moerdijk

doi:10.1017/S0960129514000516

W-types in homotopy type theory

Benno Van Den Berg, Ieke Moerdijk

extern

Research output: Contribution to journal › Article › Academic › peer-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 language	English
Pages (from-to)	1100-1115
Number of pages	16
Journal	Mathematical Structures in Computer Science
Volume	25
Issue number	5
DOIs	https://doi.org/10.1017/S0960129514000516
Publication status	Published - 30 Jun 2015
Externally published	Yes

Bibliographical note

Publisher Copyright:
© 2014 Cambridge University Press.

Access to Document

10.1017/S0960129514000516

w-types-in-homotopy-type-theoryFinal published version, 168 KBLicence: Taverne

Cite this

@article{2a50b6cce9a24defb85545b938324ae3,

title = "W-types in homotopy type 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.",

author = "\{Van Den Berg\}, Benno and Ieke Moerdijk",

note = "Publisher Copyright: {\textcopyright} 2014 Cambridge University Press.",

year = "2015",

month = jun,

day = "30",

doi = "10.1017/S0960129514000516",

language = "English",

volume = "25",

pages = "1100--1115",

journal = "Mathematical Structures in Computer Science",

issn = "0960-1295",

publisher = "Cambridge University Press",

number = "5",

}

TY - JOUR

T1 - W-types in homotopy type theory

AU - Van Den Berg, Benno

AU - Moerdijk, Ieke

PY - 2015/6/30

Y1 - 2015/6/30

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/84928694525

U2 - 10.1017/S0960129514000516

DO - 10.1017/S0960129514000516

M3 - Article

AN - SCOPUS:84928694525

SN - 0960-1295

VL - 25

SP - 1100

EP - 1115

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

IS - 5

ER -

W-types in homotopy type theory

Abstract

Bibliographical note

Access to Document

Other files and links

Fingerprint

Cite this