Theorems · Theorem · category theory

CategoryTheory.NatTrans.naturality_apply

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {FD : outParam (D → D → Type u_2)} {CD : outParam (D → Type w)}
  [inst_2 : outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] [inst_3 : CategoryTheory.ConcreteCategory D FD]
  {F G : CategoryTheory.Functor C D} (φ : F ⟶ G) {X Y : C} (f : X ⟶ Y) (x : CategoryTheory.ToType (F.obj X)),
  (CategoryTheory.ConcreteCategory.hom (φ.app Y)) ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) =
    (CategoryTheory.ConcreteCategory.hom (G.map f)) ((CategoryTheory.ConcreteCategory.hom (φ.app X)) x)

Defined in

Mathlib.CategoryTheory.ConcreteCategory.Basic

Cited by

51 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryoutParamCategoryTheory.ConcreteCategory