Theorems · Definition · category theory
CategoryTheory.Grpd
Type (max (u + 1) u (v + 1))
Category of groupoids
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Groupoidproof · cited by 182
- CategoryTheory.Bundledproof · cited by 42
Cited by57
Results whose statement or proof uses this declaration.
- FundamentalGroupoid.fundamentalGroupoidFunctorstatement · cited by 21
- CategoryTheory.Grpd.ofstatement · cited by 9
- FundamentalGroupoidFunctor.prodToProdTopstatement · cited by 7
- CategoryTheory.Grpd.freestatement · cited by 6
- FundamentalGroupoid.fromTopstatement · cited by 6
- ContinuousMap.Homotopy.hcaststatement · cited by 6
- ContinuousMap.Homotopy.prodToProdTopIstatement · cited by 4
- CategoryTheory.Grpd.forgetToCatstatement and proof · cited by 4
- CategoryTheory.Grpd.freeForgetAdjunctionstatement and proof · cited by 4
- FundamentalGroupoidFunctor.piToPiTopstatement · cited by 3
- FundamentalGroupoidFunctor.projstatement · cited by 3
- ContinuousMap.Homotopy.eq_path_of_eq_imagestatement · cited by 2