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
12 votes
3 answers
257 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 ...
9 votes
1 answer
178 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 ...
5 votes
1 answer
139 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,037
4 votes
1 answer
113 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,037
4 votes
2 answers
151 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 ...
  • 896
2 votes
0 answers
65 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,037