Theorems · Definition · category theory

CategoryTheory.shrinkCoyonedaCompEvaluationCompUliftFunctorIsoUliftFunctor

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      (Y : C) →
        CategoryTheory.shrinkCoyoneda.{w, v, u}.comp
            (((CategoryTheory.evaluation C (Type w)).obj Y).comp CategoryTheory.uliftFunctor.{v, w}) ≅
          (CategoryTheory.yoneda.obj Y).comp CategoryTheory.uliftFunctor.{w, v}

The functor shrinkCoyoneda.{w} followed by the evaluation at Y : C and uliftFunctor.{v} identifies to yoneda.obj Y followed by uliftFunctor.{w}.

Defined in

Mathlib.CategoryTheory.ShrinkYoneda

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.LocallySmall