English
Let P be a multivariate functor in arity n+1. Given g0: β → P.A, g1 and g2 providing the recursive structure, the destination of the corec' construction at x is the pair consisting of g0 x and a compatible split of the recursive part, namely splitFun (g1 x) (corec' P g0 g1 g2 ∘ g2 x).
Русский
Пусть P — многовариантный функтор arity n+1. Пусть g0: β → P.A, g1 и g2 задают рекурсивную структуру. Тогда разрушение уcorec' в точке x равно паре: (g0 x, splitFun (g1 x) (corec' P g0 g1 g2 ∘ g2 x)).
LaTeX
$$$\forall {\alpha : TypeVec n} \ {\beta : Type u} \ (g0 : β \to P.A) \ (g1 : \forall b, P.drop.B (g0 b) \Rightarrow \alpha) \ (g2 : \forall b, P.last.B (g0 b) \to \beta) \ (x : β), \\ M.dest P (M.corec' P g0 g1 g2 x) = ⟨g0 x, splitFun (g1 x) (M.corec' P g0 g1 g2 ∘ g2 x)\rangle$$
Lean4
theorem dest_corec' {α : TypeVec.{u} n} {β : Type u} (g₀ : β → P.A) (g₁ : ∀ b : β, P.drop.B (g₀ b) ⟹ α)
(g₂ : ∀ b : β, P.last.B (g₀ b) → β) (x : β) :
M.dest P (M.corec' P g₀ g₁ g₂ x) = ⟨g₀ x, splitFun (g₁ x) (M.corec' P g₀ g₁ g₂ ∘ g₂ x)⟩ :=
rfl
