Skip to main content
9 votes
Accepted

Is 'subsingleton elimination' the same concept as 'function comprehension'?

Indeed, these two notions are about what we allow to eliminate from Prop to Type, and they both roughly follow the idea that &...
Meven Lennon-Bertrand's user avatar
8 votes
Accepted

Why is `--irrelevant-projections` unsafe in Agda?

--irrelevant-projections can be used to prove the irrelevance axiom mentioned in the Agda manual: ...
James Martin's user avatar
  • 1,035
6 votes

Why does it matter if canonicity holds for irrelevant types?

Consider the following type theory: \begin{gather} \frac{ }{\vdash G \; \mathsf{type}} \qquad \frac{ }{\vdash \Lambda \; \mathsf{type}} \\[2ex] \frac{\vdash g : G \qquad \vdash e_1 : \Lambda \qquad \...
Andrej Bauer's user avatar
  • 9,593
5 votes

Defining coercion for proof irrelevant equality

In the latest versions of Coq, you can use an irrelevant equality, and eliminate it into Set/Type, see the reference manual. You ...
Meven Lennon-Bertrand's user avatar
5 votes
Accepted

Defining coercion for proof irrelevant equality

Agda has a runtime irrelevance modality which may be closer to what you want. In particular, since there's only one constructor, it is ok to eliminate the identity type even if it is marked irrelevant....
Trebor's user avatar
  • 4,015
5 votes
Accepted

Why does it matter if canonicity holds for irrelevant types?

I will focus here on a universe of definitionally irrelevant types; let's call it SProp. In short, we can postulate any consistent SProp axiom, without breaking any constructive metatheoretic property....
András Kovács's user avatar
4 votes

Why does it matter if canonicity holds for irrelevant types?

One answer is that (judgmental) proof irrelevance does not correspond to computational irrelevance. Proof irrelevance means that every proof is equal in some sense. But that doesn't mean the values ...
Dan Doel's user avatar
  • 982
1 vote

Use proof irrelevance in cast

It is indeed possible, but not so easy to build infrastructure to do. I'd suggest you have a look at MathComp's subType class, and how it organizes the set of ...
ejgallego's user avatar
  • 151

Only top scored, non community-wiki answers of a minimum length are eligible