Cubical Type Theory: a constructive interpretation of the univalence axiom

DOI10.4230/LIPIcs.TYPES.2015.5zbMath1434.03036arXiv1611.02108OpenAlexW2550513301MaRDI QIDQ4580226

Simon Huber, Anders Mörtberg, Cyril Cohen, Thierry Coquand

Publication date: 13 August 2018

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

zbMATH Keywords

univalence axiomdependent type theorycubical sets

Mathematics Subject Classification ID

Abstract and axiomatic homotopy theory in algebraic topology (55U35) Categorical semantics of formal languages (18C50) Metamathematics of constructive systems (03F50) Type theory (03B38)

Related Items (68)

Varieties of Cubical Sets ⋮ The construction of set-truncated higher inductive types ⋮ Cubical methods in homotopy type theory and univalent foundations ⋮ Naive cubical type theory ⋮ Unnamed Item ⋮ Simplicial sets inside cubical sets ⋮ Constructive sheaf models of type theory ⋮ Unnamed Item ⋮ Finitary type theories with and without contexts ⋮ Homotopy type theory in Lean ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Meaning explanations at higher dimension ⋮ Univalent Foundations and the Equivalence Principle ⋮ Higher Structures in Homotopy Type Theory ⋮ A formal logic for formal category theory ⋮ Subtyping without reduction ⋮ Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda ⋮ On Small Types in Univalent Foundations ⋮ A general framework for the semantics of type theory ⋮ Canonicity and homotopy canonicity for cubical type theory ⋮ Towards a constructive simplicial model of Univalent Foundations ⋮ Leibniz equality is isomorphic to Martin-Löf identity, parametrically ⋮ Univalent foundations as structuralist foundations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Denotational semantics of recursive types in synthetic guarded domain theory ⋮ Unnamed Item ⋮ Denotational semantics for guarded dependent type theory ⋮ A type theory for synthetic $\infty$-categories ⋮ Ornaments for Proof Reuse in Coq ⋮ Constructing a universe for the setoid model ⋮ Unnamed Item ⋮ The Frobenius condition, right properness, and uniform fibrations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ An introduction to univalent foundations for mathematicians ⋮ Unnamed Item ⋮ A cubical model of homotopy type theory ⋮ Guarded Dependent Type Theory with Coinductive Types ⋮ Unnamed Item ⋮ Cartesian cubical computational type theory: Constructive reasoning with paths and equalities ⋮ Modal dependent type theory and dependent right adjoints ⋮ A meaning explanation for HoTT ⋮ Some Wellfounded Trees in UniMath ⋮ The univalence axiom in cubical sets ⋮ Canonicity for cubical type theory ⋮ Guarded cubical type theory ⋮ From signatures to monads in \textsf{UniMath} ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Towards a Cubical Type Theory without an Interval ⋮ Arrow categories of monoidal model categories ⋮ Models of Type Theory Based on Moore Paths ⋮ A co-reflection of cubical sets into simplicial sets with applications to model structures ⋮ A homotopy-theoretic model of function extensionality in the effective topos ⋮ Unnamed Item ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types ⋮ Extensional equality preservation and verified generic programming ⋮ Induced model structures for higher categories ⋮ Model structure on the universe of all types in interval type theory ⋮ Syntax and models of Cartesian cubical type theory ⋮ MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS ⋮ A rewriting coherence theorem with applications in homotopy type theory

Uses Software

• cubicaltt

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Nonabelian algebraic topology. Filtered spaces, crossed complexes, cubical homotopy groupoids. With contributions by Christopher D. Wensley and Sergei V. Soloviev
• The homotopy theory of type theories
• The Frobenius condition, right properness, and uniform fibrations
• Canonicity for cubical type theory
• Nominal Sets
• An algebraic weak factorisation system on 01-substitution sets: a constructive proof
• A Cubical Approach to Synthetic Homotopy Theory
• Internal type theory
• Type-theory in color
• Extensionality of lambda
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Lattices With Involution
• ABSTRACT HOMOTOPY
• A presheaf model of parametric type theory

This page was built for publication: Cubical Type Theory: a constructive interpretation of the univalence axiom