wRec — Mathlib

English

Recursor for the W-type: any motive over W can be computed by recursively applying wpRec to the children via wPathDestRight.

Русский

Рекурсор для W-типа: любой мотив над W вычисляется рекурсивно через детей через wPathDestRight.

LaTeX

$$$wRec {\alpha} {P} {C} (g) : P.W α → C$$$

Lean4

/-- Recursor for `W` -/
def wRec {α : TypeVec n} {C : Type*} (g : ∀ a : P.A, P.drop.B a ⟹ α → (P.last.B a → P.W α) → (P.last.B a → C) → C) :
    P.W α → C
  | ⟨a, f'⟩ =>
    let g' (a : P.A) (f : P.last.B a → P.last.W) (h : P.WPath ⟨a, f⟩ ⟹ α) (h' : P.last.B a → C) : C :=
      g a (P.wPathDestLeft h) (fun i => ⟨f i, P.wPathDestRight h i⟩) h'
    P.wpRec g' a f'

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