Theorems · Inductive type · category theory

CategoryTheory.EnrichedCategory

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

A V-category is a category enriched in a monoidal category V. Note that we do not assume that V is a concrete category, so there may not be an "honest" underlying category at all!

Defined in

Mathlib.CategoryTheory.Enriched.Basic

Cited by

99 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategory