WildCat Equiv.compose_cate can't compose maps between different universes

[jdchristensen]

pequiv_compose (aka o*E) is defined using Equiv.compose_cate ($oE) which means it can't compose things in different universes. It's trivial to redefine o*E to make this work. But is there a way to make the WildCat framework able to handle this? It would be great if we could use WildCat more often, but we also need fundamental operations like this to be sufficiently polymorphic.

(The universe w is an artefact of ->* being defined in terms of pForall, which requires an extra universe variable above everything else.)

Require Import Basics Types Pointed.
Local Open Scope pointed_scope.

Set Printing Universes.

Definition test@{u v w | u < v, v < w} {A : pType@{u}} {B C : pType@{v}}
           (f : pEquiv@{u v w} A B) (g : pEquiv@{v v w} B C) : pEquiv@{u v w} A C.
Proof.
  Fail exact (g o*E f).
  Fail Check (g o*E f).
  srapply (Build_pEquiv _ _ (g o* f)).
Defined.

[mikeshulman]

It seems that to make this work, each individual wildcat instance would have to be universe-polymorphic. The only way to do that would be to make them modules that implement a module type, the way we used to do with modalities, rather than instances of a typeclass, and that's seriously annoying for other reasons.

[jdchristensen]

I suspected that would be the answer. So I think I'll redefine pequiv_compose.

[Alizter]

Are the wildcat instances not universe polymorphic today? I'm not sure I follow. In any case, whatever Coq is lacking we should definitely clarify so that we can report it upstream. I and the other devs would be interested in supporting such use cases.

[jdchristensen]

Actually, making pEquiv into a Cumulative Record makes this problem go away!

[mikeshulman]

@Alizter Sorry, that wasn't phrased very well. I meant that the fields of a wild category would have to be individually universe-polymorphic.

[Alizter]

@jdchristensen I think we should try to use cumulativity as much as possible.

[jdchristensen]

Rats, even with pEquiv marked as cumulative, the following still doesn't work. I'm out of ideas and will just redefine pequiv_compose unless someone else has an idea.

Definition test2@{u v w | u < v, v < w} {A B : pType@{v}} {C : pType@{u}}
           (f : pEquiv@{v v w} A B) (g : pEquiv@{v u w} B C) : pEquiv@{v u w} A C.
Proof.
  Fail exact (g o*E f).
  exact (Build_pEquiv _ _ (g o* f) _).
Defined.

[jarlg]

It's puzzling to me that marking pEquiv cumulative solved the problem above, but that that this still fails. Do you have any idea why?

[jdchristensen]

No, I don't understand why. And I don't really understand why the first test does work.

[jdchristensen]

The issue is that even with pEquiv marked as Cumulative, the universe variable u0 is marked as "invariant", as indicated by the = beside it:

Record
pEquiv@{u u0 u1} (A : pType@{u}) (B : pType@{u0})
  : Type@{max(u,u0)} := Build_pEquiv
  { pointed_equiv_fun : A ->* B;
    pointed_isequiv : IsEquiv@{u u0} pointed_equiv_fun }.
(* *u =u0 =u1 |= u0 < u1
                 u <= u1 *)

Both pForall and IsEquiv are cumulative with "irrelevant" universe variables (the most flexible kind), so I'm not sure why Coq doesn't let u0 be irrelevant as well.

[Alizter]

@jdchristensen you should be able to explicitly annotate the relevences yourself.

[jdchristensen]

@Alizter I tried that, but it doesn't let me make u0 weaker than invariant.

[jdchristensen]

I found a way to add a fourth universe variable to pEquiv which then makes u and u0 irrelevant. Then test2 works. But things still fail in the real spot where I want to compose pointed equivalences, probably because of differences in u1 and the new universe variable, which are both invariant. So this doesn't really solve the problem.

If A ->* B is defined directly, rather than as a special case of pForall, then everything works out great:

Cumulative Record pMap (A : pType) (B : pType) := {
  pointed_fun : A -> B;
  point_eq : pointed_fun pt = pt
}.

Coercion pointed_fun : pMap >-> Funclass.

Cumulative Record newpEquiv (A : pType) (B : pType) := {
  pointed_equiv_fun : pMap A B;
  pointed_isequiv : IsEquiv pointed_equiv_fun
}.

Now newpEquiv only has two universe variables, and they are both irrelevant. There are other places in the library where having ->* defined using pForall complicates things (at least visually), but it's also beneficial to only have to prove various facts about pointed maps once. And I imagine it might be a fair bit of work to change the definition at this point.

So I'm still leaning towards merging #1706.

[jarlg]

I think we should try defining pMap directly, like you did above, if only because it lets us get rid of an unnecessary universe variable in lots of places. I'm inclined to define a coercion pMap >-> pForall though. You then get a coercion to Funclass via the one for pForall. It's only going to get harder to make a change like this, so I think it's worth trying out...

[jdchristensen]

I think I'll first merge #1706, and then someone can take their time thinking about how to redo pMap and see if it works out.

[jdchristensen]

For the record, this issue was solved by #1708.