```
From HoTT Require Import Basics.
Section StrictProp.
Context (P Q : SProp).
Context (P_to_Q : forall _ : P, Q).
Context (Q_to_P : forall _: Q, P).
Definition PQ_Equiv : IsEquiv P_to_Q.
Proof.
unshelve eapply Build_IsEquiv.
- exact Q_to_P.
- intro x.
(* Prove P_to_Q (Q_to_P x) = x *)
reflexivity.
```

I think the proof of reflexivity should succeed, but I get the error message

```
Unable to unify "x" with "P_to_Q (Q_to_P x)".
```

This is surprising as SProp has definitional proof irrelevance.

Now in this example I have not assumed cumulative universe checking, which is a problem as an IsEquiv is only defined between two types. So I should expect some kind of error eventually. But it doesn't make sense to me why I should get a unification error.

If I do add the assumption of cumulativity I still get the error. Now maybe I can chalk that up to the warning that typechecking is not complete if cumulativity is assumed.

If I prove `forall (x : Q), x = P_to_Q (Q_to_P x)`

as a lemma on its own, I can prove it by reflexivity and then I can use that lemma later.

Also when the documentation says "Status of SProp is experimental In particular, conversion checking through bytecode or native code compilation currently does not understand proof irrelevance." To my understanding there are two versions of Coqc and Coqctop, one is the bytecode version and one is the native code compilation version, so this error messages reads to me something like "In particular, conversion checking in Coq does not understand proof irrelevance."

It would be helpful to say what works in SProp.

The "two versions of coqc/coqtop" issue should be orthogonal, that text is most likely talking about the vm_compute and native_compute tactics

I tried to minimize it and got an anomaly which i reported on the issue tracker

Ok, I talked to Gaetan Gilbert on the Github issue tracker and he said that this is to be expected as part of how Cumulative SProp works, I guess that typechecking /unification is undecidable in general if this flag is enabled but are there any positive guidelines which suggest when we should be able to unify?

https://coq.github.io/doc/master/refman/addendum/sprop.html#issues-with-non-cumulativity

the "The implementation of proof irrelevance uses inferred "relevance" marks on binders to determine which variables are irrelevant. " paragraph

any use of cumulativity which makes a binder change proof relevance status will stop coq from considering that variable irrelevant

Last updated: Jun 25 2024 at 18:02 UTC