Commit 2025-01-28 09:37 afd713f8

feat: equalizers and coequalizers in the category of ind-objects (#21139) We study parallel pairs of morphisms in Ind C, discover that they are always induced by natural transformations in a suitable indexing category, and deduce that ind-objects are closed under equalizers and the category of ind-objects has coequalizers. Huge thanks to @javra and @datokrat. If they had not spent countless hours tirelessly PRing properties of comma categories and the Grothendieck construction to mathlib this PR would not have been possible, even though you can't see any of their results used in the PR (since they are applied by instance synthesis).