(C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Δ : SimplexCategoryᵒᵖ} →
      (A : SimplicialObject.Splitting.IndexSet Δ) →
        SimplicialObject.Split.evalN C (Opposite.unop A.fst).len ⟶
          (SimplicialObject.Split.forget C).comp ((CategoryTheory.evaluation SimplexCategoryᵒᵖ C).obj Δ)