Canonicity for cubical type theory

DOI10.1007/S10817-018-9469-1MaRDI QIDQ2319982zbMATH OpenOpenAlexWikidataFDO

Authors 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/1607.04156

zbMATH Keywords

canonicitydependent type theorycubical type theory

Mathematics Subject Classification ID

Type theory (03B38)

Abstract: Cubical type theory is an extension of Martin-L"of type theory recently proposed by Cohen, Coquand, M"ortberg 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.

Recommendations

• Canonicity and homotopy canonicity for cubical type theory
• Computational higher-dimensional type theory
• On higher inductive types in cubical type theory
• Cubical type theory: a constructive interpretation of the univalence axiom
• scientific article; zbMATH DE number 6694181

Cites work

• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• scientific article; zbMATH DE number 1302061 (Why is no real title available?)
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Computational higher-dimensional type theory
• Cubical type theory: a constructive interpretation of the univalence axiom
• Homotopy type theory. Univalent foundations of mathematics
• Intensional interpretations of functionals of finite type I
• On irrelevance and algorithmic equality in predicative type theory
• The independence of Markov's principle in type theory

Cited in

(21)

• Canonicity for 2-dimensional type theory
• Canonicity and homotopy canonicity for cubical type theory
• scientific article; zbMATH DE number 7559277 (Why is no real title available?)
• Guarded cubical type theory
• On higher inductive types in cubical type theory
• Naive cubical type theory
• Towards a cubical type theory without an interval
• scientific article; zbMATH DE number 7003193 (Why is no real title available?)
• Internal Parametricity for Cubical Type Theory
• On Church’s thesis in cubical assemblies
• Cubical methods in homotopy type theory and univalent foundations
• On equivalence and canonical forms in the LF type theory
• Computational higher-dimensional type theory
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• Cubical Agda: a dependently typed programming language with univalence and higher inductive types
• scientific article; zbMATH DE number 7559297 (Why is no real title available?)
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• Internal parametricity for cubical type theory
• Cubical type theory: a constructive interpretation of the univalence axiom
• scientific article; zbMATH DE number 7566056 (Why is no real title available?)
• Syntax and models of Cartesian cubical type theory

Describes a project that uses

Uses Software

• cubicaltt

This page was built for publication: Canonicity for cubical type theory

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