English
Let F be a multivariate functor with a W-type structure, and let u be a function F(α.append1 β) → β. For any α and elements x, y of the W-type q.P.W α, if x and y are equivalent under the W-equivalence relation WEquiv, then applying recF to x and y yields the same value: recF u x = recF u y.
Русский
Пусть F — многопараметричный функтор с конструкцией W; пусть u: F(α ⊎ β) → β; для любых α и элементов x, y типа q.P.W α, если x и y эквивалентны по отношению WEquiv, то recF u x = recF u y.
LaTeX
$$$\forall {\alpha : TypeVec n} \forall {\beta : Type u} (u : F (\alpha.append1 \beta) \to \beta) \forall x y : (q.P F).W \alpha,\; WEquiv x y \Rightarrow recF\,u\,x = recF\,u\,y$$$
Lean4
theorem recF_eq_of_wEquiv (α : TypeVec n) {β : Type u} (u : F (α.append1 β) → β) (x y : q.P.W α) :
WEquiv x y → recF u x = recF u y := by
apply q.P.w_cases _ x
intro a₀ f'₀ f₀
apply q.P.w_cases _ y
intro a₁ f'₁ f₁ h
refine @WEquiv.recOn _ _ _ _ (fun a a' _ ↦ recF u a = recF u a') _ _ h ?_ ?_ ?_
· intro a f' f₀ f₁ _h ih; simp only [recF_eq]
congr 4; funext; apply ih
· intro a₀ f'₀ f₀ a₁ f'₁ f₁ h; simp only [recF_eq', abs_map, MvPFunctor.wDest'_wMk, h]
· intro x y z _e₁ _e₂ ih₁ ih₂; exact Eq.trans ih₁ ih₂
