Theorems · Definition · category theory

CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F₀ F₁ F₂ : CategoryTheory.Functor C C} →
      (α : F₀ ⟶ F₁) →
        (β : F₁ ⟶ F₂) →
          CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans (CategoryTheory.CategoryStruct.comp α β) ≅
            (CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans α).comp
              (CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans β)

A composition of natural transformations gives the composition of corresponding functors.

Defined in

Mathlib.CategoryTheory.Endofunctor.Algebra

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category