From 50cc57be33e3775ec01ad91a0a7841a59f28c00a Mon Sep 17 00:00:00 2001 From: Yakov Pechersky Date: Mon, 29 Nov 2021 06:04:28 +0000 Subject: [PATCH] chore(category_theory/limits/shapes/wide_pullbacks): speed up `wide_cospan` (#10535) --- src/category_theory/limits/shapes/wide_pullbacks.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/category_theory/limits/shapes/wide_pullbacks.lean b/src/category_theory/limits/shapes/wide_pullbacks.lean index 09265b0334f1b..a543936508be3 100644 --- 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` -/