Theorems · Definition · category theory
CategoryTheory.Grpd.of
(C : Type u) → [CategoryTheory.Groupoid C] → CategoryTheory.Grpd
Construct a bundled Grpd from the underlying type and the typeclass Groupoid.
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Groupoid
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.
- CategoryTheory.Groupoidstatement and proof · cited by 182
- CategoryTheory.Grpdstatement · cited by 30
- CategoryTheory.Bundled.ofproof · cited by 6
Cited by14
Results whose statement or proof uses this declaration.
- CategoryTheory.Grpd.freeproof · cited by 6
- FundamentalGroupoidFunctor.prodIsostatement · cited by 2
- FundamentalGroupoidFunctor.piIsostatement · cited by 2
- CategoryTheory.Grpd.piIsoPistatement · cited by 1
- CategoryTheory.Grpd.piLimitFanproof · cited by 1
- FundamentalGroupoidFunctor.prodIso_homstatement · cited by 0
- FundamentalGroupoidFunctor.prodIso_invstatement · cited by 0
- CategoryTheory.Grpd.piIsoPi_hom_πstatement · cited by 0
- CategoryTheory.Grpd.coe_ofstatement · cited by 0
- FundamentalGroupoidFunctor.piIso_homstatement · cited by 0
- FundamentalGroupoidFunctor.piIso_invstatement · cited by 0
- CategoryTheory.Grpd.freeForgetAdjunction_counit_appstatement · cited by 0