Theorems · Theorem · category theory

CategoryTheory.Paths.lift_spec

∀ {V : Type u₁} [inst : Quiver V] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C] (φ : V ⥤q C),
  CategoryTheory.Paths.of V ⋙q (CategoryTheory.Paths.lift φ).toPrefunctor = φ

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