Canonicity for cubical type theory

DOI10.1007/S10817-018-9469-1zbMATH Open1477.03036arXiv1607.04156OpenAlexW2963955593WikidataQ129724373 ScholiaQ129724373MaRDI QIDQ2319982FDOQ2319982

Simon Huber

Publication date: 21 August 2019

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

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.

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

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 Keywords

canonicitydependent type theorycubical type theory

Mathematics Subject Classification ID

Type theory (03B38)

Cites Work

• Homotopy Type Theory: Univalent Foundations of Mathematics
• Title not available (Why is that?)
• Intensional interpretations of functionals of finite type I
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Computational higher-dimensional type theory
• Title not available (Why is that?)
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• The Independence of Markov's Principle in Type Theory.
• On irrelevance and algorithmic equality in predicative type theory

Cited In (13)

• Canonicity and homotopy canonicity for cubical type theory
• Title not available (Why is that?)
• Guarded cubical type theory
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Title not available (Why is that?)
• Internal Parametricity for Cubical Type Theory
• Cubical methods in homotopy type theory and univalent foundations
• On equivalence and canonical forms in the LF type theory
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• Title not available (Why is that?)
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• Title not available (Why is that?)
• Syntax and models of Cartesian cubical type theory

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)