Commit 2025-03-01 17:18 b5719fa2

View on Github →

feat: TypeMax is no longer needed (#22418)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Limits/Indization/IndObject.lean

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

modified def CategoryTheory.Limits.Types.coproductColimitCocone

modified theorem CategoryTheory.Limits.Types.coproductIso_mk_comp_inv

modified theorem CategoryTheory.Limits.Types.coproductIso_ι_comp_hom

modified theorem CategoryTheory.Limits.Types.productIso_hom_comp_eval

modified theorem CategoryTheory.Limits.Types.productIso_hom_comp_eval_apply

modified theorem CategoryTheory.Limits.Types.productIso_inv_comp_π

modified def CategoryTheory.Limits.Types.productLimitCone

Modified Mathlib/CategoryTheory/Limits/Types.lean

modified def CategoryTheory.Limits.Types.TypeMax.colimitCocone

modified def CategoryTheory.Limits.Types.TypeMax.colimitCoconeIsColimit

Deleted Mathlib/Data/TypeMax.lean

Modified Mathlib/Geometry/RingedSpace/Basic.lean