Theorems · Theorem · category theory

MonCat.Colimits.cocone_naturality_components

∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] (F : CategoryTheory.Functor J MonCat) (j j' : J) (f : j ⟶ j')
  (x : ↑(F.obj j)),
  (CategoryTheory.ConcreteCategory.hom (MonCat.Colimits.coconeMorphism F j'))
      ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) =
    (CategoryTheory.ConcreteCategory.hom (MonCat.Colimits.coconeMorphism F j)) x

Defined in

Mathlib.Algebra.Category.MonCat.Colimits

Cited by

0 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.Category