Universe constraints!

Stream: new members

[Gareth Ma]

I am struggling to understand what's going on here, or in general what's going on in the category theory files. I see a lot of universes labelled manually, sometimes some are equal, but an explanation would be great.. Here is the code

import Mathlib.Algebra.Category.Grp.Colimits

open Function CategoryTheory Category Limits

variable {G H : AddCommGrp} (f g : G ⟶ H)

open Group AddSubgroup

-- I need this cuz .mk' gives a →+ and type checker doesn't like it in place of ⟶
abbrev cocone_quotient_map : H ⟶ AddCommGrp.of (H ⧸ (f - g).range) :=
  QuotientAddGroup.mk' (AddMonoidHom.range (f - g))

-- Define the cocone over parallelPair f g
noncomputable def cocone_coequalizer : Cocone (parallelPair f g) where
  pt := AddCommGrp.of (H ⧸ (f - g).range)
  ι := {
    app := fun
      | .zero => f ≫ cocone_quotient_map f g
      | .one => cocone_quotient_map f g
    naturality := sorry
  }

[Gareth Ma]

For "I see a lot of universes labelled manually" I am thinking of these 5 lines, and also the HasColimitsOfSize HasColimits HasColimitsOfShape stuff

[Gareth Ma]

Error is simple but undecipherable:

▶ expected type (17:12-19:40)
G H : AddCommGrp
f g : G ⟶ H
⊢ (X : WalkingParallelPair) →
  (parallelPair f g).obj X ⟶
    ((Functor.const WalkingParallelPair).obj (AddCommGrp.of (↑H ⧸ AddMonoidHom.range (f - g)))).obj X

▶ 19:7-19:40: error:
stuck at solving universe constraint
  max ?u.4135 ?u.4136 =?= max ?u.3195 ?u.3826
while trying to unify
  Quiver.Hom.{(max ?u.4136 ?u.4135) + 1, (max ?u.4136 ?u.4135) + 1} G H : Type (max ?u.4136 ?u.4135)
with
  Quiver.Hom.{(max ?u.3826 ?u.3195) + 1, (max ?u.3826 ?u.3195) + 1} G H : Type (max ?u.3826 ?u.3195)

[Gareth Ma]

Update: Modifying G H by adding universe constraints manually fixes the error:

universe u
variable {G H : AddCommGrp.{u}} (f g : G ⟶ H)

However, this doesn't answer any questions. In fact I have more questions now, since G and H have to be of the same universe for the type check to work at all (objects in a category have to be in the same universe), so why is this .{u} needed

[Matthew Ballard]

Unifying level (universe) metavariables is fairly conservative currently and without specifying some universes explicitly you tend to have a lot of level metavariables floating around in the context. While a person can say "oh that's the solution I want", the code can't immediately jump to that case without ignoring other possibly valid solutions at a cost

[Gareth Ma]

Hmm so here Lean is just not trying hard enough to unify level/universes metavraiables? Does it mean I should try to add universe variables manually whenever I can (in category theory I guess)

[Kevin Buzzard]

Clearly max ?u.4135 ?u.4136 =?= max ?u.3195 ?u.3826 has got lots of solutions, I don't think it's a case of not trying hard enough, Lean can't read your mind. If you know which of those universes you want to be equal you're going to have to tell Lean explicitly, surely?

[Gareth Ma]

Maybe this is closer to what to universes not trying hard enough

image.png

[Gareth Ma]

https://gist.github.com/grhkm21/231f9bfcac11b7d9a57f985e957e49cd MRE (Maximal Reproducible Example)
Just load and scroll down

[Gareth Ma]

It seems that it is solved by replacing (J : Type) by (J : Type v_1). But then I realised (R : Type v_1) as well so now I need to use (J : Type v_2) :/

[Gareth Ma]

\- and that leads to another issue(ss), because of some category theory stuff (see TODO in FGModuleCat file)