Theorems · Theorem · category theory

Quiver.FreeGroupoid.lift_unique

∀ {V : Type u} [inst : Quiver V] {V' : Type u'} [inst_1 : CategoryTheory.Groupoid V'] (φ : V ⥤q V')
  (Φ : CategoryTheory.Functor (Quiver.FreeGroupoid V) V'),
  Quiver.FreeGroupoid.of V ⋙q Φ.toPrefunctor = φ → Φ = Quiver.FreeGroupoid.lift φ

Defined in

Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Cited by

3 results in Mathlib

Foundations

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

Assumes

QuiverCategoryTheory.Groupoid