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