English
Dest of corec for g equals a mapped form of g under Cofix.dest, demonstrating corec's structure.
Русский
Dest(corec g) = Cofix.dest, отображённая через map, демонстрируя структуру corec.
LaTeX
$$$\\mathrm{dest}(\\mathrm{Cofix.corec}\\ g\\ x) = (q.map (\\text{TypeVec.appendFun TypeVec.id (Cofix.corec g)}) (g\\ x))$$$
Lean4
theorem dest_corec' {α : TypeVec.{u} n} {β : Type u} (g : β → F (α.append1 (Cofix F α ⊕ β))) (x : β) :
Cofix.dest (Cofix.corec' g x) = appendFun id (Sum.elim _root_.id (Cofix.corec' g)) <$$> g x :=
by
rw [Cofix.corec', Cofix.dest_corec]; dsimp
congr!; ext (i | i) <;> erw [corec_roll] <;> dsimp [Cofix.corec']
· mv_bisim i with R a b x Ha Hb
rw [Ha, Hb, Cofix.dest_corec]
dsimp [Function.comp_def]
repeat rw [MvFunctor.map_map, ← appendFun_comp_id]
apply liftR_map_last'
dsimp [Function.comp_def]
intros
exact ⟨_, rfl, rfl⟩
· congr 1 with y
erw [appendFun_id_id]
simp [MvFunctor.id_map, Sum.elim]
