Questions tagged [prop]
A sort of definitionally proof-irrelevant propositions introduced in "Definitional Proof-Irrelevance without K" and implemented by Agda (as Prop) and Coq (as SProp).
8
questions
1
vote
1
answer
39
views
Coq Induction on Hypothesis destroys the Hypothesis
I'm trying to prove something in coq
I have and Inductive prop type named in_order_merge which is a relation between three lists that shows third one is in_order merge of first two, here is the ...
5
votes
0
answers
78
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,424
2
votes
0
answers
86
views
Is there a good demonstration of bidirectional type checking with strict Prop?
I've seen elaboration-zoo, pi-forall, Mini-TT, etc., all kinds of demonstrations of dependent type elaboration. However, none of them support Prop.
I am interested ...
- 5,424
5
votes
1
answer
160
views
Why can termination checker affect strict Prop in Agda?
In https://dl.acm.org/doi/10.1145/3290316 section 4 (which I believe is a standard reference), the authors claimed that Voevodsky's propositional resizing rule justifies the consistency of an ...
- 5,424
4
votes
1
answer
128
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,424
4
votes
2
answers
155
views
Turning off some sProp checks
In Definitional Proof Irrelevance Without K, inductives in sProp need to satisfy three conditions to allow large elimination:
(1) Every non-forced argument must be in sProp.
(2) The return types of ...
- 906
9
votes
1
answer
220
views
How does Prop relate to h-prop and double negation?
I'm referring to these concepts:
Prop in Agda and SProp in Coq, a "sort of definitionally proof-irrelevant propositions", and their squash type (and relatedly, the usual Prop in Coq);
mere ...
- 983
12
votes
3
answers
281
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 ...
- 983