On higher inductive types in cubical type theory
From MaRDI portal
(Redirected from Publication:5145298)
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
Cited in
(43)- Higher homotopies in a hierarchy of univalent universes
- Canonicity for cubical type theory
- Type-theoretic approaches to ordinals
- Impredicative encodings of (higher) inductive types
- \(\pi _{n }(S ^{n })\) in homotopy type theory
- scientific article; zbMATH DE number 6694181 (Why is no real title available?)
- Model structure on the universe of all types in interval type theory
- Extending homotopy type theory with strict equality
- Canonicity and homotopy canonicity for cubical type theory
- Two-level type theory and applications
- scientific article; zbMATH DE number 7559277 (Why is no real title available?)
- 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
- The equivariant model structure on cartesian cubical sets
- Naive cubical type theory
- scientific article; zbMATH DE number 7168146 (Why is no real title available?)
- A foundation for synthetic algebraic geometry
- 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
- scientific article; zbMATH DE number 7215286 (Why is no real title available?)
- The construction of set-truncated higher inductive types
- scientific article; zbMATH DE number 7756115 (Why is no real title available?)
- Internal Parametricity for Cubical Type Theory
- Constructing inductive-inductive types in cubical type theory
- On Church’s thesis in cubical assemblies
- Cubical methods in homotopy type theory and univalent foundations
- scientific article; zbMATH DE number 7561492 (Why is no real title available?)
- Automating boundary filling in cubical Agda
- A cubical approach to synthetic homotopy theory
- Computational higher-dimensional type theory
- Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
- 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?)
- Internal parametricity for cubical type theory
- Cubical type theory: a constructive interpretation of the univalence axiom
- Constructive sheaf models of type theory
- 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
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)
