∀ {X : SSet} {n : ℕ}
  (concat :
    (x : X.obj (Opposite.op { len := 1 })) →
      (s : X.obj (Opposite.op { len := n })) →
        CategoryTheory.SimplicialObject.δ X 0 x = X.map ({ len := 0 }.const { len := n } 0).op s →
          X.obj (Opposite.op { len := n + 1 }))
  (map_mkOfSucc_zero_concat :
    ∀ (x : X.obj (Opposite.op { len := 1 })) (s : X.obj (Opposite.op { len := n }))
      (h : CategoryTheory.SimplicialObject.δ X 0 x = X.map ({ len := 0 }.const { len := n } 0).op s),
      X.map (SimplexCategory.mkOfSucc 0).op (concat x s h) = x)
  (δ₀_concat :
    ∀ (x : X.obj (Opposite.op { len := 1 })) (s : X.obj (Opposite.op { len := n }))
      (h : CategoryTheory.SimplicialObject.δ X 0 x = X.map ({ len := 0 }.const { len := n } 0).op s),
      CategoryTheory.SimplicialObject.δ X 0 (concat x s h) = s)
  (injective :
    ∀ {x y : X.obj (Opposite.op { len := n + 1 })},
      X.map (SimplexCategory.mkOfSucc 0).op x = X.map (SimplexCategory.mkOfSucc 0).op y →
        CategoryTheory.SimplicialObject.δ X 0 x = CategoryTheory.SimplicialObject.δ X 0 y → x = y)
  (concat_1 :
    (x : X.obj (Opposite.op { len := 1 })) →
      (s : X.obj (Opposite.op { len := n })) →
        CategoryTheory.SimplicialObject.δ X 0 x = X.map ({ len := 0 }.const { len := n } 0).op s →
          X.obj (Opposite.op { len := n + 1 }))
  (map_mkOfSucc_zero_concat_1 :
    ∀ (x : X.obj (Opposite.op { len := 1 })) (s : X.obj (Opposite.op { len := n }))
      (h : CategoryTheory.SimplicialObject.δ X 0 x = X.map ({ len := 0 }.const { len := n } 0).op s),
      X.map (SimplexCategory.mkOfSucc 0).op (concat_1 x s h) = x)
  (δ₀_concat_1 :
    ∀ (x : X.obj (Opposite.op { len := 1 })) (s : X.obj (Opposite.op { len := n }))
      (h : CategoryTheory.SimplicialObject.δ X 0 x = X.map ({ len := 0 }.const { len := n } 0).op s),
      CategoryTheory.SimplicialObject.δ X 0 (concat_1 x s h) = s)
  (injective_1 :
    ∀ {x y : X.obj (Opposite.op { len := n + 1 })},
      X.map (SimplexCategory.mkOfSucc 0).op x = X.map (SimplexCategory.mkOfSucc 0).op y →
        CategoryTheory.SimplicialObject.δ X 0 x = CategoryTheory.SimplicialObject.δ X 0 y → x = y),
  ({ concat := concat, map_mkOfSucc_zero_concat := map_mkOfSucc_zero_concat, δ₀_concat := δ₀_concat,
        injective := injective } =
      { concat := concat_1, map_mkOfSucc_zero_concat := map_mkOfSucc_zero_concat_1, δ₀_concat := δ₀_concat_1,
        injective := injective_1 }) =
    (concat = concat_1)