English
In a path category, a property P on morphisms depends only on the identity and is preserved under right composition with length-1 paths; hence P holds for all morphisms if it holds for identities and is closed under such right compositions.
Русский
В пути категорий свойство P морфизмов зависит только от тождества и сохраняется при правой композиции с путём длины 1; следовательно, P верно для всех морфизмов, если верно для тождеств и сохраняется при таких правых композициях.
LaTeX
$$$\forall P:\forall {a b}, (a \to b) \to Prop,\; P(\mathrm{Id}) \\Rightarrow \; (\forall p:\; a \to a', q:\; a' \to b, P(p) \Rightarrow P(p \circ q)) \Rightarrow \forall f:\; a \to b, P(f)$$$
Lean4
/-- 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. -/
theorem induction (P : ∀ {a b : Paths V}, (a ⟶ b) → Prop) (id : ∀ {v : V}, P (𝟙 ((of V).obj v)))
(comp : ∀ {u v w : V} (p : (of V).obj u ⟶ (of V).obj v) (q : v ⟶ w), P p → P (p ≫ (of V).map q)) :
∀ {a b : Paths V} (f : a ⟶ b), P f := fun {_} ↦ induction_fixed_source _ id comp
