Commit 2022-02-12 00:03 227293b5

View on Github →

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.

Estimated changes

Modified src/category_theory/category/Bipointed.lean

added def Pointed_to_Bipointed

added def Pointed_to_Bipointed_comp_Bipointed_to_Pointed_fst

added def Pointed_to_Bipointed_comp_Bipointed_to_Pointed_snd

deleted theorem Pointed_to_Bipointed_fst_comp

added theorem Pointed_to_Bipointed_fst_comp_swap

deleted theorem Pointed_to_Bipointed_snd_comp

added theorem Pointed_to_Bipointed_snd_comp_swap

Modified src/category_theory/category/Pointed.lean

Created src/category_theory/category/Twop.lean

added def Pointed_to_Twop_fst

added theorem Pointed_to_Twop_fst_comp_forget_to_Bipointed

added theorem Pointed_to_Twop_fst_comp_swap

added def Pointed_to_Twop_fst_forget_comp_Bipointed_to_Pointed_fst_adjunction

added def Pointed_to_Twop_snd

added theorem Pointed_to_Twop_snd_comp_forget_to_Bipointed

added theorem Pointed_to_Twop_snd_comp_swap

added def Pointed_to_Twop_snd_forget_comp_Bipointed_to_Pointed_snd_adjunction

added def Twop.of

added def Twop.swap

added def Twop.swap_equiv

added theorem Twop.swap_equiv_symm

added def Twop.to_Bipointed

added structure Twop

added theorem Twop_swap_comp_forget_to_Bipointed