Theorems · Definition · category theory

CategoryTheory.FunctorToTypes.shrinkMap

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C (Type w')} →
      (F ⟶ G) →
        [inst_1 : CategoryTheory.FunctorToTypes.Small.{w, w', v, u} F] →
          [inst_2 : CategoryTheory.FunctorToTypes.Small.{w, w', v, u} G] →
            CategoryTheory.FunctorToTypes.shrink.{w, w', v, u} F ⟶ CategoryTheory.FunctorToTypes.shrink.{w, w', v, u} G

The natural transformation shrink.{w} F ⟶ shrink.{w} G induces by a natural transformation τ : F ⟶ G between w-small functors to types.

Defined in

Mathlib.CategoryTheory.ShrinkYoneda

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.FunctorToTypes.SmallCategoryTheory.FunctorToTypes.Small