Commit 2025-02-13 22:37 4ec5921b

View on Github →

chore(CategoryTheory): move coequalizer in Type to earlier file (#21824) That way we can use the coequalizer of plain functions without importing category theory.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Types.lean

deleted inductive CategoryTheory.Limits.Types.CoequalizerRel

Created Mathlib/Logic/Function/Coequalizer.lean

added inductive Function.Coequalizer.Rel

added theorem Function.Coequalizer.condition

added def Function.Coequalizer.desc

added theorem Function.Coequalizer.desc_mk

added def Function.Coequalizer.mk

added theorem Function.Coequalizer.mk_surjective

added def Function.Coequalizer

Modified Mathlib/Topology/Gluing.lean