Theorems · Definition · category theory
CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf
(C : Type u) →
[inst : CategoryTheory.Category.{v, u} C] →
[inst_1 : CategoryTheory.MonoidalCategory C] →
[CategoryTheory.MonoidalClosed C] → CategoryTheory.EnrichedOrdinaryCategory C CA monoidal closed category is an enriched ordinary category over itself.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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.MonoidalCategorystatement and proof · cited by 3,095
- CategoryTheory.MonoidalClosedstatement and proof · cited by 134
- CategoryTheory.EnrichedOrdinaryCategorystatement · cited by 109
- CategoryTheory.MonoidalClosed.curryHomEquiv'proof · cited by 4
Cited by15
Results whose statement or proof uses this declaration.
- CategoryTheory.MonoidalClosed.FunctorCategory.homEquivstatement · cited by 2
- CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquivstatement · cited by 2
- CategoryTheory.Presheaf.isSheaf_functorEnrichedHomstatement · cited by 1
- CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv_naturalitystatement · cited by 1
- CategoryTheory.GrothendieckTopology.W.whiskerLeftstatement · cited by 1
- CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerLeftstatement · cited by 1
- CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerRightstatement · cited by 1
- CategoryTheory.MonoidalClosed.FunctorCategory.closedstatement · cited by 0
- CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv_naturality_threestatement · cited by 0
- CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv_naturality_two_symmstatement · cited by 0
- CategoryTheory.MonoidalClosed.FunctorCategory.monoidalClosedstatement · cited by 0
- CategoryTheory.GrothendieckTopology.W.whiskerRightstatement · cited by 0