Commit 2023-04-27 08:42 ea1dfb2d

View on Github →

chore: use TypeMax in CategoryTheory.Limits.Types (#3653) Per discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.233463.20universe.20constraint.20issues

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Types.lean

modified theorem CategoryTheory.Limits.Types.productIso_hom_comp_eval

modified theorem CategoryTheory.Limits.Types.productIso_inv_comp_π

Modified Mathlib/CategoryTheory/Limits/Types.lean

modified theorem CategoryTheory.Limits.Types.Colimit.w_apply

modified theorem CategoryTheory.Limits.Types.Colimit.ι_desc_apply

modified theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply

modified theorem CategoryTheory.Limits.Types.FilteredColimit.eqvGen_quot_rel_of_rel

modified theorem CategoryTheory.Limits.Types.FilteredColimit.rel_of_quot_rel

modified theorem CategoryTheory.Limits.Types.Limit.lift_π_apply

modified theorem CategoryTheory.Limits.Types.Limit.map_π_apply'

modified theorem CategoryTheory.Limits.Types.Limit.map_π_apply

modified theorem CategoryTheory.Limits.Types.Limit.w_apply'

modified theorem CategoryTheory.Limits.Types.Limit.w_apply

modified theorem CategoryTheory.Limits.Types.Limit.π_mk

modified def CategoryTheory.Limits.Types.Quot.Rel

modified def CategoryTheory.Limits.Types.Quot

modified def CategoryTheory.Limits.Types.colimitCocone

modified def CategoryTheory.Limits.Types.colimitCoconeIsColimit

modified theorem CategoryTheory.Limits.Types.colimitEquivQuot_apply

modified theorem CategoryTheory.Limits.Types.colimitEquivQuot_symm_apply

modified theorem CategoryTheory.Limits.Types.colimit_eq

modified theorem CategoryTheory.Limits.Types.colimit_sound'

modified theorem CategoryTheory.Limits.Types.colimit_sound

modified def CategoryTheory.Limits.Types.isLimitEquivSections

modified theorem CategoryTheory.Limits.Types.isLimitEquivSections_apply

modified theorem CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply

modified theorem CategoryTheory.Limits.Types.jointly_surjective'

modified theorem CategoryTheory.Limits.Types.jointly_surjective

modified def CategoryTheory.Limits.Types.limitCone

modified def CategoryTheory.Limits.Types.limitConeIsLimit

modified theorem CategoryTheory.Limits.Types.limitEquivSections_apply

modified theorem CategoryTheory.Limits.Types.limitEquivSections_symm_apply

modified theorem CategoryTheory.Limits.Types.limit_ext'

modified theorem CategoryTheory.Limits.Types.limit_ext

modified theorem CategoryTheory.Limits.Types.limit_ext_iff'

modified theorem CategoryTheory.Limits.Types.limit_ext_iff

Created Mathlib/Data/TypeMax.lean