Theorems · Definition · category theory

CategoryTheory.shrinkYonedaEquiv

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      {X : C} →
        {P : CategoryTheory.Functor Cᵒᵖ (Type w)} →
          (CategoryTheory.shrinkYoneda.{w, v, u}.obj X ⟶ P) ≃ P.obj (Opposite.op X)

The type of natural transformations shrinkYoneda.{w}.obj X ⟶ P with X : C and P : Cᵒᵖ ⥤ Type w is equivalent to P.obj (op X).

Defined in

Mathlib.CategoryTheory.ShrinkYoneda

Cited by

15 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.LocallySmall