Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes