English
Let F be a functor and q a QPF F. For every α, every u : F α → α, and every x, y in the W-type (q.P F).W, if x is Wequiv-related to y, then recF u x = recF u y.
Русский
Пусть F — конфигурация функторa и q — QPF F. Для любого типа α и любой функции u: F α → α, а также для любых x, y ∈ W‑типа (q.P F).W, если x и y эквивалентны по Wequiv, то recF u x = recF u y.
LaTeX
$$$$\forall \{F : Type u \to Type v\} [q : QPF F] \{\alpha : Type u\} (u : F \alpha \to \alpha) (x y : (q.P F).W),\ Wequiv x y \to recF u x = recF u y.$$$$
Lean4
/-- `recF` is insensitive to the representation -/
theorem recF_eq_of_Wequiv {α : Type u} (u : F α → α) (x y : q.P.W) : Wequiv x y → recF u x = recF u y :=
by
intro h
induction h with
| ind a f f' _ ih => simp only [recF_eq', PFunctor.map_eq, Function.comp_def, ih]
| abs a f a' f' h => simp only [recF_eq', abs_map, h]
| trans x y z _ _ ih₁ ih₂ => exact Eq.trans ih₁ ih₂
