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).

Filter by
Sorted by
Tagged with
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 ...
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 ...