Kernel error with category theory and aesop_cat

Stream: mathlib4

[Gareth Ma]

In the proof below, when I replace the proof of hom_inv_id by := by aesop_cat (or omitting the field), I get a Lean kernel error (test online). Any idea why? It seems there are some size issues :/

import Mathlib

open CategoryTheory Category Limits Functor

variable
  {C D E : Type u} [Category C] [Category D] [Category E]
  {F : C ⥤ E} {K : C ⥤ D} (R : D ⥤ E) (ε : K ⋙ R ⟶ F)
  [R.IsRightKanExtension ε]

lemma CategoryTheory.Functor.liftOfIsRightKanExtension_existsUnique (G : D ⥤ E) (β : K ⋙ G ⟶ F) :
    ∃! η, whiskerLeft K η ≫ ε = β :=
  (R.isUniversalOfIsRightKanExtension ε).existsUnique (RightExtension.mk G β)

noncomputable def homEquivOfIsRightKanExtension' :
    yoneda.obj R ≅ ((whiskeringLeft C D E).obj K).op ⋙ yoneda.obj F where
  hom := {
    app := fun G ↦ (R.homEquivOfIsRightKanExtension ε G.unop).toFun
    naturality := by
      unfold homEquivOfIsRightKanExtension
      aesop_cat
  }
  inv := {
    app := fun G ↦ (R.homEquivOfIsRightKanExtension ε G.unop).invFun
    naturality := fun _ _ _ ↦ by
      ext1 δ
      unfold homEquivOfIsRightKanExtension
      exact (liftOfIsRightKanExtension_existsUnique ..).unique
        (liftOfIsRightKanExtension_fac ..) (by aesop_cat)
  }
  hom_inv_id := by ext; simp
  inv_hom_id := by ext; simp

[Gareth Ma]

Wait, no error with aesop

[Aaron Liu]

My guess is universe metavariables

[Gareth Ma]

But I made everything Type u already

[Gareth Ma]

Oh do I have to specify universes of morphisms as well or something

[Aaron Liu]

But you didn't make them all Category.{v}

[Gareth Ma]

Okay yeah that fixes it

[Kenny Lau]

Note that specifying the universes fixes it:

import Mathlib

open CategoryTheory Category Limits Functor
universe v₁ v₂ v₃ u

variable
  {C D E : Type u} [Category.{v₁} C] [Category.{v₂} D] [Category.{v₃} E]
  {F : C ⥤ E} {K : C ⥤ D} (R : D ⥤ E) (ε : K ⋙ R ⟶ F)
  [R.IsRightKanExtension ε]

lemma CategoryTheory.Functor.liftOfIsRightKanExtension_existsUnique (G : D ⥤ E) (β : K ⋙ G ⟶ F) :
    ∃! η, whiskerLeft K η ≫ ε = β :=
  (R.isUniversalOfIsRightKanExtension ε).existsUnique (RightExtension.mk G β)

noncomputable def homEquivOfIsRightKanExtension' :
    yoneda.obj R ≅ ((whiskeringLeft C D E).obj K).op ⋙ yoneda.obj F where
  hom := {
    app := fun G ↦ (R.homEquivOfIsRightKanExtension ε G.unop).toFun
    naturality := by
      unfold homEquivOfIsRightKanExtension
      aesop_cat
  }
  inv := {
    app := fun G ↦ (R.homEquivOfIsRightKanExtension ε G.unop).invFun
    naturality := fun _ _ _ ↦ by
      ext1 δ
      unfold homEquivOfIsRightKanExtension
      exact (liftOfIsRightKanExtension_existsUnique ..).unique
        (liftOfIsRightKanExtension_fac ..) (by aesop_cat)
  }
  hom_inv_id := by aesop_cat
  inv_hom_id := by ext; simp

[Kenny Lau]

do the u's have to be the same?

[Gareth Ma]

It seems to complain if not

[Kenny Lau]

basically you always want to remember the idiom [Category.{v} C]

[Kenny Lau]

that will keep you out of troubles

[Gareth Ma]

Right but that's so confusing, in your code your v are all different

[Gareth Ma]

How's that different from omitting them

[Kenny Lau]

Lean universe is magic

[Aaron Liu]

Gareth Ma said:

How's that different from omitting them

You don't get to set v = u

[Aaron Liu]

but if you omit them then it can be anything (including u)

[Kenny Lau]

and also max (max (v1+1) (v2+2)) (u+37)

[Gareth Ma]

ummmm hmmm okay