Theorems · Inductive type · category theory
CategoryTheory.MonoidalClosed
(C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → Type (max u v)A monoidal category C is (right) monoidal closed if every object is (right) closed.
- Cited by
- 134 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 3 definitions · 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.Categorystatement · cited by 32,673
- CategoryTheory.MonoidalCategorystatement · cited by 3,095
Cited by207
Results whose statement or proof uses this declaration.
- CategoryTheory.MonoidalClosed.internalHomstatement and proof · cited by 23
- CategoryTheory.MonoidalCategory.DayConvolutionInternalHomstatement · cited by 17
- CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.πstatement and proof · cited by 14
- CategoryTheory.MonoidalCategory.Arrow.pullbackHomstatement and proof · cited by 12
- CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelfstatement and proof · cited by 10
- CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctorstatement and proof · cited by 10
- CategoryTheory.Functor.closedIhomstatement and proof · cited by 9
- CategoryTheory.ExponentialIdealstatement · cited by 8
- CategoryTheory.InternallyProjectivestatement and proof · cited by 8
- CategoryTheory.MonoidalClosed.internalHomAdjunction₂statement and proof · cited by 7
- CategoryTheory.expComparisonstatement and proof · cited by 7
- CategoryTheory.Pi.ihomstatement and proof · cited by 7
Showing the 200 most cited of 207.