W-types in Homotopy Type Theory
classification
🧮 math.CT
math.LO
keywords
w-typesmodelssimplicialtheorywillaccountadditionapplication
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.