∀ (A : Type u_5) [inst : CategoryTheory.Category.{u_1, u_5} A] (A' : Type u_4)
  [inst_1 : CategoryTheory.Category.{u_2, u_4} A'] (B : Type u_6) [inst_2 : CategoryTheory.Category.{u_3, u_6} B]
  (X : CategoryTheory.Functor (A ⊕ A') B),
  CategoryTheory.Prod.mkHom ((CategoryTheory.Sum.inl_ A A').whiskerLeft (CategoryTheory.CategoryStruct.id X))
      ((CategoryTheory.Sum.inr_ A A').whiskerLeft (CategoryTheory.CategoryStruct.id X)) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Sum.inl_ A A').comp X, (CategoryTheory.Sum.inr_ A A').comp X)