Theorems · Definition · category theory

CategoryTheory.enrichedNatTransYonedaTypeIsoYonedaNatTrans

{C : Type v} →
  [inst : CategoryTheory.EnrichedCategory (Type v) C] →
    {D : Type v} →
      [inst_1 : CategoryTheory.EnrichedCategory (Type v) D] →
        (F G : CategoryTheory.EnrichedFunctor (Type v) C D) →
          CategoryTheory.enrichedNatTransYoneda F G ≅
            CategoryTheory.yoneda.obj
              (CategoryTheory.enrichedFunctorTypeEquivFunctor F ⟶ CategoryTheory.enrichedFunctorTypeEquivFunctor G)

We verify that the presheaf representing natural transformations between Type v-enriched functors is actually represented by the usual type of natural transformations!

Defined in

Mathlib.CategoryTheory.Enriched.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.EnrichedCategoryCategoryTheory.EnrichedCategory