∀ (x : Pointed),
  Option.map (CategoryTheory.CategoryStruct.id x).toFun { X := Option x.X, toProd := (some x.point, none) }.toProd.2 =
    Option.map (CategoryTheory.CategoryStruct.id x).toFun { X := Option x.X, toProd := (some x.point, none) }.toProd.2