∀ {x y : SimplexCategory} (e : x ≅ y),
  SimplexCategory.orderIsoOfIso e =
    { toFun := ⇑(SimplexCategory.Hom.toOrderHom e.hom), invFun := ⇑(SimplexCategory.Hom.toOrderHom e.inv),
          left_inv := ⋯, right_inv := ⋯ }.toOrderIso
      ⋯ ⋯