English
A variant of induction for path categories: if P holds for identities and is preserved under left composition with a 1-step morphism, then P holds for all morphisms.
Русский
Вариант индукции для путевых категорий: если P выполняется для тождеств и сохраняется при левой композиции с морфизмом длины 1, то P верно для всех морфизмов.
LaTeX
$$$\forall P:\forall {a b}, (a \to b) \to Prop,\; (\forall v, P(\mathrm{Id}_{(of V).obj v})) \Rightarrow (\forall p:\; u \to v, q:\; (of V).obj v \to (of V).obj w, P(q) \Rightarrow P((of V).map 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 left 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 : u ⟶ v) (q : (of V).obj v ⟶ (of V).obj w), P q → P ((of V).map p ≫ q)) :
∀ {a b : Paths V} (f : a ⟶ b), P f := by
intro a b
revert a
exact induction_fixed_target (P := fun f ↦ P f) id (fun _ _ ↦ comp _ _)
