W-types in homotopy type theory

DOI10.1017/S0960129514000516zbMath1362.03009arXiv1307.2765OpenAlexW2963457218MaRDI QIDQ5740651

Benno van den Berg, Ieke Moerdijk

Publication date: 27 July 2016

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1307.2765

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20) Topological categories, foundations of homotopy theory (55U40)

Related Items (6)

Univalent completion ⋮ W-types in homotopy-type theory – CORRIGENDUM ⋮ Towards a constructive simplicial model of Univalent Foundations ⋮ Derived rules for predicative set theory: an application of sheaves ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ Semantics of higher inductive types

Cites Work

• On an extension of the notion of Reedy category
• Non-well-founded trees in categories
• Wellfounded trees in categories
• Categories and cohomology theories
• Some free constructions in realizability and proof theory
• Reedy categories and the \(\varTheta\)-construction
• Rational homotopy theory
• Containers: Constructing strictly positive types
• A construction of non-well-founded sets within Martin-Löf's type theory
• Dendroidal Segal spaces and ∞-operads
• Models of non-well-founded sets via an indexed final coalgebra theorem
• Simplicial homotopy theory
• Type theories, toposes and constructive set theory: Predicative aspects of AST

This page was built for publication: W-types in homotopy type theory