∀ {C₁ : Type u_7} {C₂ : Type u_2} {C₃ : Type u_5} [inst : CategoryTheory.Category.{u_6, u_7} C₁]
  [inst_1 : CategoryTheory.Category.{u_8, u_2} C₂] [inst_2 : CategoryTheory.Category.{u_4, u_5} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_9} {J : Type u_1} {K : Type u_3}
  (p : I × J → K)
  [inst_3 :
    ∀ (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂),
      (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p]
  (X : CategoryTheory.GradedObject I C₁) (X_1 : CategoryTheory.GradedObject J C₂),
  CategoryTheory.GradedObject.mapBifunctorMapMap F p (CategoryTheory.CategoryStruct.id X)
      (CategoryTheory.CategoryStruct.id X_1) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.GradedObject.mapBifunctorMapObj F p X X_1)