Documentation

Mathlib.CategoryTheory.GradedObject.Unitor

The left and right unitors #

Given a bifunctor F : C ⥤ D ⥤ D, an object X : C such that F.obj X ≅ 𝟭 D and a map p : I × J → J such that hp : ∀ (j : J), p ⟨0, j⟩ = j, we define an isomorphism of J-graded objects for any Y : GradedObject J D. mapBifunctorLeftUnitor F X e p hp Y : mapBifunctorMapObj F p ((single₀ I).obj X) Y ≅ Y.

TODO (@joelriou): define similarly a right unitor isomorphism and get the triangle identity.

source
@[simp]
theorem CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso_inv {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) (Y : CategoryTheory.GradedObject J D) (a : I × J) (ha : a.1 = 0) :
(CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso F X e Y a ha).inv = CategoryTheory.CategoryStruct.comp (e.inv.app (Y a.2)) ((F.map (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 X a.1 ha).inv).app (Y a.2))
source
@[simp]
theorem CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso_hom {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) (Y : CategoryTheory.GradedObject J D) (a : I × J) (ha : a.1 = 0) :
(CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso F X e Y a ha).hom = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 X a.1 ha).hom).app (Y a.2)) (e.hom.app (Y a.2))
source
noncomputable def CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) (Y : CategoryTheory.GradedObject J D) (a : I × J) (ha : a.1 = 0) :
((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y a ≅ Y a.2

Given F : C ⥤ D ⥤ D, X : C, e : F.obj X ≅ 𝟭 D and Y : GradedObject J D, this is the isomorphism ((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y a ≅ Y a.2 when a : I × J is such that a.1 = 0.

Equations
Instances For
    source
    noncomputable def CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIsInitial {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) [(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.Functor.flip F).obj Y)] (Y : CategoryTheory.GradedObject J D) (a : I × J) (ha : a.1 ≠ 0) :
    CategoryTheory.Limits.IsInitial (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y a)

    Given F : C ⥤ D ⥤ D, X : C and Y : GradedObject J D, ((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y a is an initial when a : I × J is such that a.1 ≠ 0.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.Functor.flip F).obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) (j : J) :
      CategoryTheory.GradedObject.CofanMapObjFun (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) p j

      Given F : C ⥤ D ⥤ D, X : C, e : F.obj X ≅ 𝟭 D, Y : GradedObject J D and p : I × J → J such that p ⟨0, j⟩ = j for all j, this is the (colimit) cofan which shall be used to construct the isomorphism mapBifunctorMapObj F p ((single₀ I).obj X) Y ≅ Y, see mapBifunctorLeftUnitor.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan_inj_assoc {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.Functor.flip F).obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) (j : J) {Z : D} (h : (CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan F X e p hp Y j).pt ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan F X e p hp Y j) { val := (0, j), property := ⋯ }) h = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j)) (CategoryTheory.CategoryStruct.comp (e.hom.app (Y j)) h)
        source
        @[simp]
        theorem CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan_inj {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.Functor.flip F).obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) (j : J) :
        CategoryTheory.Limits.Cofan.inj (CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan F X e p hp Y j) { val := (0, j), property := ⋯ } = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j)) (e.hom.app (Y j))
        source
        noncomputable def CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofanIsColimit {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.Functor.flip F).obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) (j : J) :
        CategoryTheory.Limits.IsColimit (CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan F X e p hp Y j)

        The cofan mapBifunctorLeftUnitorCofan F X e p hp Y j is a colimit.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem CategoryTheory.GradedObject.mapBifunctorLeftUnitor_hasMap {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.Functor.flip F).obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) :
          CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) p
          source
          noncomputable def CategoryTheory.GradedObject.mapBifunctorLeftUnitor {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.Functor.flip F).obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) [CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) p] :
          CategoryTheory.GradedObject.mapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y ≅ Y

          Given F : C ⥤ D ⥤ D, X : C, e : F.obj X ≅ 𝟭 D, Y : GradedObject J D and p : I × J → J such that p ⟨0, j⟩ = j for all j, this is the left unitor isomorphism mapBifunctorMapObj F p ((single₀ I).obj X) Y ≅ Y.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.GradedObject.ι_mapBifunctorLeftUnitor_hom_assoc {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.Functor.flip F).obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) [CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) p] (j : J) {Z : D} (h : Y j ⟶ Z) :
            CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y 0 j j ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).hom j) h) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j)) (CategoryTheory.CategoryStruct.comp (e.hom.app (Y j)) h)
            source
            @[simp]
            theorem CategoryTheory.GradedObject.ι_mapBifunctorLeftUnitor_hom {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.Functor.flip F).obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) [CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) p] (j : J) :
            CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y 0 j j ⋯) ((CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).hom j) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j)) (e.hom.app (Y j))
            source
            theorem CategoryTheory.GradedObject.mapBifunctorLeftUnitor_inv_apply {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.Functor.flip F).obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) [CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) p] (j : J) :
            (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).inv j = CategoryTheory.CategoryStruct.comp (e.inv.app (Y j)) (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).inv).app (Y j)) (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y 0 j j ⋯))
            source
            theorem CategoryTheory.GradedObject.mapBifunctorLeftUnitor_inv_naturality_assoc {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.Functor.flip F).obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) {Y : CategoryTheory.GradedObject J D} {Y' : CategoryTheory.GradedObject J D} (φ : Y ⟶ Y') [CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) p] [CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y') p] {Z : CategoryTheory.GradedObject J D} (h : CategoryTheory.GradedObject.mapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y' ⟶ Z) :
            CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorMapMap F p (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ) h)
            source
            theorem CategoryTheory.GradedObject.mapBifunctorLeftUnitor_inv_naturality {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.Functor.flip F).obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) {Y : CategoryTheory.GradedObject J D} {Y' : CategoryTheory.GradedObject J D} (φ : Y ⟶ Y') [CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) p] [CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y') p] :
            CategoryTheory.CategoryStruct.comp φ (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).inv (CategoryTheory.GradedObject.mapBifunctorMapMap F p (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ)
            source
            theorem CategoryTheory.GradedObject.mapBifunctorLeftUnitor_naturality_assoc {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.Functor.flip F).obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) {Y : CategoryTheory.GradedObject J D} {Y' : CategoryTheory.GradedObject J D} (φ : Y ⟶ Y') [CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) p] [CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y') p] {Z : CategoryTheory.GradedObject J D} (h : Y' ⟶ Z) :
            CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorMapMap F p (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).hom (CategoryTheory.CategoryStruct.comp φ h)
            source
            theorem CategoryTheory.GradedObject.mapBifunctorLeftUnitor_naturality {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.Functor.flip F).obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) {Y : CategoryTheory.GradedObject J D} {Y' : CategoryTheory.GradedObject J D} (φ : Y ⟶ Y') [CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) p] [CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y') p] :
            CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorMapMap F p (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ) (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).hom φ