Commit 2023-03-13 12:12 746b3386

View on Github →

feat: port CategoryTheory.Category.Cat.Limit (#2834)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Category/Cat.lean

Created Mathlib/CategoryTheory/Category/Cat/Limit.lean

added def CategoryTheory.Cat.HasLimits.homDiagram

added def CategoryTheory.Cat.HasLimits.limitCone

added def CategoryTheory.Cat.HasLimits.limitConeIsLimit

added def CategoryTheory.Cat.HasLimits.limitConeLift

added def CategoryTheory.Cat.HasLimits.limitConeX

added theorem CategoryTheory.Cat.HasLimits.limit_π_homDiagram_eqToHom

Modified Mathlib/CategoryTheory/Limits/Types.lean