English
There is a canonical interpretation of n-ary functions p0 → p1 → ... → p(n-1) → τ, built recursively from a family p: Fin n → Type and a codomain τ. This defines the type FromTypes.
Русский
Существует каноническое задание n-арных функций p_0 → p_1 → ... → p_{n-1} → τ, определяемое рекурсивно по семейству p: Fin n → Type и коду τ. Это задаёт тип FromTypes.
LaTeX
$$$\\mathrm{FromTypes}: \\{n: \\mathbb{N}\\} \\to (\\mathrm{Fin}\n n \\to \\mathrm{Type}) \\to \\mathrm{Type} \\to \\mathrm{Type}$ с базовым случаем $\\mathrm{FromTypes}(0,p,\\tau)=\\tau$ и рекуррентно $\\mathrm{FromTypes}(n+1,p,\\tau)=p(0) \\to \\mathrm{FromTypes}(n,\\lambda i. p(i+1), \\tau)$.$$
Lean4
/-- The type of `n`-ary functions `p 0 → p 1 → ... → p (n - 1) → τ`. -/
def FromTypes : {n : ℕ} → (Fin n → Type u) → Type u → Type u
| 0, _, τ => τ
| n + 1, p, τ => vecHead p → @FromTypes n (vecTail p) τ
