Commit 2023-03-02 21:24 3ea0b020

View on Github →

feat: port/CategoryTheory.Limits.Yoneda (#2381)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Yoneda.lean

added def CategoryTheory.Coyoneda.colimitCocone

added def CategoryTheory.Coyoneda.colimitCoconeIsColimit

added def CategoryTheory.coyonedaJointlyReflectsLimits

added def CategoryTheory.yonedaJointlyReflectsLimits