English
Equational form for Fix.rec: Fix.rec g (Fix.mk x) equals g (appendFun id (Fix.rec g) <$$> x).
Русский
Экватиональная форма Fix.rec: Fix.rec g (Fix.mk x) = g (appendFun id (Fix.rec g) <$$> x).
LaTeX
$$$\text{Fix.rec} \ g \ (\text{Fix.mk} x) = g (\text{appendFun} id (\text{Fix.rec} g) \langle x \rangle)$$$
Lean4
theorem rec_eq {β : Type u} (g : F (append1 α β) → β) (x : F (append1 α (Fix F α))) :
Fix.rec g (Fix.mk x) = g (appendFun id (Fix.rec g) <$$> x) :=
by
have : recF g ∘ fixToW = Fix.rec g := by
apply funext
apply Quotient.ind
intro x
apply recF_eq_of_wEquiv
apply wrepr_equiv
conv =>
lhs
rw [Fix.rec, Fix.mk]
dsimp
rcases h : repr x with ⟨a, f⟩
rw [MvPFunctor.map_eq, recF_eq', ← MvPFunctor.map_eq, MvPFunctor.wDest'_wMk']
rw [← MvPFunctor.comp_map, abs_map, ← h, abs_repr, ← appendFun_comp, id_comp, this]
