∀ {X Y : Pointed} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((pointedToBipointed.comp bipointedToPointedFst).map f)
      ((fun X =>
            { hom := { toFun := id, map_point := ⋯ }, inv := { toFun := id, map_point := ⋯ }, hom_inv_id := ⋯,
              inv_hom_id := ⋯ })
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun X =>
            { hom := { toFun := id, map_point := ⋯ }, inv := { toFun := id, map_point := ⋯ }, hom_inv_id := ⋯,
              inv_hom_id := ⋯ })
          X).hom
      ((CategoryTheory.Functor.id Pointed).map f)