Theorems · Theorem · category theory

CategoryTheory.ConcreteCategory.comp_apply

∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {FC : outParam (C → C → Type u_1)} {CC : outParam (C → Type w)}
  {inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))} [self : CategoryTheory.ConcreteCategory C FC]
  {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : CC X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

Defined in

Mathlib.CategoryTheory.ConcreteCategory.Basic

Cited by

60 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

CategoryTheory.ConcreteCategory