HackerPapers

arXiv:1607.04156cs.LO

Canonicity for Cubical Type Theory

Simon Huber

Abstract

Cubical type theory is an extension of Martin-Löf type theory recently proposed by Cohen, Coquand, Mörtberg 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.

arXiv comments
34 pages. v2: Added section on propositional truncation; fixed typos. To appear in the Journal of Automated Reasoning
Journal reference
DOI
Subjects
cs.LOLogic in Computer Science

On Hacker News

Linked by 2 identifiable commenters in 2 comments across 1 thread, from Oct 2018 to Oct 2018.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. Reified Generics: The Search for the Cure 2 comments

    • Oh, it's more common a question than you suggest. If I am writing a block of code and I come to some hole in context, for example `foo (bar _) baz`, and I know what type of thing has to go in that hole, then the very next thing I ask is "What term do I need there?". This is a…

      danharajView on HNParent context

    • I know that this question is being asked and reseached -- indeed I do research in this direction. But it's not well understood, and it's not nearly as widely asked a question as the type-inference question which the java compiler asks every time you type something like int n = 2…

      YorkshireSeasonView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.