∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  ⦃X_1 Y_1 : CategoryTheory.Limits.WalkingParallelPair⦄ (f_1 : X_1 ⟶ Y_1),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj 0).map f_1) 0 =
    CategoryTheory.CategoryStruct.comp 0 ((CategoryTheory.Limits.parallelPair f 0).map f_1)