English
In a path category with fixed source a, to prove a property P for all morphisms a ⟶ b it suffices to prove P for the identity and that P is preserved under right composition with a length-1 path.
Русский
В категорийном пути с фиксированным источником a, чтобы доказать свойство P для всех морфизмов a ⟶ b, достаточно доказать P для тождества и что P сохраняется при правой композиции с путём длины 1.
LaTeX
$$$\forall a:\, Paths V,\; \forall (P:\{b: Paths V\}\to (a \to b)\to Prop),\; P(\mathrm{Id}_{a}) \Rightarrow (\forall u v, p:\, a\to (of V).obj u, q:\, u\to v, P(p) \Rightarrow P(p \circ (of V).map q))\Rightarrow \forall b:\, Paths V,\; \forall f:\, a \to b, P(f)$$$
Lean4
/-- To prove a property on morphisms of a path category with given source `a`, 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_fixed_source {a : Paths V} (P : ∀ {b : Paths V}, (a ⟶ b) → Prop) (id : P (𝟙 a))
(comp : ∀ {u v : V} (p : a ⟶ (of V).obj u) (q : u ⟶ v), P p → P (p ≫ (of V).map q)) :
∀ {b : Paths V} (f : a ⟶ b), P f := by
intro _ f
induction f with
| nil => exact id
| cons _ w h => exact comp _ w h
