On higher inductive types in cubical type theory

DOI10.1145/3209108.3209197MaRDI QIDQ5145298zbMATHOpenAlexFDO

Authors Thierry Coquand, Simon Huber, Anders Mörtberg

Publication date 20 January 2021

Published in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

homotopy type theoryunivalent foundationshigher inductive typescubical type theory

Mathematics Subject Classification ID

Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)

Abstract: Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. This paper describes a constructive semantics, expressed in a presheaf topos with suitable structure inspired by cubical sets, of some higher inductive types. It also extends cubical type theory by a syntax for the higher inductive types of spheres, torus, suspensions,truncations, and pushouts. All of these types are justified by the semantics and have judgmental computation rules for all constructors, including the higher dimensional ones, and the universes are closed under these type formers.

Recommendations

• Cubical type theory: a constructive interpretation of the univalence axiom
• Canonicity for cubical type theory
• Canonicity and homotopy canonicity for cubical type theory
• scientific article; zbMATH DE number 6694181
• \(\pi _{n }(S ^{n })\) in homotopy type theory

Cited in

(40)

• An introduction to univalent foundations for mathematicians
• Model structure on the universe of all types in interval type theory
• Two-level type theory and applications
• scientific article; zbMATH DE number 7215286 (Why is no real title available?)
• A class of higher inductive types in Zermelo‐Fraenkel set theory
• Constructing inductive-inductive types in cubical type theory
• Constructing higher inductive types as groupoid quotients
• Extending homotopy type theory with strict equality
• scientific article; zbMATH DE number 7561492 (Why is no real title available?)
• \(\pi _{n }(S ^{n })\) in homotopy type theory
• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• Canonicity for cubical type theory
• Topological quantum gates in homotopy type theory
• Internal Parametricity for Cubical Type Theory
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• scientific article; zbMATH DE number 7559277 (Why is no real title available?)
• Naive cubical type theory
• Computational higher-dimensional type theory
• Internal parametricity for cubical type theory
• Canonicity and homotopy canonicity for cubical type theory
• Higher homotopies in a hierarchy of univalent universes
• Type-theoretic approaches to ordinals
• On Church’s thesis in cubical assemblies
• Non-wellfounded trees in homotopy type theory
• Cubical methods in homotopy type theory and univalent foundations
• Inductive types in homotopy type theory
• Impredicative encodings of (higher) inductive types
• Syntax and models of Cartesian cubical type theory
• Cubical Agda: a dependently typed programming language with univalence and higher inductive types
• scientific article; zbMATH DE number 7559297 (Why is no real title available?)
• Constructive sheaf models of type theory
• The construction of set-truncated higher inductive types
• Constructions with non-recursive higher inductive types
• Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda
• Cubical type theory: a constructive interpretation of the univalence axiom
• scientific article; zbMATH DE number 7168146 (Why is no real title available?)
• scientific article; zbMATH DE number 7756115 (Why is no real title available?)
• The compatibility of the minimalist foundation with homotopy type theory
• Semantics of higher inductive types
• A cubical approach to synthetic homotopy theory

This page was built for publication: On higher inductive types in cubical type theory

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