Commit 2021-08-16 06:19 a983f241
View on Github →fix(*): fix universe levels (#8677)
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