Theorems · Theorem · category theory

CategoryTheory.Paths.induction

∀ {V : Type u₁} [inst : Quiver V] (P : {a b : CategoryTheory.Paths V} → (a ⟶ b) → Prop),
  (∀ {v : V}, P (CategoryTheory.CategoryStruct.id ((CategoryTheory.Paths.of V).obj v))) →
    (∀ {u v w : V} (p : (CategoryTheory.Paths.of V).obj u ⟶ (CategoryTheory.Paths.of V).obj v) (q : v ⟶ w),
        P p → P (CategoryTheory.CategoryStruct.comp p ((CategoryTheory.Paths.of V).map q))) →
      ∀ {a b : CategoryTheory.Paths V} (f : a ⟶ b), P f

To prove a property on morphisms of a path category, it suffices to prove it for the identity and prove that the property is preserved under composition on the right with length 1 paths.

Defined in

Mathlib.CategoryTheory.PathCategory.Basic

Cited by

2 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext

Assumes

Quiver