On higher inductive types in cubical type theory

DOI10.1145/3209108.3209197zbMATH Open1452.03036arXiv1802.01170OpenAlexW2964029175MaRDI QIDQ5145298FDOQ5145298

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)

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.

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

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
• \(\pi _{n }(S ^{n })\) in homotopy type theory

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)

Cited In (28)

• Type-theoretic approaches to ordinals
• Model structure on the universe of all types in interval type theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Canonicity and homotopy canonicity for cubical type theory
• Two-level type theory and applications
• Title not available (Why is that?)
• Topological quantum gates in homotopy type theory
• A class of higher inductive types in Zermelo‐Fraenkel set theory
• Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda
• Cubical Agda: A dependently typed programming language with univalence and higher inductive types
• Naive cubical type theory
• Title not available (Why is that?)
• Semantics of higher inductive types
• Title not available (Why is that?)
• Title not available (Why is that?)
• The construction of set-truncated higher inductive types
• Title not available (Why is that?)
• Internal Parametricity for Cubical Type Theory
• On Church’s thesis in cubical assemblies
• Cubical methods in homotopy type theory and univalent foundations
• Title not available (Why is that?)
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• Title not available (Why is that?)
• Constructive sheaf models of type theory
• Syntax and models of Cartesian cubical type theory
• An introduction to univalent foundations for mathematicians
• The compatibility of the minimalist foundation with homotopy type 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)