The univalence axiom in cubical sets

DOI10.1007/S10817-018-9472-6MaRDI QIDQ2319981zbMATH OpenOpenAlexWikidataFDO

Authors Marc Bezem, Thierry Coquand, Simon Huber

Publication date 21 August 2019

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

cubical setsdependent type theoryunivalence axiom

Mathematics Subject Classification ID

Type theory (03B38) Other constructive mathematics (03F65) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45) Abstract and axiomatic homotopy theory in algebraic topology (55U35)

Abstract: In this note we show that Voevodsky's univalence axiom holds in the model of type theory based on symmetric cubical sets. We will also discuss Swan's construction of the identity type in this variation of cubical sets. This proves that we have a model of type theory supporting dependent products, dependent sums, univalent universes, and identity types with the usual judgmental equality, and this model is formulated in a constructive metatheory.

Recommendations

• scientific article; zbMATH DE number 1330268
• Minimal surfaces bounded by a pair of convex planar curves
• On the minimal surfaces of Riemann
• On the number of minimal surfaces with a given boundary
• scientific article; zbMATH DE number 1279050

Cites work

• An algebraic weak factorisation system on 01-substitution sets: a constructive proof
• Cubical type theory: a constructive interpretation of the univalence axiom
• Homotopy theoretic models of identity types
• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• Understanding the small object argument

Cited in

(18)

• On the Morse number of embedded and non-embedded minimal immersions spanning wires on the boundary of special bodies in \({\mathbb{R}}^ 3\)
• Cubical type theory: a constructive interpretation of the univalence axiom
• 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
• Cubical methods in homotopy type theory and univalent foundations
• Languages of higher-dimensional automata
• Cubical assemblies, a univalent and impredicative universe and a failure of propositional resizing
• Partial univalence in n-truncated type theory
• A Constructive Model of Directed Univalence in Bicubical Sets
• W-types in homotopy type theory
• Decomposing the univalence axiom
• A formal logic for formal category theory
• Combining higher-order logic with set theory formalizations
• Univalence and ontic structuralism
• Single-set cubical categories and their formalisation with a proof assistant
• The equivariant model structure on cartesian cubical sets
• C-sets of n-uninorms

Describes a project that uses

Uses Software

• cubicaltt

This page was built for publication: The univalence axiom in cubical sets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2319981)