∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6}
  (p : I × J → K) {X₁ X₂ : CategoryTheory.GradedObject I C₁} (f : X₁ ⟶ X₂) {Y₁ Y₂ : CategoryTheory.GradedObject J C₂}
  (g : Y₁ ⟶ Y₂) [inst_3 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p]
  [inst_4 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p] (i : I) (j : J) (k : K)
  (h : p (i, j) = k),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X₁ Y₁ i j k h)
      (CategoryTheory.GradedObject.mapBifunctorMapMap F p f g k) =
    CategoryTheory.CategoryStruct.comp ((F.map (f i)).app (Y₁ j))
      (CategoryTheory.CategoryStruct.comp ((F.obj (X₂ i)).map (g j))
        (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X₂ Y₂ i j k h))