The construction of set-truncated higher inductive types

DOI10.1016/J.ENTCS.2019.09.014OpenAlexW2994973104WikidataQ113317349 ScholiaQ113317349MaRDI 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)

Cites Work

• Structural induction and coinduction in a fibrational setting
• Title not available (Why is that?)
• Inductive families
• The formal theory of monads
• Types are weak \(\omega \)-groupoids
• Weak ω-Categories from Intensional Type Theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• The simplicial model of univalent foundations (after Voevodsky)
• Univalent categories and the Rezk completion
• A Syntax for Higher Inductive-Inductive Types
• Computational higher-dimensional type theory
• Inductive Types in Homotopy Type Theory
• Constructions with Non-Recursive Higher Inductive Types
• Semantics of higher inductive types
• A Type-Theoretical Definition of Weak {\omega}-Categories
• Title not available (Why is that?)
• Quotient inductive-inductive types
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Wild omega-Categories for the Homotopy Hypothesis in Type Theory
• Finitary higher inductive types in the groupoid model
• Higher inductive types as homotopy-initial algebras
• Eilenberg-MacLane spaces in homotopy type theory
• Sets in homotopy type theory
• Title not available (Why is that?)
• The real projective spaces in homotopy type theory
• Type theory in type theory using quotient inductive types
• Partiality, Revisited
• Displayed Categories
• Quotienting the delay monad by weak bisimilarity
• A syntactical approach to weak omega-groupoids
• On Higher Inductive Types in Cubical Type Theory
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• Title not available (Why is that?)
• Homotopical patch theory

Cited In (2)

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

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)