From c9f3b766f897124f770cbc939f3b2c44cb97ca55 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Jun 2015 14:40:26 -0700 Subject: [PATCH] refactor(library/algebra/category/constructions): modify proof It was affected by the new way of handling projections that we will implement --- library/algebra/category/constructions.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/algebra/category/constructions.lean b/library/algebra/category/constructions.lean index 474c15d43..b60976e69 100644 --- a/library/algebra/category/constructions.lean +++ b/library/algebra/category/constructions.lean @@ -140,7 +140,7 @@ namespace category (λ a, F a) (λ a b f, F f) (λ a, respect_id F a) - (λ a b c g f, respect_comp F f g) + (λ a b c g f, by apply @respect_comp C D) end end opposite