Theorems · Definition · category theory

Prefunctor.comp

{U : Type u_1} →
  [inst : Quiver U] →
    {V : Type u_2} → [inst_1 : Quiver V] → {W : Type u_3} → [inst_2 : Quiver W] → U ⥤q V → V ⥤q W → U ⥤q W

Composition of morphisms between quivers.

Defined in

Mathlib.Combinatorics.Quiver.Prefunctor

Cited by

35 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

QuiverQuiverQuiver