∀ (X : TwoP),
  CategoryTheory.CategoryStruct.comp
      (TwoP.swap.map ((CategoryTheory.Iso.refl (CategoryTheory.Functor.id TwoP)).hom.app X))
      ((CategoryTheory.Iso.refl (TwoP.swap.comp TwoP.swap)).hom.app (TwoP.swap.obj X)) =
    CategoryTheory.CategoryStruct.id (TwoP.swap.obj X)