Theorems · Definition · category theory
CategoryTheory.BasedCategory.obj
{𝒮 : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] → CategoryTheory.BasedCategory 𝒮 → Type u₂The type of objects in a BasedCategory
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
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.Categorystatement and proof · cited by 32,673
- CategoryTheory.BasedCategorystatement and proof · cited by 38
Cited by44
Results whose statement or proof uses this declaration.
- CategoryTheory.BasedFunctor.toFunctorstatement · cited by 23
- CategoryTheory.BasedCategory.pstatement · cited by 14
- CategoryTheory.BasedNatTrans.toNatTransstatement · cited by 12
- CategoryTheory.BasedCategory.categorystatement · cited by 9
- CategoryTheory.BasedFunctor.compproof · cited by 7
- CategoryTheory.BasedFunctor.idproof · cited by 4
- CategoryTheory.BasedNatTrans.forgetfulstatement · cited by 3
- CategoryTheory.BasedFunctor.wstatement · cited by 2
- CategoryTheory.BasedNatTrans.extstatement and proof · cited by 2
- CategoryTheory.BasedNatTrans.mk.injstatement and proof · cited by 1
- CategoryTheory.BasedNatTrans.mk.noConfusionstatement and proof · cited by 1
- CategoryTheory.BasedFunctor.mk.injstatement and proof · cited by 1