Theorems · Definition · category theory
TwoP.toTwoPointing
(self : TwoP) → TwoPointing self.X
The two points of a bipointed type, bundled together as a pair of distinct elements.
- Defined in
- Mathlib.CategoryTheory.Category.TwoP
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TwoPstatement and proof · cited by 31
- TwoPointingstatement · cited by 24
- TwoP.Xstatement · cited by 13
Cited by12
Results whose statement or proof uses this declaration.
- TwoP.toBipointedproof · cited by 15
- TwoP.swapproof · cited by 8
- pointedToTwoPSnd_obj_toTwoPointing_toProdstatement and proof · cited by 0
- TwoP.swapEquiv_inverse_obj_toTwoPointing_toProdstatement and proof · cited by 0
- TwoP.swap_mapstatement · cited by 0
- TwoP.swap_obj_toTwoPointingstatement and proof · cited by 0
- pointedToTwoPFstForgetCompBipointedToPointedFstAdjunctionproof · cited by 0
- pointedToTwoPFst_obj_toTwoPointing_toProdstatement and proof · cited by 0
- pointedToTwoPSndForgetCompBipointedToPointedSndAdjunctionproof · cited by 0
- TwoP.swapEquiv_functor_map_hom_toFunstatement · cited by 0
- TwoP.swapEquiv_functor_obj_toTwoPointing_toProdstatement and proof · cited by 0
- TwoP.swapEquiv_inverse_map_hom_toFunstatement · cited by 0