Theorems · Definition · category theory

MonCat.shrinkFunctorMap

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C MonCat} →
      (F ⟶ G) →
        [inst_1 : ∀ (X : C), Small.{w, w'} ↑(F.obj X)] →
          [inst_2 : ∀ (X : C), Small.{w, w'} ↑(G.obj X)] →
            MonCat.shrinkFunctor.{w, w', v, u} F ⟶ MonCat.shrinkFunctor.{w, w', v, u} G

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

Defined in

Mathlib.Algebra.Category.MonCat.Shrink

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategorySmallSmall