The univalence axiom in cubical sets

DOI10.1007/s10817-018-9472-6zbMath1506.03064arXiv1710.10941OpenAlexW2963912390WikidataQ114017561 ScholiaQ114017561MaRDI QIDQ2319981

Simon Huber, Thierry Coquand, Marc Bezem

Publication date: 21 August 2019

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

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

zbMATH Keywords

univalence axiomdependent type theorycubical sets

Mathematics Subject Classification ID

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

Related Items (8)

Cubical methods in homotopy type theory and univalent foundations ⋮ Languages of higher-dimensional automata ⋮ A formal logic for formal category theory ⋮ Combining higher-order logic with set theory formalizations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Model structure on the universe of all types in interval type theory ⋮ Syntax and models of Cartesian cubical type theory

Uses Software

• cubicaltt

Cites Work

• Unnamed Item
• An algebraic weak factorisation system on 01-substitution sets: a constructive proof
• Homotopy theoretic models of identity types
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Understanding the small object argument

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