corecShape — Mathlib

English

Construct through corecursion the shape of an M-type from a given P using a seed g0 and a next-step function g2.

Русский

Сконструировать форму M‑типа через коррекурсию из заданного P с семенем g0 и функцией перехода g2.

LaTeX

$$$\\text{corecShape} : (g_0 : β \\to P.A) \\to (g_2 : ∀ b, P.last.B (g_0 b) \\to β) \\to β \\to P.last.M$$$

Lean4

/-- construct through corecursion the shape of an M-type
without its contents -/
def corecShape {β : Type u} (g₀ : β → P.A) (g₂ : ∀ b : β, P.last.B (g₀ b) → β) : β → P.last.M :=
  PFunctor.M.corec fun b => ⟨g₀ b, g₂ b⟩

Похожие утверждения