[Merged by Bors] - fix(*): fix universe levels #8677
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
fpvandoorn
added
the
awaiting-review
|
Did you make a linter for this to find all these? Because that would be amazing. |
|
Yes, but it's not ready for mathlib yet. See my comment in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/crazy.20universe |
1 task
eric-wieser
reviewed
Aug 15, 2021
| @@ -300,7 +300,7 @@ open quotient_add_group | |||
| The categorical cokernel of a morphism in `AddCommGroup` | |||
| agrees with the usual group-theoretical quotient. | |||
| -/ | |||
| noncomputable def cokernel_iso_quotient {G H : AddCommGroup} (f : G ⟶ H) : | |||
| noncomputable def cokernel_iso_quotient {G H : AddCommGroup.{u}} (f : G ⟶ H) : | |||
There was a problem hiding this comment.
Are G and H not allowed to reside in different universes?
There was a problem hiding this comment.
no, G ⟶ H is only defined when G and H are in the same category, so they must have the same type (including universe level)
eric-wieser
reviewed
Aug 15, 2021
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
This is great, @fpvandoorn! With the linting coming along soon, let's get this merged. bors merge |
github-actions
bot
added
ready-to-merge
|
Canceled. |
github-actions
bot
removed
the
merge-conflict
|
can I bors r- this myself? Or was that automatic? I think someone else has to bors r+ it again? @semorrison |
fpvandoorn
added
awaiting-review
|
Pushing a commit to an already r+'d PR automatically cancels it. |
|
bors merge |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Aug 16, 2021
The universe levels in the following declarations have been fixed . This means that there was an argument of the form `Type (max u v)` or `Sort (max u v)`, which could be generalized to `Type u` or `Sort u`. In a few cases, I made explicit that there is a universe restriction (sometimes `max u v` is legitimately used as an arbitrary universe level higher than `u`) In some files I also cleaned up some declarations around these. ``` algebraic_geometry.Spec.SheafedSpace_map algebraic_geometry.Spec.to_SheafedSpace algebraic_geometry.Spec.to_PresheafedSpace category_theory.discrete_is_connected_equiv_punit writer_t.uliftable' writer_t.uliftable equiv.prod_equiv_of_equiv_nat free_algebra.dim_eq linear_equiv.alg_conj module.flat cardinal.add_def slim_check.injective_function.mk topological_add_group.of_nhds_zero' topological_group.of_nhds_one' topological_group.of_comm_of_nhds_one topological_add_group.of_comm_of_nhds_zero has_continuous_mul.of_nhds_one has_continuous_add.of_nhds_zero has_continuous_add_of_comm_of_nhds_zero has_continuous_mul_of_comm_of_nhds_one uniform_space_of_compact_t2 AddCommGroup.cokernel_iso_quotient algebraic_geometry.Scheme algebraic_geometry.Scheme.Spec_obj simplex_category.skeletal_functor category_theory.Type_to_Cat.full CommMon_.equiv_lax_braided_functor_punit.lax_braided_to_CommMon CommMon_.equiv_lax_braided_functor_punit.unit_iso Mon_.equiv_lax_monoidal_functor_punit.lax_monoidal_to_Mon Mon_.equiv_lax_monoidal_functor_punit.unit_iso uliftable.down_map weak_dual.has_continuous_smul stone_cech_equivalence Compactum_to_CompHaus.full TopCommRing.category_theory.forget₂.category_theory.reflects_isomorphisms ``` Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The universe levels in the following declarations have been fixed .
This means that there was an argument of the form
Type (max u v)orSort (max u v), which could be generalized toType uorSort u. In a few cases, I made explicit that there is a universe restriction (sometimesmax u vis legitimately used as an arbitrary universe level higher thanu)In some files I also cleaned up some declarations around these.
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/crazy.20universe