Cubical type theory: a constructive interpretation of the univalence axiom
From MaRDI portal
Publication:4580226
Abstract: This paper presents a type theory in which it is possible to directly manipulate -dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.
Recommendations
Cites work
- scientific article; zbMATH DE number 6694181 (Why is no real title available?)
- scientific article; zbMATH DE number 3645093 (Why is no real title available?)
- scientific article; zbMATH DE number 3501559 (Why is no real title available?)
- scientific article; zbMATH DE number 3521950 (Why is no real title available?)
- scientific article; zbMATH DE number 1241699 (Why is no real title available?)
- scientific article; zbMATH DE number 1302061 (Why is no real title available?)
- scientific article; zbMATH DE number 1420782 (Why is no real title available?)
- scientific article; zbMATH DE number 226803 (Why is no real title available?)
- A cubical approach to synthetic homotopy theory
- A presheaf model of parametric type theory
- ABSTRACT HOMOTOPY
- An algebraic weak factorisation system on 01-substitution sets: a constructive proof
- Canonicity for cubical type theory
- Extensionality of \(\lambda^*\)
- Homotopy type theory. Univalent foundations of mathematics
- Internal type theory
- Lattices With Involution
- Nominal presentation of cubical sets models of type theory
- Nominal sets. Names and symmetry in computer science
- Nonabelian algebraic topology. Filtered spaces, crossed complexes, cubical homotopy groupoids. With contributions by Christopher D. Wensley and Sergei V. Soloviev
- The Frobenius condition, right properness, and uniform fibrations
- The homotopy theory of type theories
- Type-theory in color
Cited in
(84)- An introduction to univalent foundations for mathematicians
- Model structure on the universe of all types in interval type theory
- scientific article; zbMATH DE number 7215286 (Why is no real title available?)
- A co-reflection of cubical sets into simplicial sets with applications to model structures
- The equivalence of the torus and the product of two circles in homotopy type theory
- Constructing higher inductive types as groupoid quotients
- The Frobenius condition, right properness, and uniform fibrations
- Finitary type theories with and without contexts
- From signatures to monads in \textsf{UniMath}
- Varieties of cubical sets
- Towards a cubical type theory without an interval
- scientific article; zbMATH DE number 7561492 (Why is no real title available?)
- Modal dependent type theory and dependent right adjoints
- Homotopy type theory in Lean
- Meaning explanations at higher dimension
- A meaning explanation for HoTT
- Higher Structures in Homotopy Type Theory
- scientific article; zbMATH DE number 6694181 (Why is no real title available?)
- Canonicity for cubical type theory
- Homotopical patch theory
- Extensional equality preservation and verified generic programming
- Some Wellfounded Trees in UniMath
- Internal Parametricity for Cubical Type Theory
- scientific article; zbMATH DE number 7003193 (Why is no real title available?)
- Decomposing the univalence axiom
- scientific article; zbMATH DE number 7559277 (Why is no real title available?)
- Naive cubical type theory
- Internal parametricity for cubical type theory
- Canonicity and homotopy canonicity for cubical type theory
- Higher homotopies in a hierarchy of univalent universes
- A homotopy-theoretic model of function extensionality in the effective topos
- Guarded dependent type theory with coinductive types
- A rewriting coherence theorem with applications in homotopy type theory
- Cubical methods in homotopy type theory and univalent foundations
- Simplicial sets inside cubical sets
- Ornaments for Proof Reuse in Coq
- Univalent foundations as structuralist foundations
- The univalence axiom in cubical sets
- Denotational semantics for guarded dependent type theory
- A cubical model of homotopy type theory
- Syntax and models of Cartesian cubical type theory
- Constructing a universe for the setoid model
- Cubical Agda: a dependently typed programming language with univalence and higher inductive types
- Constructive sheaf models of type theory
- On higher inductive types in cubical type theory
- The construction of set-truncated higher inductive types
- Denotational semantics of recursive types in synthetic guarded domain theory
- MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
- The clocks they are adjunctions. Denotational semantics for clocked type theory
- Guarded cubical type theory
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
- Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda
- scientific article; zbMATH DE number 7168146 (Why is no real title available?)
- scientific article; zbMATH DE number 7756115 (Why is no real title available?)
- A type theory for synthetic \(\infty\)-categories
- The Cayley-Dickson construction in homotopy type theory
- Models of type theory based on Moore paths
- Internal universes in models of homotopy type theory
- Univalent Foundations and the Equivalence Principle
- Examples and cofibrant generation of effective Kan fibrations
- A general framework for the semantics of type theory
- A formal logic for formal category theory
- Kripke-Joyal forcing for type theory and uniform fibrations
- Two guarded recursive powerdomains for applicative simulation
- Two-sided Cartesian fibrations of synthetic \((\infty, 1)\)-categories
- Models of Type Theory Based on Moore Paths
- Induced model structures for higher categories
- scientific article; zbMATH DE number 7288622 (Why is no real title available?)
- Topological quantum gates in homotopy type theory
- A type theory for strictly unital \(\infty \)-categories
- Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
- Rigidification of cubical quasicategories
- Leibniz equality is isomorphic to Martin-Löf identity, parametrically
- Apartness relations between propositions
- Subtyping without reduction
- Arrow categories of monoidal model categories
- On Small Types in Univalent Foundations
- A dependently-typed construction of semi-simplicial types
- scientific article; zbMATH DE number 7407785 (Why is no real title available?)
- Synthetic fibered \((\infty,1)\)-category theory
- scientific article; zbMATH DE number 7566056 (Why is no real title available?)
- Big step normalisation for type theory
- From cubes to twisted cubes via graph morphisms in type theory
- Towards a constructive simplicial model of Univalent Foundations
This page was built for publication: Cubical type theory: a constructive interpretation of the univalence axiom
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4580226)
