English
Compatibility of map with the W-constructor: applying g to a wMk node equals building a new node with g applied along the tail.
Русский
Совместимость отображения с конструктором W: применение g к узлу wMk равно построению нового узла с применением g к хвосту.
LaTeX
$$$ g <$$> P.wMk\ a f' f = P.wMk a (g \circ f') (\lambda i. g <$$> f i). $$$
Lean4
theorem w_map_wMk {α β : TypeVec n} (g : α ⟹ β) (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α) :
g <$$> P.wMk a f' f = P.wMk a (g ⊚ f') fun i => g <$$> f i :=
by
change _ = P.wMk a (g ⊚ f') (MvFunctor.map g ∘ f)
have : MvFunctor.map g ∘ f = fun i => ⟨(f i).fst, g ⊚ (f i).snd⟩ :=
by
ext i : 1
dsimp [Function.comp_def]
cases f i
rfl
rw [this]
have : f = fun i => ⟨(f i).fst, (f i).snd⟩ := by
ext1 x
cases f x
rfl
rw [this]
dsimp
rw [wMk_eq, wMk_eq]
have h := MvPFunctor.map_eq P.wp g
rw [h, comp_wPathCasesOn]
-- TODO: this technical theorem is used in one place in constructing the initial algebra.
-- Can it be avoided?
