chore(category_theory/limits/shapes/wide_pullbacks): speed up `wide_c…

…ospan` (#10535)
leanprover-community · Nov 29, 2021 · 50cc57b · 50cc57b
1 parent 16daabf
commit 50cc57b
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/src/category_theory/limits/shapes/wide_pullbacks.lean b/src/category_theory/limits/shapes/wide_pullbacks.lean
@@ -89,6 +89,13 @@ def wide_cospan (B : C) (objs : J → C) (arrows : Π (j : J), objs j ⟶ B) :
     cases f with _ j,
     { apply (𝟙 _) },
     { exact arrows j }
+  end,
+  map_comp' := λ _ _ _ f g,
+  begin
+    cases f,
+    { simpa },
+    cases g,
+    simpa
   end }
 
 /-- Every diagram is naturally isomorphic (actually, equal) to a `wide_cospan` -/