∀ (X : Pointed),
  { hom := { toFun := Option.map (CategoryTheory.CategoryStruct.id X).toFun, map_fst := ⋯, map_snd := ⋯ } } =
    CategoryTheory.CategoryStruct.id
      { X := Option X.X, toTwoPointing := { fst := none, snd := some X.point, fst_ne_snd := ⋯ } }