Commit 2024-02-03 12:31 469d1d73

View on Github →

feat(CategoryTheory/SingleObj): characterise (co)limits of shape SingleObj M in types (#10213) In the category of types: limits of shape SingleObj M are fixed points, colimits are quotients.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean

added theorem CategoryTheory.Limits.SingleObj.Types.Quot.Rel.iff_orbitRel

added def CategoryTheory.Limits.SingleObj.Types.Quot.equivOrbitRelQuotient

added def CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints