To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Cubical type theory: a co… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

Cubical type theory: a constructive interpretation of the univalence axiom

Journal article
Authors Cyril Cohen
Thierry Coquand
Simon Huber
Anders Mörtberg
Published in Journal of Applied Logics
Volume 4
Issue 10
Pages 3127-3169
ISSN 2055-3706
Publication year 2017
Published at Department of Computer Science and Engineering, Computing Science, Programming Logic
Department of Computer Science and Engineering (GU)
Pages 3127-3169
Language en
Subject categories Computer Science


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.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?