Cubical type theory: a constructive interpretation of the univalence axiom
From MaRDI portal
(Redirected from 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
- 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 ^*
- Homotopy type theory. Univalent foundations of mathematics
- 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?)
- 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
(only showing first 100 items - show all)- Homotopy type theory in Lean
- Meaning explanations at higher dimension
- Univalent foundations as structuralist foundations
- A cubical model of homotopy type theory
- The Frobenius condition, right properness, and uniform fibrations
- A meaning explanation for HoTT
- The construction of set-truncated higher inductive types
- Constructing a universe for the setoid model
- The univalence axiom in cubical sets
- Canonicity for cubical type theory
- Guarded cubical type theory
- From signatures to monads in \textsf{UniMath}
- A co-reflection of cubical sets into simplicial sets with applications to model structures
- Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda
- Guarded dependent type theory with coinductive types
- Some Wellfounded Trees in UniMath
- Homotopical patch theory
- Higher homotopies in a hierarchy of univalent universes
- scientific article; zbMATH DE number 6694181 (Why is no real title available?)
- A homotopy-theoretic model of function extensionality in the effective topos
- A type theory for synthetic -categories
- The Cayley-Dickson construction in homotopy type theory
- Towards a cubical type theory without an interval
- scientific article; zbMATH DE number 7003193 (Why is no real title available?)
- Models of type theory based on Moore paths
- Denotational semantics of recursive types in synthetic guarded domain theory
- An introduction to univalent foundations for mathematicians
- Constructing higher inductive types as groupoid quotients
- Internal universes in models of homotopy type theory
- The clocks they are adjunctions. Denotational semantics for clocked type theory
- Cubical Agda: a dependently typed programming language with univalence and higher inductive types
- Extensional equality preservation and verified generic programming
- Model structure on the universe of all types in interval type theory
- Syntax and models of Cartesian cubical type theory
- Internal parametricity for cubical type theory
- Canonicity and homotopy canonicity for cubical type theory
- Cubical methods in homotopy type theory and univalent foundations
- Naive cubical type theory
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
- Constructive sheaf models of type theory
- Homotopy canonicity for cubical type theory
- Cubical assemblies, a univalent and impredicative universe and a failure of propositional resizing
- A cubical language for Bishop sets
- Models of Type Theory Based on Moore Paths
- Cellular cohomology in homotopy type theory
- Leibniz equality is isomorphic to Martin-Löf identity, parametrically
- Denotational semantics for guarded dependent type theory
- scientific article; zbMATH DE number 7288622 (Why is no real title available?)
- On higher inductive types in cubical type theory
- Representing continuous functions between greatest fixed points of indexed containers
- Signatures and induction principles for higher inductive-inductive types
- Modal dependent type theory and dependent right adjoints
- Arrow categories of monoidal model categories
- The equivalence of the torus and the product of two circles in homotopy type theory
- Varieties of cubical sets
- A dependently-typed construction of semi-simplicial types
- Simplicial sets inside cubical sets
- Induced model structures for higher categories
- Internal Parametricity for Cubical Type Theory
- Ornaments for Proof Reuse in Coq
- MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
- A rewriting coherence theorem with applications in homotopy type theory
- Finitary type theories with and without contexts
- Decomposing the univalence axiom
- Univalent Foundations and the Equivalence Principle
- Higher Structures in Homotopy Type Theory
- Big step normalisation for type theory
- From cubes to twisted cubes via graph morphisms in type theory
- scientific article; zbMATH DE number 7756115 (Why is no real title available?)
- A formal logic for formal category theory
- Subtyping without reduction
- On Small Types in Univalent Foundations
- A general framework for the semantics of type theory
- Towards a constructive simplicial model of Univalent Foundations
- Synthetic fibered (,1)-category theory
- Topological quantum gates in homotopy type theory
- Kripke-Joyal forcing for type theory and uniform fibrations
- Two-sided Cartesian fibrations of synthetic \((\infty, 1)\)-categories
- Rigidification of cubical quasicategories
- Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
- A type theory for strictly unital -categories
- Two guarded recursive powerdomains for applicative simulation
- Apartness relations between propositions
- Examples and cofibrant generation of effective Kan fibrations
- Parametricity via cohesion
- Free commutative monoids in homotopy type theory
- Towards constructive hybrid semantics
- Quotients in dependent type theory (invited talk)
- What monads can and cannot do with a bit of extra time
- What monads can and cannot do with a few extra pages
- A sound and complete substitution algorithm for multimode type theory
- Automating boundary filling in cubical Agda
- Toward the effective 2-topos
- Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
- A short proof of the Frobenius property for generic fibrations
- The patch topology in univalent foundations
- A parametricity-based formalization of semi-simplicial and semi-cubical sets
- The RedPRL proof assistant (invited paper)
- Primitive recursive dependent type theory
- A foundation for synthetic algebraic geometry
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)
