Theorems · Definition · category theory

CategoryTheory.Quiv.pathsEquiv

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

The universal property of the path category of a quiver.

Defined in

Mathlib.CategoryTheory.Category.Quiv

Cited by

1 results in Mathlib

Foundations

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

Assumes

QuiverCategoryTheory.Category