Commit 2023-11-18 09:34 af527f21

View on Github →

chore: make fullyFaithfulReflects(Co)Limits instances (#8462)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Preserves/Basic.lean

deleted def CategoryTheory.Limits.fullyFaithfulReflectsColimits

deleted def CategoryTheory.Limits.fullyFaithfulReflectsLimits

Modified Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Basic.lean

Modified Mathlib/CategoryTheory/Limits/Yoneda.lean

Modified Mathlib/Topology/Category/CompHaus/Limits.lean

Modified Mathlib/Topology/Category/Profinite/Basic.lean

Modified Mathlib/Topology/Category/Profinite/Limits.lean

Modified Mathlib/Topology/Category/Stonean/Limits.lean