Theorems · Theorem · category theory

CategoryTheory.EnrichedCat.rightUnitor_inv_out_app

∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₁} [inst_3 : CategoryTheory.EnrichedCategory V D]
  (F : CategoryTheory.EnrichedFunctor V C D) (X : CategoryTheory.ForgetEnrichment V C),
  (CategoryTheory.EnrichedCat.rightUnitor F).inv.out.app X =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.ForgetEnrichment.of V (F.obj (CategoryTheory.ForgetEnrichment.to V X)))

Defined in

Mathlib.CategoryTheory.Enriched.EnrichedCat

Cited by

0 results in Mathlib

Foundations

Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.EnrichedCategoryCategoryTheory.EnrichedCategory