Stack Exchange Network
Stack Exchange network consists of 181 Q&A communities including
Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
Visit Stack Exchange
A sort of definitionally proof-irrelevant propositions introduced in "Definitional Proof-Irrelevance without K" and implemented by Agda (as Prop) and Coq (as SProp).
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 ...
I understand proof irrelevance implementation as one of the two language features listed below:
Prop as SProp in Coq or ...
I've seen elaboration-zoo, pi-forall, Mini-TT, etc., all kinds of demonstrations of dependent type elaboration. However, none of them support
I am interested ...
Nov 17, 2022 at 4:15
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 ...
Oct 26, 2022 at 7:25
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 ...
Sep 19, 2022 at 17:23
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 ...
May 1, 2022 at 18:41
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);
Mar 25, 2022 at 19:20
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 ...
Mar 6, 2022 at 3:32
By clicking “Accept all cookies”, you agree Stack Exchange can store cookies on your device and disclose information in accordance with our
Accept all cookies
Necessary cookies only