Commit 2023-03-17 00:32 3fdd077f

View on Github →

feat: port CategoryTheory.Category.Bipointed (#2931)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Category/Bipointed.lean

added def Bipointed.Hom.comp

added theorem Bipointed.coe_of

added def Bipointed.of

added def Bipointed.swap

added def Bipointed.swapEquiv

added theorem Bipointed.swapEquiv_symm

added structure Bipointed

added def bipointedToPointedFst

added theorem bipointedToPointedFst_comp_forget

added def bipointedToPointedSnd

added theorem bipointedToPointedSnd_comp_forget

added def pointedToBipointed

added def pointedToBipointedCompBipointedToPointedFst

added def pointedToBipointedCompBipointedToPointedSnd

added def pointedToBipointedFst

added def pointedToBipointedFstBipointedToPointedFstAdjunction

added theorem pointedToBipointedFst_comp_swap

added def pointedToBipointedSnd

added def pointedToBipointedSndBipointedToPointedSndAdjunction

added theorem pointedToBipointedSnd_comp_swap

added theorem swap_comp_bipointedToPointedFst

added theorem swap_comp_bipointedToPointedSnd