English
Let F be a polynomial functor and X a type. Given a map f : X → F X, the operation sCorec f defines, for each i ∈ X and each height n, an approximation of the final coalgebra of F of height n. The height-0 approximation is the trivial continue state, and the height n+1 approximation is built from the head provided by f i and a recursive call on the tail (f i).2 j with the inner index j.
Русский
Пусть F — полином-функтор и X — множество. Пусть f : X → F X. Тогда sCorec f задаёт, для каждого элемента i ∈ X и высоты n, приближение финальной коалгебры F до высоты n. При высоте 0 получаем элемент-«продолжение»; при высоте n+1 конструируем новое приближение из головы, заданной f i, и рекурсивного вызова на хвостовую часть через (f i).2 j.
LaTeX
$$$\\displaystyle sCorec\\ f\\ i\\ 0 = \\operatorname{CofixA.continue}, \\quad sCorec\\ f\\ i\\ (\\operatorname{succ} n) = \\operatorname{CofixA.intro}\\big((f\\ i).1\\big)\\,\\big(\\lambda j.\\, sCorec\\ f\\ ((f\\ i).2\\ j)\\ n\\big).$$$
Lean4
/-- `sCorec f i n` creates an approximation of height `n`
of the final coalgebra of `f` -/
def sCorec : X → ∀ n, CofixA F n
| _, 0 => CofixA.continue
| j, succ _ => CofixA.intro (f j).1 fun i => sCorec ((f j).2 i) _
