Bipointed.Hom.ext

theorem Bipointed.Hom.ext : ∀ {X Y : Bipointed} (x y : X.Hom Y), x.toFun = y.toFun → x = y

This theorem states that for any two objects `X` and `Y` in the category of bipointed sets, if two morphisms (functions respecting the pointedness) `x` and `y` from `X` to `Y` are such that their underlying functions `x.toFun` and `y.toFun` are identical, then `x` and `y` themselves are necessarily the same. In other words, the morphism in a bipointed category is uniquely determined by its underlying function.

More concisely: In the category of bipointed sets, two morphisms between objects with identical underlying functions are equal.