# Commit 2022-02-04 18:53 aaaeeaed

View on Github →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.