Theorems · Definition · category theory

CategoryTheory.Quiv.lift

{V : Type u} →
  [inst : Quiver V] →
    {C : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} C] → V ⥤q C → CategoryTheory.Functor (CategoryTheory.Paths V) C

Any prefunctor into a category lifts to a functor from the path category.

Defined in

Mathlib.CategoryTheory.Category.Quiv

Cited by

2 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext

Assumes

QuiverCategoryTheory.Category