make pEquiv Cumulative and pequiv_compose more polymorphic

[jdchristensen]

See the discussion and examples in #1703.

[jarlg]

After this change, does pequiv_compose still unify with $oE when the latter makes sense? It seems it would be good if we could achieve that, even if we don't use the wildcat instance of pType much at the moment.

[jdchristensen]

After this change, does pequiv_compose still unify with $oE when the latter makes sense? It seems it would be good if we could achieve that, even if we don't use the wildcat instance of pType much at the moment.

No, they don't unify. The proofs of isequiv_compose in Basics/Equivalences and compose_cate in WildCat/Equiv are different. The proofs of the section property and retraction property are different, and in addition, compose_cate uses isequiv_adjointify, while isequiv_compose gives a direct proof without any rewriting. It's likely that these two could be unified, but I'm not sure it's worth fiddling with. In this case, the WildCat proof ends up with lots of extra reflexivity paths; isequiv_compose can make use of the fact that function composition is strictly associative and unital, while WildCat can't assume that. So if they were unified, then isequiv_compose would have to always insert extra reflexivity paths, which would be annoying.

[jarlg]

Makes sense. Thanks for the analysis!

[jdchristensen]

Merging this. If ->* is redefined to avoid using pForall, then pequiv_compose can probably be changed back to being defined using $oE.