On higher inductive types in cubical type theory

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

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)

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; zbMATH DE number 6694181
• \(\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 (39)

• Canonicity for cubical type theory
• Type-theoretic approaches to ordinals
• Impredicative encodings of (higher) inductive types
• Model structure on the universe of all types in interval type theory
• \(\pi _{n }(S ^{n })\) in homotopy type theory
• Title not available (Why is that?)
• Extending homotopy type theory with strict equality
• 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
• Naive cubical type theory
• Title not available (Why is that?)
• Semantics of higher inductive types
• Inductive types in homotopy type theory
• Constructions with non-recursive higher inductive types
• Constructing higher inductive types as groupoid quotients
• 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?)
• A cubical approach to synthetic homotopy theory
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• Computational higher-dimensional type theory
• Cubical Agda: a dependently typed programming language with univalence and higher inductive types
• Title not available (Why is that?)
• Internal parametricity for cubical type theory
• Constructive sheaf models of type theory
• Cubical type theory: a constructive interpretation of the univalence axiom
• Non-wellfounded trees in homotopy 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
• Higher homotopies in a hierarchy of univalent universes

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)