∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C)
  (e e_1 : F.flip.obj Y ≅ CategoryTheory.Functor.id D),
  e = e_1 →
    ∀ [inst_5 : ∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
      (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D)
      [inst_6 :
        (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj
              ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
          p],
      CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X =
        CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e_1 p hp X