Commit 2024-10-25 22:10 4d9990b3

View on Github →

feat(CategoryTheory/Limits/Final): Add pointfree version of Final.colimitIso (#17902)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Final.lean

added def CategoryTheory.Functor.Final.colimIso

deleted def CategoryTheory.Functor.Final.colimitIso'

added def CategoryTheory.Functor.Initial.limIso

deleted def CategoryTheory.Functor.Initial.limitIso'