Commit 2025-01-31 07:04 53f8caff

feat(CategoryTheory/Subpresheaf): equalizer (#21096) If F₁ and F₂ are presheaves of types, A : Subpresheaf F₁, and f and g are two morphisms A.toPresheaf ⟶ F₂, we introduce Subcomplex.equalizer f g, which is the subpresheaf of F₁ contained in A where f and g coincide.