English
In a path category with fixed target b, to prove a property P for all morphisms a ⟶ b it suffices to prove P for identity and that P is preserved under left composition with a length-1 path.
Русский
В пути категорий с фиксированным назначением b, чтобы доказать свойство P для всех морфизмов a ⟶ b, достаточно доказать P для тождества и что P сохраняется при левой композиции с путём длины 1.
LaTeX
$$$\forall b:\, Paths V,\; (P:\forall a, (a \to b) \to Prop)\; (\mathrm{Id}_{b})\;\Rightarrow\; (\forall a w, p: (of V).obj v \to b, q: a \to v, P(p) \Rightarrow P((of V).map q \circ p)) \Rightarrow \forall a:\, Paths V,\; \forall f:\, a \to b, P(f)$$$
Lean4
/-- To prove a property on morphisms of a path category with given target `b`, it suffices to prove
it for the identity and prove that the property is preserved under composition on the left
with length 1 paths. -/
theorem induction_fixed_target {b : Paths V} (P : ∀ {a : Paths V}, (a ⟶ b) → Prop) (id : P (𝟙 b))
(comp : ∀ {u v : V} (p : (of V).obj v ⟶ b) (q : u ⟶ v), P p → P ((of V).map q ≫ p)) :
∀ {a : Paths V} (f : a ⟶ b), P f := by
intro a f
generalize h : f.length = k
induction k generalizing f a with
| zero =>
cases f with
| nil => exact id
| cons _ _ => simp at h
| succ k h' =>
obtain ⟨c, f, q, hq, rfl⟩ := f.eq_toPath_comp_of_length_eq_succ h
exact comp _ _ (h' _ hq)
