English
Let P be the multivariate functorial W-construction. For any g that defines a W-algebra structure, and for any a, f′, f, the recursor satisfies the defining equation: wRec g (wMk a f′ f) = g a f′ f (λ i, wRec g (f i)).
Русский
Пусть P задаёт мультивекторную конструкцию W. Для любого g, задающего структуру алгебры W, и любых a, f′, f выполняется определяющее равенство: wRec g (wMk a f′ f) = g a f′ f (λ i, wRec g (f i)).
LaTeX
$$$ wRec\, g\,(wMk\, a\, f'\, f) = g\, a\, f'\, f\, (\lambda i.\, wRec\, g\,(f\, i)) $$$
Lean4
/-- Defining equation for the recursor of `W` -/
theorem wRec_eq {α : TypeVec n} {C : Type*}
(g : ∀ a : P.A, P.drop.B a ⟹ α → (P.last.B a → P.W α) → (P.last.B a → C) → C) (a : P.A) (f' : P.drop.B a ⟹ α)
(f : P.last.B a → P.W α) : P.wRec g (P.wMk a f' f) = g a f' f fun i => P.wRec g (f i) :=
rfl
