Theorems · Theorem · category theory

CategoryTheory.EnrichedFunctor.comp_map

∀ (V : Type v) [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  {D : Type u₂} {E : Type u₃} [inst_2 : CategoryTheory.EnrichedCategory V C]
  [inst_3 : CategoryTheory.EnrichedCategory V D] [inst_4 : CategoryTheory.EnrichedCategory V E]
  (F : CategoryTheory.EnrichedFunctor V C D) (G : CategoryTheory.EnrichedFunctor V D E) (x x_1 : C),
  (CategoryTheory.EnrichedFunctor.comp V F G).map x x_1 =
    CategoryTheory.CategoryStruct.comp (F.map x x_1) (G.map (F.obj x) (F.obj x_1))

Defined in

Mathlib.CategoryTheory.Enriched.Basic

Cited by

1 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.EnrichedCategoryCategoryTheory.EnrichedCategoryCategoryTheory.EnrichedCategory