Questions tagged [canonicity]
A type theory satisfies canonicity if every term computes to a canonical form, built explicitly using the constructors of its type.
7
questions
1
vote
1
answer
195
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 (...
- 209
3
votes
1
answer
206
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 ...
- 5,857
7
votes
1
answer
121
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 ...
- 5,857
13
votes
1
answer
275
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 ...
- 660
17
votes
2
answers
285
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., ...
- 660
16
votes
2
answers
350
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 ...
- 1,015
12
votes
3
answers
315
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 ...
- 1,015