{X : SSet} →
  {n : ℕ} →
    (concat :
        (x : X.obj (Opposite.op (SimplexCategory.mk 1))) →
          (s : X.obj (Opposite.op (SimplexCategory.mk n))) →
            CategoryTheory.SimplicialObject.δ X 0 x =
                X.map ((SimplexCategory.mk 0).const (SimplexCategory.mk n) 0).op s →
              X.obj (Opposite.op (SimplexCategory.mk (n + 1)))) →
      (∀ (x : X.obj (Opposite.op (SimplexCategory.mk 1))) (s : X.obj (Opposite.op (SimplexCategory.mk n)))
          (h :
            CategoryTheory.SimplicialObject.δ X 0 x =
              X.map ((SimplexCategory.mk 0).const (SimplexCategory.mk n) 0).op s),
          X.map (SimplexCategory.mkOfSucc 0).op (concat x s h) = x) →
        (∀ (x : X.obj (Opposite.op (SimplexCategory.mk 1))) (s : X.obj (Opposite.op (SimplexCategory.mk n)))
            (h :
              CategoryTheory.SimplicialObject.δ X 0 x =
                X.map ((SimplexCategory.mk 0).const (SimplexCategory.mk n) 0).op s),
            CategoryTheory.SimplicialObject.δ X 0 (concat x s h) = s) →
          (∀ {x y : X.obj (Opposite.op (SimplexCategory.mk (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) →
            X.StrictSegalCore n