English
Let g: F α → α and x ∈ F(Fix F). Then Fix.rec g (Fix.mk x) = g (Fix.rec g <$> x).
Русский
Пусть g: F α → α и x ∈ F(Fix F). Тогда Fix.rec g (Fix.mk x) = g (Fix.rec g <$> x).
LaTeX
$$$$\forall {F : Type u \to Type u} [q : QPF F] {\alpha : Type u} (g : F \alpha \to \alpha) (x : F (Fix F)),\ Fix.rec g (Fix.mk x) = g (Fix.rec g <$> x).$$$$
Lean4
theorem rec_eq {α : Type _} (g : F α → α) (x : F (Fix F)) : Fix.rec g (Fix.mk x) = g (Fix.rec g <$> x) :=
by
have : recF g ∘ fixToW = Fix.rec g := by
ext ⟨x⟩
apply recF_eq_of_Wequiv
rw [fixToW]
apply Wrepr_equiv
conv =>
lhs
rw [Fix.rec, Fix.mk]
dsimp
rcases h : repr x with ⟨a, f⟩
rw [PFunctor.map_eq, recF_eq, ← PFunctor.map_eq, PFunctor.W.dest_mk, PFunctor.map_map, abs_map, ← h, abs_repr, this]
