Theorems · Definition · category theory

CategoryTheory.EnrichedFunctor.forgetId

(W : Type v') →
  [inst : CategoryTheory.Category.{w', v'} W] →
    [inst_1 : CategoryTheory.MonoidalCategory W] →
      (C : Type u₁) →
        [inst_2 : CategoryTheory.EnrichedCategory W C] →
          (CategoryTheory.EnrichedFunctor.id W C).forget ≅
            CategoryTheory.Functor.id (CategoryTheory.ForgetEnrichment W C)

EnrichedFunctor.forget maps the identity enriched functor to a functor isomorphic to Functor.id.

Defined in

Mathlib.CategoryTheory.Enriched.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.EnrichedCategory