Theorems · Definition · category theory

CategoryTheory.shrinkCoyonedaEquiv

{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.shrinkCoyoneda.{w, v, u}.obj X ⟶ P) ≃ P.obj (Opposite.unop X)

The type of natural transformations shrinkCoyoneda.{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

7 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.LocallySmall