From 152e6c6296bf9740679131317f00743307a38720 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Fri, 1 Feb 2019 14:53:37 -0800
Subject: [PATCH] fix(functor_category): remove superfluous coercions

---
 src/category_theory/functor_category.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/category_theory/functor_category.lean b/src/category_theory/functor_category.lean
index 4233f1f745f74..4c5807678b42d 100644
--- a/src/category_theory/functor_category.lean
+++ b/src/category_theory/functor_category.lean
@@ -35,7 +35,7 @@ section
 
 @[simp] lemma id_app (F : C ⥤ D) (X : C) : (𝟙 F : F ⟹ F).app X = 𝟙 (F.obj X) := rfl
 @[simp] lemma comp_app {F G H : C ⥤ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) :
-  ((α ≫ β) : F ⟹ H).app X = (α : F ⟹ G).app X ≫ (β : G ⟹ H).app X := rfl
+  (α ≫ β).app X = α.app X ≫ β.app X := rfl
 end
 
 namespace nat_trans