Skip to main content

Questions tagged [canonicity]

A type theory satisfies canonicity if every term computes to a canonical form, built explicitly using the constructors of its type.

Filter by
Sorted by
Tagged with
1 vote
1 answer
63 views

About the use of command Canonical in Coq for mantaining Record Type information

Inside the MathComp book https://zenodo.org/records/7118596 there is the following example of use for the Canonical command: ...
Bruno Rafael's user avatar
1 vote
1 answer
268 views

Does Agda's --injective-type-constructors flag have canonicity?

Since 2010/01/07, when the Anti-classicality of Agda was proved by Chung-Kil Hur, Agda's --injective-type-constructors is separated from the main branch of Agda (...
Ember Edison's user avatar
3 votes
1 answer
214 views

Does cubical canonicity imply closed version of regularity?

Clarification of my terminologies: Cubical canonicity: a generalized version of canonicity that the "generated by introduction rules" property holds in, not just closed context, but also ...
ice1000's user avatar
  • 6,186
7 votes
1 answer
125 views

How is "propositional canonicity" useful?

I know that canonicity implies that all closed terms can be computed into a term generated by introduction rules, but people (I forgot who) told me about "propositional canonicity", where ...
ice1000's user avatar
  • 6,186
13 votes
1 answer
303 views

Does the canonicity of natural number imply that of all types?

I've heard about a folklore claim that If all terms of ℕ are literals, all closed terms admit canonical form. In MLTT-style type theories. I am assured that it's true for Bool if one also assumes ...
KANG Rongji's user avatar
18 votes
2 answers
353 views

Is there computational interpretation for countable choice?

I've wondered how a type theory/proof assistant could manage to add countable choice (or its dependent choice version) as something primitive as well as to keep the computational properties, e.g., ...
KANG Rongji's user avatar
16 votes
2 answers
427 views

What axioms have a computational interpretation?

The type of call/cc (which may be realized with the 𝜆𝜇-calculus) corresponds with Peirce's Law, which implies LEM. This answer by Pierre-Marie Pédrot explains how ...
James Martin's user avatar
  • 1,025
12 votes
3 answers
359 views

Why does it matter if canonicity holds for irrelevant types?

Suppose you were to add a non-constructive axiom which only applies to irrelevant types, such as the irrelevance axiom. To my understanding canonicity and strong normalization are defining features of ...
James Martin's user avatar
  • 1,025