universe issue

Stream: mathlib4

[Joël Riou]

In the following code (which is https://github.com/leanprover-community/mathlib4/pull/2712/files#diff-bdf99f608dbfa1aa55eb2722832ecc408e6c92d8ff93cea9c45cce42e0ff0b84R102-R119 from !4#2712), some instances cannot be inferred, like HasLimit F for a functor J ⥤ Type max v u (where J : Type v is a small category). Even if I define this instance explicitly (as test), the instance of HasLimit F is not found in the definition limitEquivSections. It is however found if u=v, see limitEquivSections_test.

instance test (F : J ⥤ Type max v u) : HasLimit F :=
  (Types.hasLimitsOfSize.{v, u}.has_limits_of_shape J).has_limit F

instance (F : J ⥤ Type v) : HasLimit F :=
  test.{v, v} F

/-- The equivalence between the abstract limit of `F` in `Type u`
and the "concrete" definition as the sections of `F`.
-/
noncomputable def limitEquivSections (F : J ⥤ Type max v u) :
    (limit F : Type max v u) ≃ F.sections :=
  isLimitEquivSections.{v, u} (limit.isLimit F)
#align category_theory.limits.types.limit_equiv_sections CategoryTheory.Limits.Types.limitEquivSections

-- the following works
noncomputable def limitEquivSections_test (F : J ⥤ Type v) :
    (limit F : Type v) ≃ F.sections :=
  isLimitEquivSections.{v, v} (limit.isLimit F)

I do not know how to fix this apart from adding everywhere [HasLimit F] as an assumption.

[Matthew Ballard]

In similar situations I had to do a haveI after the colon.

[Joël Riou]

Thanks! Indeed, the following works:

instance hasLimit (F : J ⥤ Type max v u) : HasLimit F :=
  (Types.hasLimitsOfSize.{v, u}.has_limits_of_shape J).has_limit F

noncomputable def limitEquivSections (F : J ⥤ Type max v u) :
  (@limit _ _ _ _ F (hasLimit.{v, u} F) : Type max v u) ≃ F.sections :=
  haveI := (hasLimit.{v, u} F); isLimitEquivSections.{v, u} (limit.isLimit F)

[Matthew Ballard]

And I am doing this right now because of Function.comp...

[Adam Topaz]

Are we going to have to use haveI whenever we do anything with limits now? That doesn't seem good.

[Adam Topaz]

I still have mixed feelings about allowing arbitrary universes in the indexing categories for (co)limits. It seems to me that this was causing too many issues to be worthwhile even in lean3, and maybe things are even worse in lean4?

[Matthew Ballard]

I don't think it is universes. It is computation inside the limit classes generally

[Joël Riou]

Adam Topaz said:

I still have mixed feelings about allowing arbitrary universes in the indexing categories for (co)limits. It seems to me that this was causing too many issues to be worthwhile even in lean3, and maybe things are even worse in lean4?

I am not sure it will be such a problem, apart from a few API files. For example, the following works fine:

example {J : Type} [Category.{0} J] (F : J ⥤ Type u) :
  HasColimit F := by infer_instance

example {J : Type} [Category.{0} J] (F : J ⥤ Type u) :
  HasLimit F := by infer_instance

[Adam Topaz]

Okay, so maybe it's only as bad as it was in lean3 :)

[Matthew Ballard]

Was max or \circ a problem there?

[Joël Riou]

It seems the problem was with max.

[Matthew Ballard]

Sorry, I meant could Lean 3 handle max or Function.comp in these places?

[Johan Commelin]

feat: port CategoryTheory.Limits.Types !4#2712

This PR adds a lot of haveIs. Are we happy with that? Should there be an issue for this?
@Joël Riou you seem to think that this haveI-issue is only restricted to a few files, right? So maybe we can just move along?

[Eric Wieser]

Is this an eta thing?

[Joël Riou]

Johan Commelin said:

Joël Riou you seem to think that this haveI-issue is only restricted to a few files, right?

I would speculate that the problem was specific to limits in Type. For standard bundled categories (those in algebra/category), only one universe will appear, so that there should be less problems.

[Chris Hughes]

Universe unification does seem to have got much worse in Lean4. I might open an issue about it.