English
Let ι be a finite index type and (α i) a family of types. For any type C depending on the family of truncations ∀ i, Trunc(α i), together with a datum q = (i ↦ Trunc(α i)), a family f assigning to each a : ∀ i, α i an element of C (mk a ·), and a coherence condition h saying that f is constant along compatible choices, there exists an element of C q. In other words, there is a recursion principle for the finite-index truncations.
Русский
Пусть ι — конечный индексный тип и (α i) — семейство типов. Для любой задачи C, зависящей от семейства Trunc(α i), и любых данных q = (i ↦ Trunc(α i)), f, задающего для каждого a : ∀ i, α i элемент C (mk a ·), и согласовательного условия h, существует элемент типа C q. Иными словами, существует рекурсивный принцип для конечнопозиционных обрезанных типов.
LaTeX
$$$\forall \iota\ (\text{finite})\;\forall \alpha: \iota \to \mathrm{Sort},\; \forall C: ((i:\iota) \mapsto \mathrm{Trunc}(\alpha(i))) \to \mathrm{Sort},\; \forall q: (i:\iota) \mapsto \mathrm{Trunc}(\alpha(i)),\; \forall f: (a: (i:\iota) \to \alpha(i)) \mapsto C(\mathrm{mk}\, a),\; \forall h: \forall (a,b: (i:\iota) \to \alpha(i)), \mathrm{Eq}(\mathrm{Eq.ndrec}(f(a))(\mathrm{funext}(\lambda\_:\iota, \mathrm{Trunc.eq}(_ , _)))) = f(b) \;\Rightarrow \; C(q) $$$
Lean4
/-- Recursion principle for `Trunc`s indexed by a finite type. -/
@[elab_as_elim]
def finRecOn {C : (∀ i, Trunc (α i)) → Sort*} (q : ∀ i, Trunc (α i)) (f : ∀ a : ∀ i, α i, C (mk <| a ·))
(h : ∀ (a b : ∀ i, α i), (Eq.ndrec (f a) (funext fun _ ↦ Trunc.eq _ _)) = f b) : C q :=
Quotient.finRecOn q (f ·) (fun _ _ _ ↦ h _ _)
