feat(category_theory): associator and unitors for functors (#478)

also check pentagon and triangle

category_theory/whiskering.lean

@@ -2,12 +2,14 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Scott Morrison
 
+import category_theory.isomorphism
 import category_theory.functor_category
 
 namespace category_theory
 
 universes u₁ v₁ u₂ v₂ u₃ v₃ u₄ v₄
 
+section
 variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C]
           (D : Type u₂) [𝒟 : category.{u₂ v₂} D]
           (E : Type u₃) [ℰ : category.{u₃ v₃} E]
@@ -86,5 +88,57 @@ rfl
 lemma whisker_right_left (F : B ⥤ C) {G H : C ⥤ D} (α : G ⟹ H) (K : D ⥤ E) :
   whisker_right (whisker_left F α) K = whisker_left F (whisker_right α K) :=
 rfl
+end
+
+namespace functor
+
+universes u₅ v₅
+
+variables {A : Type u₁} [𝒜 : category.{u₁ v₁} A]
+variables {B : Type u₂} [ℬ : category.{u₂ v₂} B]
+include 𝒜 ℬ
+
+def left_unitor (F : A ⥤ B) : ((functor.id _) ⋙ F) ≅ F :=
+{ hom := { app := λ X, 𝟙 (F.obj X) },
+  inv := { app := λ X, 𝟙 (F.obj X) } }
+
+def right_unitor (F : A ⥤ B) : (F ⋙ (functor.id _)) ≅ F :=
+{ hom := { app := λ X, 𝟙 (F.obj X) },
+  inv := { app := λ X, 𝟙 (F.obj X) } }
+
+variables {C : Type u₃} [𝒞 : category.{u₃ v₃} C]
+variables {D : Type u₄} [𝒟 : category.{u₄ v₄} D]
+include 𝒞 𝒟
+
+def associator (F : A ⥤ B) (G : B ⥤ C) (H : C ⥤ D) : ((F ⋙ G) ⋙ H) ≅ (F ⋙ (G ⋙ H)) :=
+{ hom := { app := λ _, 𝟙 _ },
+  inv := { app := λ _, 𝟙 _ } }
+
+omit 𝒟
+
+lemma triangle (F : A ⥤ B) (G : B ⥤ C) :
+  (associator F (functor.id B) G).hom ⊟ (whisker_left F (left_unitor G).hom) =
+    (whisker_right (right_unitor F).hom G) :=
+begin
+  ext1,
+  dsimp [associator, left_unitor, right_unitor],
+  simp
+end
+
+variables {E : Type u₅} [ℰ : category.{u₅ v₅} E]
+include 𝒟 ℰ
+
+variables (F : A ⥤ B) (G : B ⥤ C) (H : C ⥤ D) (K : D ⥤ E)
+
+lemma pentagon :
+  (whisker_right (associator F G H).hom K) ⊟ (associator F (G ⋙ H) K).hom ⊟ (whisker_left F (associator G H K).hom) =
+    ((associator (F ⋙ G) H K).hom ⊟ (associator F G (H ⋙ K)).hom) :=
+begin
+  ext1,
+  dsimp [associator],
+  simp,
+end
+
+end functor
 
 end category_theory