∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S₁ S₂ : SimplicialObject.Split C} (F : S₁.X ⟶ S₂.X)
  (f : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n)
  (comm :
    autoParam
      (∀ (n : ℕ),
        CategoryTheory.CategoryStruct.comp (S₁.s.ι n) (F.app (Opposite.op (SimplexCategory.mk n))) =
          CategoryTheory.CategoryStruct.comp (f n) (S₂.s.ι n))
      SimplicialObject.Split.Hom.comm._autoParam)
  (F_1 : S₁.X ⟶ S₂.X) (f_1 : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n)
  (comm_1 :
    autoParam
      (∀ (n : ℕ),
        CategoryTheory.CategoryStruct.comp (S₁.s.ι n) (F_1.app (Opposite.op (SimplexCategory.mk n))) =
          CategoryTheory.CategoryStruct.comp (f_1 n) (S₂.s.ι n))
      SimplicialObject.Split.Hom.comm._autoParam),
  ({ F := F, f := f, comm := comm } = { F := F_1, f := f_1, comm := comm_1 }) = (F = F_1 ∧ f = f_1)