New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - refactor: move morphisms in StructuredArrow to a lower universe #6397
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In general I think that this is probably the right approach; I think it's good to have a bit more control over exactly which universes you're allowing limits over rather than just announcing [HasLimits X]
.
I also believe this is a nice improvement. Thanks! bors merge |
This PR changes the definition ```lean abbrev fromPUnit (X : C) : Discrete PUnit.{v + 1} ⥤ C := (Functor.const _).obj X ``` to ```lean abbrev fromPUnit (X : C) : Discrete PUnit.{w + 1} ⥤ C := (Functor.const _).obj X ``` and then redefines ```lean def StructuredArrow (S : D) (T : C ⥤ D) := Comma (Functor.fromPUnit S) T ``` to ```lean 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.
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
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
to
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 ofStructuredArrow S T
no longer live inmax v₁ v₂
, but inv₁
, 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 ofStructuredArrow
live inv₁
. Luckily, by now it is possible to state everything correctly, and this PR adjustsLimits/Comma.lean
andLimits/Over.lean
accordingly.