Questions tagged [irrelevance]

For questions about proof irrelevant propositions and related annotations. Irrelevant types carry typechecking information which is erased at runtime.

Filter by
Sorted by
Tagged with
1 vote
1 answer

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 ...
Adrian L's user avatar
6 votes
0 answers

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 ...
ice1000's user avatar
  • 5,877
5 votes
1 answer

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 ...
ice1000's user avatar
  • 5,877
9 votes
2 answers

Defining coercion for proof irrelevant equality

Say I would like to define coercion for proof irrelevant equality between types. In Coq I try ...
Couchy's user avatar
  • 2,171
12 votes
3 answers

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,015
8 votes
1 answer

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 ...
James Martin's user avatar
  • 1,015