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
9 votes
2 answers
367 views

Defining coercion for proof irrelevant equality

Say I would like to define coercion for proof irrelevant equality between types. In Coq I try ...
user avatar
  • 1,662
11 votes
3 answers
210 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 ...
user avatar
6 votes
1 answer
122 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 ...
user avatar