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
3 votes
1 answer
65 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 ...
  • 4,740
9 votes
2 answers
387 views

Defining coercion for proof irrelevant equality

Say I would like to define coercion for proof irrelevant equality between types. In Coq I try ...
  • 1,868
12 votes
3 answers
244 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 ...
7 votes
1 answer
146 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 ...