Theorems · Inductive type · category theory

CategoryTheory.EnrichedOrdinaryCategory

(V : Type u') →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [CategoryTheory.MonoidalCategory V] →
      (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max (max (max u u') v) v')

An enriched ordinary category is a category C that is also enriched over a category V in such a way that morphisms X ⟶ Y in C identify to morphisms 𝟙_ V ⟶ (X ⟶[V] Y) in V.

Defined in

Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Cited by

109 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 3 definitions · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.Category