Commit 2023-07-07 04:28 56112d4c

View on Github →

feat: using UnivLE in constructing limits in Type (#5724)

Estimated changes

Modified Mathlib/Algebra/Category/GroupCat/Limits.lean

Modified Mathlib/Algebra/Category/MonCat/Limits.lean

deleted def MonCat.HasLimits.limitCone

deleted def MonCat.HasLimits.limitConeIsLimit

deleted def MonCat.limitπMonoidHom

Modified Mathlib/CategoryTheory/Closed/Types.lean

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

added theorem CategoryTheory.Limits.Types.UnivLE.productIso_hom_comp_eval

added theorem CategoryTheory.Limits.Types.UnivLE.productIso_hom_comp_eval_apply

added theorem CategoryTheory.Limits.Types.UnivLE.productIso_inv_comp_π

modified theorem CategoryTheory.Limits.Types.pi_lift_π_apply

modified theorem CategoryTheory.Limits.Types.pi_map_π_apply

Modified Mathlib/CategoryTheory/Limits/Types.lean

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

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

modified theorem CategoryTheory.Limits.Types.Limit.w_apply

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

added theorem CategoryTheory.Limits.Types.UnivLE.limitCone_pt_ext

deleted def CategoryTheory.Limits.Types.isLimitEquivSections

modified theorem CategoryTheory.Limits.Types.isLimitEquivSections_apply

modified theorem CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply

deleted def CategoryTheory.Limits.Types.limitCone

deleted 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_iff

Modified Mathlib/CategoryTheory/Sites/SheafOfTypes.lean

Modified Mathlib/Logic/Small/Basic.lean

added theorem Shrink.ext