{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) →
                      (F.flip.obj Y ≅ CategoryTheory.Functor.id D) →
                        [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] →
                          (p : J × I → J) →
                            (∀ (j : J), p (j, 0) = j) →
                              (X : CategoryTheory.GradedObject J D) →
                                (j : J) →
                                  (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj
                                        ((CategoryTheory.GradedObject.single₀ I).obj Y)).CofanMapObjFun
                                    p j