∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {C₂₃ : Type u_5} {E : Type u_9}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃] [inst_3 : CategoryTheory.Category.{v_5, u_5} C₂₃]
  [inst_4 : CategoryTheory.Category.{v_9, u_9} E] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ E))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) (X : C₁) (X_1 : C₂) (X_2 : C₃),
  (((F.bifunctorComp₂₃Iso G₂₃).hom.app X).app X_1).app X_2 =
    CategoryTheory.CategoryStruct.id ((F.obj X).obj ((G₂₃.obj X_1).obj X_2))