∀ (X : PartOrdEmb),
  PartOrdEmb.ofHom (PartOrdEmb.Hom.hom (CategoryTheory.CategoryStruct.id X)).dual =
    CategoryTheory.CategoryStruct.id { carrier := (↑X)ᵒᵈ, str := OrderDual.instPartialOrder ↑X }