To the top

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

Tell a friend about this page
Print version

Canonicity for Cubical Ty… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

Canonicity for Cubical Type Theory

Journal article
Authors Simon Huber
Published in Journal of Automated Reasoning
Volume 63
Issue 2
Pages 173-210
ISSN 0168-7433
Publication year 2019
Published at Department of Computer Science and Engineering, Computing Science, Programming Logic
Pages 173-210
Language en
Keywords Cubical type theory, Dependent type theory, Canonicity, Computer Science, it ww, 1967, journal of symbolic logic, v32, p198
Subject categories Computer and Information Science


Cubical type theory is an extension of Martin-Lof type theory recently proposed by Cohen, Coquand, Mortberg, and the author which allows for direct manipulation of n-dimensional cubes and where Voevodsky's Univalence Axiom is provable. In this paper we prove canonicity for cubical type theory: any natural number in a context build from only name variables is judgmentally equal to a numeral. To achieve this we formulate a typed and deterministic operational semantics and employ a computability argument adapted to a presheaf-like setting.

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?