n : ℕ
P : MvPFunctor (n + 1)
α γ : TypeVec n
g : α ⟹ γ
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ { fst := a, snd := splitFun (g ⊚ f') (wMap P g ∘ f) } = { fst := a, snd := splitFun (g ⊚ f') fun x => wMap P g (f x) }
n : ℕ
P : MvPFunctor (n + 1)
α γ : TypeVec n
g : α ⟹ γ
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ (g ::: wMap P g) <$$> objAppend1 P a f' f = objAppend1 P a (g ⊚ f') fun x => wMap P g (f x)
rw [objAppend1, objAppend1, map_eq, appendFun, ← splitFun_comp]
no goals
n : ℕ
P : MvPFunctor (n + 1)
α γ : TypeVec n
g : α ⟹ γ
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ { fst := a, snd := splitFun (g ⊚ f') (wMap P g ∘ f) } = { fst := a, snd := splitFun (g ⊚ f') fun x => wMap P g (f x) }
rfl