∀ {X : Pointed} {Y Y' : Bipointed} (f : pointedToBipointedFst.obj X ⟶ Y) (g : Y ⟶ Y'),
  { toFun := fun f => { toFun := f.toFun ∘ some, map_point := ⋯ },
        invFun := fun f => { toFun := fun o => Option.elim o Y'.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
        left_inv := ⋯, right_inv := ⋯ }
      (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp
      ({ toFun := fun f => { toFun := f.toFun ∘ some, map_point := ⋯ },
          invFun := fun f => { toFun := fun o => Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
          left_inv := ⋯, right_inv := ⋯ }
        f)
      (bipointedToPointedFst.map g)