English
Equivalence between Fix.dest and Fix.mk in the quotient sense: Fix.dest (Fix.mk x) = x, and the earlier lemmas show the equality propagates through representations.
Русский
Эквивалентность между dest и mk в факторизованном виде: Fix.dest(Fix.mk x) = x; леммы показывают, что равенство сохраняется через представления.
LaTeX
$$$\forall x, \mathrm{Fix.dest}(\mathrm{Fix.mk} x) = x$$$
Lean4
/-- Dependent recursor for `fix F` -/
def drec {β : Fix F α → Type u} (g : ∀ x : F (α ::: Sigma β), β (Fix.mk <| (id ::: Sigma.fst) <$$> x)) (x : Fix F α) :
β x :=
let y := @Fix.rec _ F _ α (Sigma β) (fun i => ⟨_, g i⟩) x
have : x = y.1 := by
symm
dsimp [y]
apply Fix.ind_rec _ id _ x
intro x' ih
rw [Fix.rec_eq]
dsimp
simp only [appendFun_id_id, MvFunctor.id_map] at ih
congr
conv =>
rhs
rw [← ih]
rw [MvFunctor.map_map, ← appendFun_comp, id_comp]
simp only [Function.comp_def]
cast (by rw [this]) y.2
