linter.checkUnivs triggers for `BundledGFunctors` and other definitions.

[ayhon]

When upgrading from v4.31.0 to v4.32.0, a new linter checkUnivs started to trigger for various definitions in Iris Lean, in particular that of BundledGFunctors. The linter complains that, although BundledGFunctors is polymorphic over three universes, it is only ever used in situations where all universes are the same. In #514 we opted to simply disable the linter for these definitions, however it might be worth considering whether it makes sense to change the definitions so they don't require more universes than usual.

The definitions which trigger this linter are:

1. BundledGFunctors, GFunctor and OFunctorPre, all because of OFunctorPre
2. Std.PartialMap.zip
3. Iris/Std/Prod.lean:mapAllM

[ayhon]

The situation for (1) is the one I'm most unsure about, for (2) I think it makes sense to require that the types of values of the maps passed to Std.PartialMap.zip are the same, and for (3) I believe it's a definition that we're not using anywhere else, and that we could delete.

For context, this is the current signature of Std.PartialMap.zip. Both V and V' already share the same universe max u_2 u_3, calling it u instead should make no difference.

Iris.Std.PartialMap.zip.{u_1, u_2, u_3, u_4} {K : Type u_1} {V : Type (max u_2 u_3)} {M : Type (max u_2 u_3) → Type u_4}
  [PartialMap M K] {V' : Type (max u_2 u_3)} (m₁ : M V) (m₂ : M V') : M (V × V')