Mathlib Map

Theorems · Inductive type · category theory

Bipointed

Type (u + 1)

The category of bipointed types.

Defined in
Mathlib.CategoryTheory.Category.Bipointed
Cited by
52 results in Mathlib
Foundations
Depth 0 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Bipointed.X · cited by 38Bipointed.XBipointed.Hom.toFun · cited by 21Hom.toFunTwoP.toBipointed · cited by 15TwoP.toBipointedBipointed.toProd · cited by 13Bipointed.toProdBipointed.swap · cited by 11Bipointed.swapBipointed.swapEquiv · cited by 11Bipointed.swapEquivBipointed.Hom · cited by 9Bipointed.HomBipointed.HomSubtype · cited by 9Bipointed.HomSubtypebipointedToPointedFst · cited by 5bipointedToPointedFstbipointedToPointedSnd · cited by 5bipointedToPointedSndpointedToBipointed · cited by 4pointedToBipointedpointedToBipointedFst · cited by 3pointedToBipointedFstpointedToBipointedSnd · cited by 3pointedToBipointedSndpointedToBipointedCompBipointedToPointedFst · cited by 2pointedToBipointedCompBip…pointedToBipointedCompBipointedToPointedSnd · cited by 2pointedToBipointedCompBip…BipointedCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by87

Results whose statement or proof uses this declaration.