minor changes

src/category_theory/concrete_category.lean

@@ -66,6 +66,7 @@ instance : has_coe_to_fun (X ⟶ Y) :=
 { F   := λ f, X → Y,
   coe := λ f, f.1 }
 
+@[simp] lemma coe_id {X : bundled c} : ((𝟙 X) : X → X) = id := rfl
 @[simp] lemma bundled_hom_coe {X Y : bundled c} (val : X → Y) (prop) (x : X) :
   (⟨val, prop⟩ : X ⟶ Y) x = val x := rfl
 

src/category_theory/eq_to_hom.lean

@@ -4,6 +4,7 @@
 
 import category_theory.isomorphism
 import category_theory.functor_category
+import category_theory.opposites
 
 universes v v' u u' -- declare the `v`'s first; see `category_theory.category` for an explanation
 
@@ -33,6 +34,12 @@ rfl
   eq_to_iso p ≪≫ eq_to_iso q = eq_to_iso (p.trans q) :=
 by ext; simp
 
+@[simp] lemma eq_to_hom_op (X Y : C) (h : X = Y) : (eq_to_hom h).op = eq_to_hom (congr_arg op h.symm) :=
+begin
+  cases h,
+  refl
+end
+
 variables {D : Sort u'} [𝒟 : category.{v'} D]
 include 𝒟
 

src/category_theory/equivalence.lean

@@ -3,7 +3,6 @@
 -- Authors: Tim Baumann, Stephen Morgan, Scott Morrison
 
 import category_theory.fully_faithful
-import category_theory.functor_category
 import category_theory.natural_isomorphism
 import tactic.slice
 import tactic.converter.interactive

src/category_theory/functor_category.lean

@@ -36,6 +36,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) :
   (α ≫ β).app X = α.app X ≫ β.app X := rfl
+
 end
 
 namespace nat_trans

src/category_theory/natural_isomorphism.lean

@@ -2,7 +2,6 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Tim Baumann, Stephen Morgan, Scott Morrison
 
-import category_theory.isomorphism
 import category_theory.functor_category
 import category_theory.whiskering
 
@@ -27,6 +26,12 @@ def app {F G : C ⥤ D} (α : F ≅ G) (X : C) : F.obj X ≅ G.obj X :=
 @[simp] lemma app_hom {F G : C ⥤ D} (α : F ≅ G) (X : C) : (app α X).hom = α.hom.app X := rfl
 @[simp] lemma app_inv {F G : C ⥤ D} (α : F ≅ G) (X : C) : (app α X).inv = α.inv.app X := rfl
 
+@[simp] lemma hom_inv_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) : α.hom.app X ≫ α.inv.app X = 𝟙 (F.obj X) :=
+congr_fun (congr_arg nat_trans.app α.hom_inv_id) X
+
+@[simp] lemma inv_hom_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) : α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X) :=
+congr_fun (congr_arg nat_trans.app α.inv_hom_id) X
+
 variables {F G : C ⥤ D}
 
 instance hom_app_is_iso (α : F ≅ G) (X : C) : is_iso (α.hom.app X) :=

src/category_theory/opposites.lean

@@ -4,6 +4,7 @@
 
 import category_theory.products
 import category_theory.types
+import category_theory.natural_isomorphism
 
 namespace category_theory
 
@@ -98,6 +99,8 @@ instance category.opposite : category.{v₁} Cᵒᵖ :=
 @[simp] lemma unop_comp {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} :
   (f ≫ g).unop = g.unop ≫ f.unop := rfl
 @[simp] lemma unop_id {X : Cᵒᵖ} : (𝟙 X).unop = 𝟙 (unop X) := rfl
+@[simp] lemma unop_id_op {X : C} : (𝟙 (op X)).unop = 𝟙 X := rfl
+@[simp] lemma op_id_unop {X : Cᵒᵖ} : (𝟙 (unop X)).op = 𝟙 X := rfl
 
 def op_op : (Cᵒᵖ)ᵒᵖ ⥤ C :=
 { obj := λ X, unop (unop X),