Theorems · Definition · category theory

Quiver.FreeGroupoid.lift

{V : Type u} →
  [inst : Quiver V] →
    {V' : Type u'} → [inst_1 : CategoryTheory.Groupoid V'] → V ⥤q V' → CategoryTheory.Functor (Quiver.FreeGroupoid V) V'

The lift of a prefunctor to a groupoid, to a functor from FreeGroupoid V

Defined in

Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Cited by

5 results in Mathlib

Foundations

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

Assumes

QuiverCategoryTheory.Groupoid