∀ {X : SSet} {dim : ℕ} {simplex : X.obj (Opposite.op (SimplexCategory.mk dim))} {dim_1 : ℕ}
  {simplex_1 : X.obj (Opposite.op (SimplexCategory.mk dim_1))},
  { dim := dim, simplex := simplex } = { dim := dim_1, simplex := simplex_1 } → dim = dim_1 ∧ simplex ≍ simplex_1