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
4 votes
1 answer
79 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 ...
  • 4,750
4 votes
2 answers
148 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
9 votes
1 answer
150 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
244 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 ...