∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} {e₀₁ : SSet.Edge x₀ x₁}
  (simplex : X.obj (Opposite.op (SimplexCategory.mk 2))),
  CategoryTheory.SimplicialObject.δ X 2 simplex = e₀₁.edge →
    ((SSet.truncation 2).obj X).map
        (SimplexCategory.Truncated.δ₂ 2 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op
        simplex =
      e₀₁.toTruncated.edge