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

Created src/category_theory/category/Bipointed.lean

added def Bipointed.hom.comp

added def Bipointed.hom.id

added def Bipointed.of

added def Bipointed.swap

added def Bipointed.swap_equiv

added theorem Bipointed.swap_equiv_symm

added structure Bipointed

added def Bipointed_to_Pointed_fst

added theorem Bipointed_to_Pointed_fst_comp_forget

added def Bipointed_to_Pointed_snd

added theorem Bipointed_to_Pointed_snd_comp_forget

added def Pointed_to_Bipointed_fst

added def Pointed_to_Bipointed_fst_Bipointed_to_Pointed_fst_adjunction

added theorem Pointed_to_Bipointed_fst_comp

added def Pointed_to_Bipointed_snd

added def Pointed_to_Bipointed_snd_Bipointed_to_Pointed_snd_adjunction

added theorem Pointed_to_Bipointed_snd_comp

added theorem swap_comp_Bipointed_to_Pointed_fst

added theorem swap_comp_Bipointed_to_Pointed_snd

Created src/category_theory/category/Pointed.lean

added def Pointed.hom.comp

added def Pointed.hom.id

added def Pointed.of

added structure Pointed

added def Type_to_Pointed

added def Type_to_Pointed_forget_adjunction