The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Hi,

I'd think so. You can define a constant PE' with the same type as PE that is based on EP, and prove this PE' commutes with EP:

Definition PE' n : P (E n) = n.
rewrite <- (PE n).
apply (f_equal P).
apply EP.
Defined.

Lemma comm x : f_equal P (EP x) = PE' (P x).

<proof not trivial but doable>

So we get the good notion of equivalence.

If you replace PE by PE' in the rest of scripts, you should be able to finish the proof, which I haven't checked.

Bruno.

---

De: "Jason Gross" <jasongross9 AT gmail.com>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Vendredi 18 Décembre 2015 17:57:25
Objet: Re: [Coq-Club] Dependent Type Problem

You should be able to do it for other (non-hset) types by "adjusting" the isomorphism into a good notion of equivalence, and using that instead, right?

-Jason