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

10 questions
Filter by
Sorted by
Tagged with
96 views

### Coq's elimination restriction corner cases -- when can you eliminate Prop's into Type?

In order to ensure soundness, and to keep axioms like proof irrelevance admissible, Coq has an "elimination restriction" on inductive types in Prop. ...
225 views

### Pattern matching from Prop to Type in Lean

I'm a beginner in the world of proof assistants, and have been taking a look at Lean4 lately. I wanted to write a function like ...
1 vote
69 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 ...
147 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,877
96 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,877
184 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,877
151 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,877
167 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
314 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 ...
• 1,015