∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
  (t :
    CategoryTheory.Limits.Cofork (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)
      (F.map CategoryTheory.Limits.WalkingParallelPairHom.right))
  ⦃X Y : CategoryTheory.Limits.WalkingParallelPair⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (F.map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (t.ι.app Y)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (t.ι.app X))
      (((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj t.pt).map f)