Theorems · Theorem · category theory

CategoryTheory.ReflPrefunctor.comp_assoc

∀ {U : Type u_1} {V : Type u_2} {W : Type u_3} {Z : Type u_4} [inst : CategoryTheory.ReflQuiver U]
  [inst_1 : CategoryTheory.ReflQuiver V] [inst_2 : CategoryTheory.ReflQuiver W] [inst_3 : CategoryTheory.ReflQuiver Z]
  (F : U ⥤rq V) (G : V ⥤rq W) (H : W ⥤rq Z), F ⋙rq G ⋙rq H = F ⋙rq (G ⋙rq H)

Defined in

Mathlib.Combinatorics.Quiver.ReflQuiver

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext

Assumes

CategoryTheory.ReflQuiverCategoryTheory.ReflQuiverCategoryTheory.ReflQuiverCategoryTheory.ReflQuiver