Hi all, new to Discourse in general and this group in particular. I’ve known about Coq for years and played with it on and off, never done much serious development in it.

I recently learned about SProp and was particularly interested in its sigma types since I assume they would behave more like “real subsets”. But at the moment it looks like, short of reinventing the entire logic library in SProp, the only real way to put an interesting proposition into there is to ‘squash’ one from Prop. And having done so, I can’t find any way to actually make use of that proposition’s content.

For example: currently what I’d like to prove is that if a map `f: A -> B`

has a left-inverse, then its restriction to `Ssig (fun y:B => Squash (exists x:A, f x = y))`

has a full inverse. This seems to me like it ought to be the case given proof-irrelevance. Here’s how that’s going:

```
Variables A B: Type.
Variables (f: A -> B) (fInv: B -> A).
Hypothesis lcancel: forall x, fInv (f x) = x.
Definition Img: Type :=
Ssig (fun y:B => Squash (exists x, f x = y)).
Definition f' (x: A): Img :=
Sexists _ (f x) (squash (ex_intro _ _ eq_refl)).
Definition fInv' (y: Img): A := fInv (Spr1 y).
Property rcancel: forall y:Img, f' (fInv' y) = y.
Proof.
intros [y sH]. (* sH: Squash (exists x, f x = y) *)
apply Spr1_inj. now_show (f (fInv y) = y).
enough (exists x, f x = y).
{ destruct H; rewrite <- H, -> lcancel; reflexivity. }
```

…and here I’m stuck. I can’t destruct sH to get the proposition I need, because `"Case analysis on sort Prop is not allowed for inductive definition Squash."`

And without that proposition there is no way to complete the proof.

Based on this, I don’t understand how I am supposed to do anything at all with a value of type `Squash P`

except admire it and then throw it away. I suppose if I just wanted a computation to *require* that some value satisfy a predicate while never actually needing to *use* that fact, I could accept a `Squash (P x)`

for that purpose, but that’s about it. Is this analysis correct, or am I missing something?