Questions tagged [irrelevance]
For questions about proof irrelevant propositions and related annotations. Irrelevant types carry typechecking information which is erased at runtime.
6
questions
1
vote
1
answer
68
views
Use proof irrelevance in cast
I'm working using cast in Coq.Vectors. When trying to rewrite with proofs, I'd like to use the fact of proof irrelevance (Coq.Logic.Eqdep_dec), preferably automatically. I.e., when I have a lemma ...
- 23
6
votes
0
answers
147
views
How does the modality-based irrelevance compare to universe-based irrelevance (`Prop`)?
I understand proof irrelevance implementation as one of the two language features listed below:
Prop as SProp in Coq or ...
- 5,877
5
votes
1
answer
151
views
Is 'subsingleton elimination' the same concept as 'function comprehension'?
I saw:
subsingleton elimination from lean-forward, which, I so far understood as "eliminate a type in Prop to a type in whatever universe that we know has at ...
- 5,877
9
votes
2
answers
432
views
Defining coercion for proof irrelevant equality
Say I would like to define coercion for proof irrelevant equality between types. In Coq I try
...
- 2,171
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
8
votes
1
answer
244
views
Why is `--irrelevant-projections` unsafe in Agda?
In Agda, irrelevance is an annotation which marks a parameter, record field, or definition which "will only be typechecked but never evaluated", with the consequence that irrelevant ...
- 1,015