Skip to content

Commit

Permalink
fix(functor_category): remove superfluous coercions
Browse files Browse the repository at this point in the history
  • Loading branch information
semorrison committed Feb 1, 2019
1 parent ed0d24a commit 152e6c6
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/category_theory/functor_category.lean
Expand Up @@ -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
Expand Down

0 comments on commit 152e6c6

Please sign in to comment.