The construction of set-truncated higher inductive types
From MaRDI portal
Publication:2133178
DOI10.1016/j.entcs.2019.09.014OpenAlexW2994973104WikidataQ113317349 ScholiaQ113317349MaRDI QIDQ2133178
Niels van der Weide, Herman Geuvers
Publication date: 29 April 2022
Full work available at URL: https://doi.org/10.1016/j.entcs.2019.09.014
Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Structural induction and coinduction in a fibrational setting
- Inductive families
- Quotient inductive-inductive types
- The simplicial model of univalent foundations (after Voevodsky)
- Finitary higher inductive types in the groupoid model
- The formal theory of monads
- Higher Inductive Types as Homotopy-Initial Algebras
- Type theory in type theory using quotient inductive types
- Inductive Types in Homotopy Type Theory
- Partiality, Revisited
- Types are weak ω -groupoids
- Displayed Categories
- Weak ω-Categories from Intensional Type Theory
- Quotienting the delay monad by weak bisimilarity
- Cubical Type Theory: a constructive interpretation of the univalence axiom
- Eilenberg-MacLane spaces in homotopy type theory
- Constructions with Non-Recursive Higher Inductive Types
- Semantics of higher inductive types
- A Syntax for Higher Inductive-Inductive Types
- A Type-Theoretical Definition of Weak {\omega}-Categories
- The real projective spaces in homotopy type theory
- On Higher Inductive Types in Cubical Type Theory
- Calculating the Fundamental Group of the Circle in Homotopy Type Theory
- Wild omega-Categories for the Homotopy Hypothesis in Type Theory
- Computational higher-dimensional type theory
- Homotopical patch theory
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Univalent categories and the Rezk completion
- Sets in homotopy type theory
This page was built for publication: The construction of set-truncated higher inductive types
