English
Let F be a multivariate functor and Cofix F α its greatest fixed point. For any type X and any g with the appropriate compatibility, the value obtained by destructing the corecursive object built via corec₁ equals the application of g to the identity map and the corec₁ map, evaluated at x. This is the corecursion principle for Cofix.
Русский
Пусть F — многоарный функтор и Cofix F α — его наибольший фиксированный точкой. Пусть для произвольного типа X и соответствующей совместимости функция g задаёт корректное отображение; тогда деструктор объекта, полученного при помощи corec₁ g x, равен применению g к идентичности и к функции corec₁ g, применённой к x. Это принцип корекурсии Cofix.
LaTeX
$$$\operatorname{Cofix.dest}(\operatorname{Cofix.corec}_1(g)\,x) = g(\operatorname{id},\ \operatorname{Cofix.corec}_1(g),\ x).$$$
Lean4
theorem dest_corec₁ {α : TypeVec n} {β : Type u} (g : ∀ {X}, (Cofix F α → X) → (β → X) → β → F (α.append1 X)) (x : β)
(h : ∀ (X Y) (f : Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = (id ::: k) <$$> g f f' x) :
Cofix.dest (Cofix.corec₁ (@g) x) = g id (Cofix.corec₁ @g) x := by rw [Cofix.corec₁, Cofix.dest_corec', ← h]; rfl
