∀ (X : Pointed),
  CategoryTheory.CategoryStruct.comp { toFun := id, map_point := ⋯ } { toFun := id, map_point := ⋯ } =
    CategoryTheory.CategoryStruct.id ((pointedToBipointed.comp bipointedToPointedSnd).obj X)