∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory}
  (e : X.obj ≅ Y.obj), (P.isoMk e).inv = CategoryTheory.ObjectProperty.homMk e.inv