Theorems · Theorem · category theory

Quiver.freeGroupoidFunctor_comp

∀ {V : Type u} [inst : Quiver V] {V' : Type u'} [inst_1 : Quiver V'] {V'' : Type u''} [inst_2 : Quiver V'']
  (φ : V ⥤q V') (φ' : V' ⥤q V''),
  Quiver.freeGroupoidFunctor (φ ⋙q φ') = (Quiver.freeGroupoidFunctor φ).comp (Quiver.freeGroupoidFunctor φ')

Defined in

Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Cited by

0 results in Mathlib

Foundations

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

Assumes

QuiverQuiverQuiver