Theorems · Theorem · category theory

CategoryTheory.FunctorToTypes.comp

Deprecated since 2026-03-09Use CategoryTheory.NatTrans.comp_app_apply instead.

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G H : CategoryTheory.Functor C (Type w)) {X : C} (σ : F ⟶ G)
  (τ : G ⟶ H) (x : F.obj X),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.CategoryStruct.comp σ τ).app X)) x =
    (CategoryTheory.ConcreteCategory.hom (τ.app X)) ((CategoryTheory.ConcreteCategory.hom (σ.app X)) x)

Defined in

Mathlib.CategoryTheory.Types.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category