Theorems · Theorem · category theory

CategoryTheory.Paths.lift_unique

∀ {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),
  CategoryTheory.Paths.of V ⋙q Φ.toPrefunctor = φ → Φ = CategoryTheory.Paths.lift φ

Defined in

Mathlib.CategoryTheory.PathCategory.Basic

Cited by

1 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound

Assumes

QuiverCategoryTheory.Category