Theorems · Definition · category theory

CategoryTheory.Paths.lift

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

Any prefunctor from V lifts to a functor from paths V

Defined in

Mathlib.CategoryTheory.PathCategory.Basic

Cited by

7 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext

Assumes

QuiverCategoryTheory.Category