mathlib

aaaeeaed - feat(category_theory/category/{Pointed,Bipointed}): The categories of pointed/bipointed types (#11777)

feat(category_theory/category/{Pointed,Bipointed}): The categories of pointed/bipointed types (#11777) Define * `Pointed`, the category of pointed types * `Bipointed`, the category of bipointed types * the forgetful functors from `Bipointed` to `Pointed` and from `Pointed` to `Type*` * `Type_to_Pointed`, the functor from `Type*` to `Pointed` induced by `option` * `Bipointed.swap_equiv` the equivalence between `Bipointed` and itself induced by `prod.swap` both ways.