Cubical Type Theory: a constructive interpretation of the univalence axiom

2016/11/07 by Cyril Cohen, Thierry Coquand, Cohen, Cyril +5 · 16 citations
Computer Science · Mathematics · Psychology · #Advanced Topology and Set Theory #F.3.2 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Philosophy and Theoretical Science

paper · doi:10.48550/arxiv.1611.02108

openalex publication_date 2016/11/07 · openalex created_date 2019/06/27 · openalex updated_date 2026/07/28

Abstract

This paper presents a type theory in which it is possible to directly manipulate n-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.

Cited by

• A Toolkit for Structured Lifts
• Multi-clocked Guarded Recursion Beyond ω
• Nominal Type Theory by Nullary Internal Parametricity
• Realization of relational presheaves
• The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups
• Computational Paths Form a Weak ω-Groupoid
• Towards Computational UIP in Cubical Agda
• Formalizing Computational Paths and Fundamental Groups in Lean
• Internalizing Extensions in Lattices of Type Theories
• A Judgmental Construction of Directed Type Theory
• Formalization of the zigzag construction of path spaces of pushouts in homotopy type theory
• Extension Types for Free
• Mechanizing Synthetic Tait Computability in Istari
• W-Types with Reductions and the Small Object Argument
• The derivator of setoids
• AdapTT: Functoriality for Dependent Type Casts

Related

• The univalence axiom in cubical sets
• On Higher Inductive Types in Cubical Type Theory
• Yet another cubical type theory, but via a semantic approach
• Cubical informal type theory: the higher groupoid structure
• Cubical sets and the topological topos