Commit 2023-08-28 21:38 7499ee49
View on Github →refactor: move morphisms in StructuredArrow to a lower universe (#6397) This PR changes the definition
abbrev fromPUnit (X : C) : Discrete PUnit.{v + 1} ⥤ C :=
(Functor.const _).obj X
to
abbrev fromPUnit (X : C) : Discrete PUnit.{w + 1} ⥤ C :=
(Functor.const _).obj X
and then redefines
def StructuredArrow (S : D) (T : C ⥤ D) :=
Comma (Functor.fromPUnit S) T
to
def StructuredArrow (S : D) (T : C ⥤ D) :=
Comma (Functor.fromPUnit.{0} S) T
The effect of this is that given {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] (S : D) (T : C ⥤ D), the morphisms of StructuredArrow S T no longer live in max v₁ v₂, but in v₁, as they should. Thus, this PR is basically a better version of #6388.
My guess for why we used to have the larger universe is that back in the day, the universes for limits were much more restricted, so stating the results of Limits/Comma.lean was not possible if the morphisms of StructuredArrow live in v₁. Luckily, by now it is possible to state everything correctly, and this PR adjusts Limits/Comma.lean and Limits/Over.lean accordingly.