removing the nat_trans and vcomp notations; use \hom and \gg

src/category_theory/adjunction.lean

@@ -27,7 +27,7 @@ structure adjunction (F : C ⥤ D) (G : D ⥤ C) :=
 (hom_equiv : Π (X Y), (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
 (unit : functor.id C ⟶ F.comp G)
 (counit : G.comp F ⟶ functor.id D)
-(hom_equiv_unit' : Π {X Y f}, (hom_equiv X Y) f = (unit : _ ⟹ _).app X ≫ G.map f . obviously)
+(hom_equiv_unit' : Π {X Y f}, (hom_equiv X Y) f = (unit : _ ⟶ _).app X ≫ G.map f . obviously)
 (hom_equiv_counit' : Π {X Y g}, (hom_equiv X Y).symm g = F.map g ≫ counit.app Y . obviously)
 
 namespace adjunction
@@ -57,15 +57,15 @@ by rw [hom_equiv_unit, G.map_comp, ← assoc, ←hom_equiv_unit]
 by rw [equiv.symm_apply_eq]; simp [-hom_equiv_counit]
 
 @[simp] lemma left_triangle :
-  (whisker_right adj.unit F).vcomp (whisker_left F adj.counit) = nat_trans.id _ :=
+  (whisker_right adj.unit F) ≫ (whisker_left F adj.counit) = nat_trans.id _ :=
 begin
   ext1 X, dsimp,
   erw [← adj.hom_equiv_counit, equiv.symm_apply_eq, adj.hom_equiv_unit],
   simp
 end
 
 @[simp] lemma right_triangle :
-  (whisker_left G adj.unit).vcomp (whisker_right adj.counit G) = nat_trans.id _ :=
+  (whisker_left G adj.unit) ≫ (whisker_right adj.counit G) = nat_trans.id _ :=
 begin
   ext1 Y, dsimp,
   erw [← adj.hom_equiv_unit, ← equiv.eq_symm_apply, adj.hom_equiv_counit],
@@ -74,11 +74,11 @@ end
 
 @[simp] lemma left_triangle_components :
   F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 _ :=
-congr_arg (λ (t : _ ⟹ functor.id C ⋙ F), t.app X) adj.left_triangle
+congr_arg (λ (t : nat_trans _ (functor.id C ⋙ F)), t.app X) adj.left_triangle
 
 @[simp] lemma right_triangle_components {Y : D} :
   adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 _ :=
-congr_arg (λ (t : _ ⟹ G ⋙ functor.id C), t.app Y) adj.right_triangle
+congr_arg (λ (t : nat_trans _ (G ⋙ functor.id C)), t.app Y) adj.right_triangle
 
 end
 
@@ -110,8 +110,8 @@ end core_hom_equiv
 structure core_unit_counit (F : C ⥤ D) (G : D ⥤ C) :=
 (unit : functor.id C ⟶ F.comp G)
 (counit : G.comp F ⟶ functor.id D)
-(left_triangle' : (whisker_right unit F).vcomp (whisker_left F counit) = nat_trans.id _ . obviously)
-(right_triangle' : (whisker_left G unit).vcomp (whisker_right counit G) = nat_trans.id _ . obviously)
+(left_triangle' : (whisker_right unit F) ≫ (whisker_left F counit) = nat_trans.id _ . obviously)
+(right_triangle' : (whisker_left G unit) ≫ (whisker_right counit G) = nat_trans.id _ . obviously)
 
 namespace core_unit_counit
 
@@ -152,13 +152,13 @@ def mk_of_unit_counit (adj : core_unit_counit F G) : adjunction F G :=
       change F.map (_ ≫ _) ≫ _ = _,
       rw [F.map_comp, assoc, ←functor.comp_map, adj.counit.naturality, ←assoc],
       convert id_comp _ f,
-      exact congr_arg (λ t : _ ⟹ _, t.app _) adj.left_triangle
+      exact congr_arg (λ t : nat_trans _ _, t.app _) adj.left_triangle
     end,
     right_inv := λ g, begin
       change _ ≫ G.map (_ ≫ _) = _,
       rw [G.map_comp, ←assoc, ←functor.comp_map, ←adj.unit.naturality, assoc],
       convert comp_id _ g,
-      exact congr_arg (λ t : _ ⟹ _, t.app _) adj.right_triangle
+      exact congr_arg (λ t : nat_trans _ _, t.app _) adj.right_triangle
   end },
   .. adj }
 

src/category_theory/comma.lean

@@ -86,13 +86,13 @@ def snd : comma L R ⥤ B :=
 @[simp] lemma fst_map {X Y : comma L R} {f : X ⟶ Y} : (fst L R).map f = f.left := rfl
 @[simp] lemma snd_map {X Y : comma L R} {f : X ⟶ Y} : (snd L R).map f = f.right := rfl
 
-def nat_trans : fst L R ⋙ L ⟹ snd L R ⋙ R :=
+def nat_trans : fst L R ⋙ L ⟶ snd L R ⋙ R :=
 { app := λ X, X.hom }
 
 section
 variables {L₁ L₂ L₃ : A ⥤ T} {R₁ R₂ R₃ : B ⥤ T}
 
-def map_left (l : L₁ ⟹ L₂) : comma L₂ R ⥤ comma L₁ R :=
+def map_left (l : L₁ ⟶ L₂) : comma L₂ R ⥤ comma L₁ R :=
 { obj := λ X,
   { left  := X.left,
     right := X.right,
@@ -103,7 +103,7 @@ def map_left (l : L₁ ⟹ L₂) : comma L₂ R ⥤ comma L₁ R :=
     w' := by tidy; rw [←category.assoc, l.naturality f.left, category.assoc]; tidy } }
 
 section
-variables {X Y : comma L₂ R} {f : X ⟶ Y} {l : L₁ ⟹ L₂}
+variables {X Y : comma L₂ R} {f : X ⟶ Y} {l : L₁ ⟶ L₂}
 @[simp] lemma map_left_obj_left  : ((map_left R l).obj X).left  = X.left                := rfl
 @[simp] lemma map_left_obj_right : ((map_left R l).obj X).right = X.right               := rfl
 @[simp] lemma map_left_obj_hom   : ((map_left R l).obj X).hom   = l.app X.left ≫ X.hom := rfl
@@ -125,22 +125,22 @@ variables {X : comma L R}
 @[simp] lemma map_left_id_inv_app_right : (((map_left_id L R).inv).app X).right = 𝟙 (X.right) := rfl
 end
 
-def map_left_comp (l : L₁ ⟹ L₂) (l' : L₂ ⟹ L₃) :
-(map_left R (l ⊟ l')) ≅ (map_left R l') ⋙ (map_left R l) :=
+def map_left_comp (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃) :
+(map_left R (l ≫ l')) ≅ (map_left R l') ⋙ (map_left R l) :=
 { hom :=
   { app := λ X, { left := 𝟙 _, right := 𝟙 _ } },
   inv :=
   { app := λ X, { left := 𝟙 _, right := 𝟙 _ } } }
 
 section
-variables {X : comma L₃ R} {l : L₁ ⟹ L₂} {l' : L₂ ⟹ L₃}
+variables {X : comma L₃ R} {l : L₁ ⟶ L₂} {l' : L₂ ⟶ L₃}
 @[simp] lemma map_left_comp_hom_app_left  : (((map_left_comp R l l').hom).app X).left  = 𝟙 (X.left)  := rfl
 @[simp] lemma map_left_comp_hom_app_right : (((map_left_comp R l l').hom).app X).right = 𝟙 (X.right) := rfl
 @[simp] lemma map_left_comp_inv_app_left  : (((map_left_comp R l l').inv).app X).left  = 𝟙 (X.left)  := rfl
 @[simp] lemma map_left_comp_inv_app_right : (((map_left_comp R l l').inv).app X).right = 𝟙 (X.right) := rfl
 end
 
-def map_right (r : R₁ ⟹ R₂) : comma L R₁ ⥤ comma L R₂ :=
+def map_right (r : R₁ ⟶ R₂) : comma L R₁ ⥤ comma L R₂ :=
 { obj := λ X,
   { left  := X.left,
     right := X.right,
@@ -151,7 +151,7 @@ def map_right (r : R₁ ⟹ R₂) : comma L R₁ ⥤ comma L R₂ :=
     w' := by tidy; rw [←r.naturality f.right, ←category.assoc]; tidy } }
 
 section
-variables {X Y : comma L R₁} {f : X ⟶ Y} {r : R₁ ⟹ R₂}
+variables {X Y : comma L R₁} {f : X ⟶ Y} {r : R₁ ⟶ R₂}
 @[simp] lemma map_right_obj_left  : ((map_right L r).obj X).left  = X.left                 := rfl
 @[simp] lemma map_right_obj_right : ((map_right L r).obj X).right = X.right                := rfl
 @[simp] lemma map_right_obj_hom   : ((map_right L r).obj X).hom   = X.hom ≫ r.app X.right  := rfl
@@ -173,14 +173,14 @@ variables {X : comma L R}
 @[simp] lemma map_right_id_inv_app_right : (((map_right_id L R).inv).app X).right = 𝟙 (X.right) := rfl
 end
 
-def map_right_comp (r : R₁ ⟹ R₂) (r' : R₂ ⟹ R₃) : (map_right L (r ⊟ r')) ≅ (map_right L r) ⋙ (map_right L r') :=
+def map_right_comp (r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃) : (map_right L (r ≫ r')) ≅ (map_right L r) ⋙ (map_right L r') :=
 { hom :=
   { app := λ X, { left := 𝟙 _, right := 𝟙 _ } },
   inv :=
   { app := λ X, { left := 𝟙 _, right := 𝟙 _ } } }
 
 section
-variables {X : comma L R₁} {r : R₁ ⟹ R₂} {r' : R₂ ⟹ R₃}
+variables {X : comma L R₁} {r : R₁ ⟶ R₂} {r' : R₂ ⟶ R₃}
 @[simp] lemma map_right_comp_hom_app_left  : (((map_right_comp L r r').hom).app X).left  = 𝟙 (X.left)  := rfl
 @[simp] lemma map_right_comp_hom_app_right : (((map_right_comp L r r').hom).app X).right = 𝟙 (X.right) := rfl
 @[simp] lemma map_right_comp_inv_app_left  : (((map_right_comp L r r').inv).app X).left  = 𝟙 (X.left)  := rfl

src/category_theory/discrete_category.lean

@@ -33,7 +33,7 @@ end functor
 namespace nat_trans
 
 @[simp] def of_function {I : Type u₁} {F G : I → C} (f : Π i : I, F i ⟶ G i) :
-  (functor.of_function F) ⟹ (functor.of_function G) :=
+  (functor.of_function F) ⟶ (functor.of_function G) :=
 { app := λ i, f i,
   naturality' := λ X Y g,
   begin

src/category_theory/eq_to_hom.lean

@@ -72,7 +72,7 @@ by cases p; simp
 by ext; cases p; simp
 
 @[simp] lemma eq_to_hom_app {F G : C ⥤ D} (h : F = G) (X : C) :
-  (eq_to_hom h : F ⟹ G).app X = eq_to_hom (functor.congr_obj h X) :=
+  (eq_to_hom h : F ⟶ G).app X = eq_to_hom (functor.congr_obj h X) :=
 by subst h; refl
 
 end category_theory

src/category_theory/functor_category.lean

@@ -23,17 +23,17 @@ However if `C` and `D` are both large categories at the same universe level,
 this is a small category at the next higher level.
 -/
 instance functor.category : category.{(max u₁ v₂ 1)} (C ⥤ D) :=
-{ hom     := λ F G, F ⟹ G,
+{ hom     := λ F G, nat_trans F G,
   id      := λ F, nat_trans.id F,
-  comp    := λ _ _ _ α β, α ⊟ β }
+  comp    := λ _ _ _ α β, vcomp α β }
 
 variables {C D} {E : Sort u₃} [ℰ : category.{v₃} E]
 
 namespace functor.category
 
 section
 
-@[simp] lemma id_app (F : C ⥤ D) (X : C) : (𝟙 F : F ⟹ F).app X = 𝟙 (F.obj X) := rfl
+@[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) :
   (α ≫ β).app X = α.app X ≫ β.app X := rfl
 end
@@ -45,11 +45,11 @@ namespace nat_trans
 
 include ℰ
 
-lemma app_naturality {F G : C ⥤ (D ⥤ E)} (T : F ⟹ G) (X : C) {Y Z : D} (f : Y ⟶ Z) :
+lemma app_naturality {F G : C ⥤ (D ⥤ E)} (T : F ⟶ G) (X : C) {Y Z : D} (f : Y ⟶ Z) :
   ((F.obj X).map f) ≫ ((T.app X).app Z) = ((T.app X).app Y) ≫ ((G.obj X).map f) :=
 (T.app X).naturality f
 
-lemma naturality_app {F G : C ⥤ (D ⥤ E)} (T : F ⟹ G) (Z : D) {X Y : C} (f : X ⟶ Y) :
+lemma naturality_app {F G : C ⥤ (D ⥤ E)} (T : F ⟶ G) (Z : D) {X Y : C} (f : X ⟶ Y) :
   ((F.map f).app Z) ≫ ((T.app Y).app Z) = ((T.app X).app Z) ≫ ((G.map f).app Z) :=
 congr_fun (congr_arg app (T.naturality f)) Z
 

src/category_theory/limits/cones.lean

@@ -49,7 +49,7 @@ An object corepresenting this functor is a colimit of `F`.
 -/
 def cocones : C ⥤ Type v := const J ⋙ coyoneda.obj (op F)
 
-lemma cocones_obj (X : C) : F.cocones.obj X = (F ⟹ (const J).obj X) := rfl
+lemma cocones_obj (X : C) : F.cocones.obj X = (F ⟶ (const J).obj X) := rfl
 
 @[simp] lemma cocones_map_app {X₁ X₂ : C} (f : X₁ ⟶ X₂) (t : F.cocones.obj X₁) (j : J) :
   (F.cocones.map f t).app j = t.app j ≫ f := rfl
@@ -84,13 +84,13 @@ namespace limits
 /--
 A `c : cone F` is:
 * an object `c.X` and
-* a natural transformation `c.π : c.X ⟹ F` from the constant `c.X` functor to `F`.
+* a natural transformation `c.π : c.X ⟶ F` from the constant `c.X` functor to `F`.
 
 `cone F` is equivalent, in the obvious way, to `Σ X, F.cones.obj X`.
 -/
 structure cone (F : J ⥤ C) :=
 (X : C)
-(π : (const J).obj X ⟹ F)
+(π : (const J).obj X ⟶ F)
 
 @[simp] lemma cone.w {F : J ⥤ C} (c : cone F) {j j' : J} (f : j ⟶ j') :
   c.π.app j ≫ F.map f = c.π.app j' :=
@@ -99,13 +99,13 @@ by convert ←(c.π.naturality f).symm; apply id_comp
 /--
 A `c : cocone F` is
 * an object `c.X` and
-* a natural transformation `c.ι : F ⟹ c.X` from `F` to the constant `c.X` functor.
+* a natural transformation `c.ι : F ⟶ c.X` from `F` to the constant `c.X` functor.
 
 `cocone F` is equivalent, in the obvious way, to `Σ X, F.cocones.obj X`.
 -/
 structure cocone (F : J ⥤ C) :=
 (X : C)
-(ι : F ⟹ (const J).obj X)
+(ι : F ⟶ (const J).obj X)
 
 @[simp] lemma cocone.w {F : J ⥤ C} (c : cocone F) {j j' : J} (f : j ⟶ j') :
   F.map f ≫ c.ι.app j' = c.ι.app j :=
@@ -189,15 +189,15 @@ namespace cones
   inv := { hom := φ.inv, w' := λ j, φ.inv_comp_eq.mpr (w j) } }
 
 def postcompose {G : J ⥤ C} (α : F ⟶ G) : cone F ⥤ cone G :=
-{ obj := λ c, { X := c.X, π := c.π ⊟ α },
+{ obj := λ c, { X := c.X, π := c.π ≫ α },
   map := λ c₁ c₂ f, { hom := f.hom, w' :=
   by intro; erw ← category.assoc; simp [-category.assoc] } }
 
 @[simp] lemma postcompose_obj_X {G : J ⥤ C} (α : F ⟶ G) (c : cone F) :
   ((postcompose α).obj c).X = c.X := rfl
 
 @[simp] lemma postcompose_obj_π {G : J ⥤ C} (α : F ⟶ G) (c : cone F) :
-  ((postcompose α).obj c).π = c.π ⊟ α := rfl
+  ((postcompose α).obj c).π = c.π ≫ α := rfl
 
 @[simp] lemma postcompose_map_hom {G : J ⥤ C} (α : F ⟶ G) {c₁ c₂ : cone F} (f : c₁ ⟶ c₂):
   ((postcompose α).map f).hom = f.hom := rfl
@@ -255,14 +255,14 @@ namespace cocones
   inv := { hom := φ.inv, w' := λ j, φ.comp_inv_eq.mpr (w j).symm } }
 
 def precompose {G : J ⥤ C} (α : G ⟶ F) : cocone F ⥤ cocone G :=
-{ obj := λ c, { X := c.X, ι := α ⊟ c.ι },
+{ obj := λ c, { X := c.X, ι := α ≫ c.ι },
   map := λ c₁ c₂ f, { hom := f.hom } }
 
 @[simp] lemma precompose_obj_X {G : J ⥤ C} (α : G ⟶ F) (c : cocone F) :
   ((precompose α).obj c).X = c.X := rfl
 
 @[simp] lemma precompose_obj_ι {G : J ⥤ C} (α : G ⟶ F) (c : cocone F) :
-  ((precompose α).obj c).ι = α ⊟ c.ι := rfl
+  ((precompose α).obj c).ι = α ≫ c.ι := rfl
 
 @[simp] lemma precompose_map_hom {G : J ⥤ C} (α : G ⟶ F) {c₁ c₂ : cocone F} (f : c₁ ⟶ c₂) :
   ((precompose α).map f).hom = f.hom := rfl

src/category_theory/limits/limits.lean

@@ -80,7 +80,7 @@ by rw [h.hom_lift f, h.hom_lift f']; congr; exact funext w
 
 /-- The universal property of a limit cone: a map `W ⟶ X` is the same as
   a cone on `F` with vertex `W`. -/
-def hom_iso (h : is_limit t) (W : C) : (W ⟶ t.X) ≅ ((const J).obj W ⟹ F) :=
+def hom_iso (h : is_limit t) (W : C) : (W ⟶ t.X) ≅ ((const J).obj W ⟶ F) :=
 { hom := λ f, (t.extend f).π,
   inv := λ π, h.lift { X := W, π := π },
   hom_inv_id' := by ext f; apply h.hom_ext; intro j; simp; dsimp; refl }
@@ -191,7 +191,7 @@ by rw [h.hom_desc f, h.hom_desc f']; congr; exact funext w
 
 /-- The universal property of a colimit cocone: a map `X ⟶ W` is the same as
   a cocone on `F` with vertex `W`. -/
-def hom_iso (h : is_colimit t) (W : C) : (t.X ⟶ W) ≅ (F ⟹ (const J).obj W) :=
+def hom_iso (h : is_colimit t) (W : C) : (t.X ⟶ W) ≅ (F ⟶ (const J).obj W) :=
 { hom := λ f, (t.extend f).ι,
   inv := λ ι, h.desc { X := W, ι := ι },
   hom_inv_id' := by ext f; apply h.hom_ext; intro j; simp; dsimp; refl }
@@ -403,7 +403,7 @@ def lim : (J ⥤ C) ⥤ C :=
   map_comp' := λ F G H α β,
     by ext; erw [assoc, is_limit.fac, is_limit.fac, ←assoc, is_limit.fac, assoc]; refl }
 
-variables {F} {G : J ⥤ C} (α : F ⟹ G)
+variables {F} {G : J ⥤ C} (α : F ⟶ G)
 
 @[simp] lemma lim.map_π (j : J) : lim.map α ≫ limit.π G j = limit.π F j ≫ α.app j :=
 by apply is_limit.fac
@@ -417,7 +417,7 @@ lemma limit.map_pre {K : Type v} [small_category K] [has_limits_of_shape K C] (E
 by ext; rw [assoc, limit.pre_π, lim.map_π, assoc, lim.map_π, ←assoc, limit.pre_π]; refl
 
 lemma limit.map_pre' {K : Type v} [small_category K] [has_limits_of_shape.{v} K C]
-  (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟹ E₂) :
+  (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) :
   limit.pre F E₂ = limit.pre F E₁ ≫ lim.map (whisker_right α F) :=
 by ext1; simp [(category.assoc _ _ _ _).symm]
 
@@ -644,7 +644,7 @@ def colim : (J ⥤ C) ⥤ C :=
   map_comp' := λ F G H α β,
     by ext; erw [←assoc, is_colimit.fac, is_colimit.fac, assoc, is_colimit.fac, ←assoc]; refl }
 
-variables {F} {G : J ⥤ C} (α : F ⟹ G)
+variables {F} {G : J ⥤ C} (α : F ⟶ G)
 
 @[simp] lemma colim.ι_map (j : J) : colimit.ι F j ≫ colim.map α = α.app j ≫ colimit.ι G j :=
 by apply is_colimit.fac
@@ -662,7 +662,7 @@ lemma colimit.pre_map {K : Type v} [small_category K] [has_colimits_of_shape K C
 by ext; rw [←assoc, colimit.ι_pre, colim.ι_map, ←assoc, colim.ι_map, assoc, colimit.ι_pre]; refl
 
 lemma colimit.pre_map' {K : Type v} [small_category K] [has_colimits_of_shape.{v} K C]
-  (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟹ E₂) :
+  (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) :
   colimit.pre F E₁ = colim.map (whisker_right α F) ≫ colimit.pre F E₂ :=
 by ext1; simp [(category.assoc _ _ _ _).symm]
 

src/category_theory/limits/types.lean

@@ -37,7 +37,7 @@ instance : has_limits.{u} (Type u) :=
 @[simp] lemma types_limit_pre
   (F : J ⥤ Type u) {K : Type u} [𝒦 : small_category K] (E : K ⥤ J) (g : (limit F).X) :
   limit.pre F E g = (⟨λ k, g.val (E.obj k), by obviously⟩ : (limit (E ⋙ F)).X) := rfl
-@[simp] lemma types_limit_map {F G : J ⥤ Type u} (α : F ⟹ G) (g : (limit F).X) :
+@[simp] lemma types_limit_map {F G : J ⥤ Type u} (α : F ⟶ G) (g : (limit F).X) :
   (lim.map α : (limit F).X → (limit G).X) g =
   (⟨λ j, (α.app j) (g.val j), λ j j' f,
     by rw [←functor_to_types.naturality, ←(g.property f)]⟩ : (limit G).X) := rfl
@@ -71,7 +71,7 @@ instance : has_colimits.{u} (Type u) :=
   (F : J ⥤ Type u) {K : Type u} [𝒦 : small_category K] (E : K ⥤ J) (g : (colimit (E ⋙ F)).X) :
   colimit.pre F E =
   quot.lift (λ p, quot.mk _ ⟨E.obj p.1, p.2⟩) (λ p p' ⟨f, h⟩, quot.sound ⟨E.map f, h⟩) := rfl
-@[simp] lemma types_colimit_map {F G : J ⥤ Type u} (α : F ⟹ G) :
+@[simp] lemma types_colimit_map {F G : J ⥤ Type u} (α : F ⟶ G) :
   (colim.map α : (colimit F).X → (colimit G).X) =
   quot.lift
     (λ p, quot.mk _ ⟨p.1, (α.app p.1) p.2⟩)

src/category_theory/natural_isomorphism.lean

@@ -37,29 +37,26 @@ instance inv_app_is_iso (α : F ≅ G) (X : C) : is_iso (α.inv.app X) :=
   hom_inv_id' := begin rw [←functor.category.comp_app, iso.inv_hom_id, ←functor.category.id_app] end,
   inv_hom_id' := begin rw [←functor.category.comp_app, iso.hom_inv_id, ←functor.category.id_app] end }
 
-@[simp] lemma hom_vcomp_inv (α : F ≅ G) : (α.hom ⊟ α.inv) = nat_trans.id _ :=
+-- TODO remove these
+@[simp] lemma hom_comp_inv (α : F ≅ G) : (α.hom ≫ α.inv) = nat_trans.id _ :=
 begin
-  have h : (α.hom ⊟ α.inv) = α.hom ≫ α.inv := rfl,
-  rw h,
   rw iso.hom_inv_id,
   refl
 end
-@[simp] lemma inv_vcomp_hom (α : F ≅ G) : (α.inv ⊟ α.hom) = nat_trans.id _ :=
+@[simp] lemma inv_comp_hom (α : F ≅ G) : (α.inv ≫ α.hom) = nat_trans.id _ :=
 begin
-  have h : (α.inv ⊟ α.hom) = α.inv ≫ α.hom := rfl,
-  rw h,
   rw iso.inv_hom_id,
   refl
 end
 
 @[simp] lemma hom_app_inv_app_id (α : F ≅ G) (X : C) : α.hom.app X ≫ α.inv.app X = 𝟙 _ :=
 begin
-  rw ←nat_trans.vcomp_app,
+  rw ←functor.category.comp_app,
   simp,
 end
 @[simp] lemma inv_app_hom_app_id (α : F ≅ G) (X : C) : α.inv.app X ≫ α.hom.app X = 𝟙 _ :=
 begin
-  rw ←nat_trans.vcomp_app,
+  rw ←functor.category.comp_app,
   simp,
 end