Theorems · Definition · category theory

CategoryTheory.enrichedFunctorTypeEquivFunctor

{C : Type u₁} →
  [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] →
    {D : Type u₂} →
      [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] →
        CategoryTheory.EnrichedFunctor (Type v) C D ≃ CategoryTheory.Functor C D

We verify that an enriched functor between Type v enriched categories is just the same thing as an honest functor.

Defined in

Mathlib.CategoryTheory.Enriched.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.EnrichedCategoryCategoryTheory.EnrichedCategory