The construction of set-truncated higher inductive types

DOI10.1016/J.ENTCS.2019.09.014OpenAlexW2994973104WikidataQ113317349MaRDI QIDQ2133178FDOQ2133178

Authors 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

zbMATH Keywords

category theoryCoqintuitionistic type theoryhomotopy type theoryhigher inductive typessetoids

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• Constructing higher inductive types as groupoid quotients
• Constructing higher inductive types as groupoid quotients
• Semantics of higher inductive types
• Quotient inductive-inductive types
• Constructions with non-recursive higher inductive types

Cites work

• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• scientific article; zbMATH DE number 7559271 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• A Type-Theoretical Definition of Weak {\omega}-Categories
• A syntactical approach to weak omega-groupoids
• A syntax for higher inductive-inductive types
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• Computational higher-dimensional type theory
• Constructions with non-recursive higher inductive types
• Cubical type theory: a constructive interpretation of the univalence axiom
• Displayed categories
• Eilenberg-MacLane spaces in homotopy type theory
• Finitary higher inductive types in the groupoid model
• Higher inductive types as homotopy-initial algebras
• Homotopical patch theory
• Homotopy type theory. Univalent foundations of mathematics
• Inductive families
• Inductive types in homotopy type theory
• Normalisation by evaluation for type theory, in type theory
• On higher inductive types in cubical type theory
• Partiality, Revisited
• Quotient inductive-inductive types
• Quotienting the delay monad by weak bisimilarity
• Semantics of higher inductive types
• Sets in homotopy type theory
• Structural induction and coinduction in a fibrational setting
• The formal theory of monads
• The real projective spaces in homotopy type theory
• The simplicial model of univalent foundations (after Voevodsky)
• Type theory in type theory using quotient inductive types
• Types are weak \(\omega \)-groupoids
• Univalent categories and the Rezk completion
• Weak ω-Categories from Intensional Type Theory
• Wild \(\omega\)-categories for the homotopy hypothesis in type theory

Cited in

(2)

• Quotients by idempotent functions in Cedille
• A construction method for induced types and its application to \(G_2\)

Describes a project that uses

Uses Software

• UniMath
• cubicaltt

This page was built for publication: The construction of set-truncated higher inductive types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2133178)