mathlib3

227293b5 - feat(category_theory/category/Twop): The category of two-pointed types (#11844)

feat(category_theory/category/Twop): The category of two-pointed types (#11844) Define `Twop`, the category of two-pointed types. Also add `Pointed_to_Bipointed` and remove the erroneous TODOs.