English
There is a two-argument induction principle for Trunc α and Trunc β: if a property holds on all mk a, mk b, it holds on any q1, q2.
Русский
Существует двухаргументная индукционная принципия для Trunc α и Trunc β: если свойство верно на всех mk a, mk b, верно и для любых q1, q2.
LaTeX
$$$\\forall q_1:\\, \\mathrm{Trunc}(\\alpha), q_2:\\, \\mathrm{Trunc}(\\beta),\\ (\\forall a:\\, \\alpha,\\forall b:\\, \\beta,\\ C(\\mathrm{mk}'' a)(\\mathrm{mk}'' b)) \\Rightarrow C(q_1,q_2)$$$
Lean4
@[elab_as_elim]
protected theorem induction_on₂ {C : Trunc α → Trunc β → Prop} (q₁ : Trunc α) (q₂ : Trunc β)
(h : ∀ a b, C (mk a) (mk b)) : C q₁ q₂ :=
Trunc.induction_on q₁ fun a₁ ↦ Trunc.induction_on q₂ (h a₁)
