feat: port CategoryTheory.Limits.Shapes.Equalizers (#2562)

leanprover-community · Mar 2, 2023 · 49552cd · 49552cd
1 parent 591e208
commit 49552cd
Show file tree

Hide file tree

Showing 2 changed files with 1,337 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -290,6 +290,7 @@ import Mathlib.CategoryTheory.Limits.HasLimits
 import Mathlib.CategoryTheory.Limits.IsLimit
 import Mathlib.CategoryTheory.Limits.Preserves.Basic
 import Mathlib.CategoryTheory.Limits.Preserves.Limits
+import Mathlib.CategoryTheory.Limits.Shapes.Equalizers
 import Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
 import Mathlib.CategoryTheory.Limits.Shapes.Terminal
 import Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks