n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ (match
      let g := fun i => (f i).fst;
      let g' := wPathCasesOn P f' fun i => (f i).snd;
      { fst := WType.mk a g, snd := g' } with
    | { fst := a, snd := f' } =>
      let g' := fun a f h h' => g a (wPathDestLeft P h) (fun i => { fst := f i, snd := wPathDestRight P h i }) h';
      wpRec P g' a f') =
    g a f' f fun i => wRec P g (f i)
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ wRec P g (wMk P a f' f) = g a f' f fun i => wRec P g (f i)
rw [wMk, wRec]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ wpRec P (fun a f h h' => g a (wPathDestLeft P h) (fun i => { fst := f i, snd := wPathDestRight P h i }) h')
      (WType.mk a fun i => (f i).fst) (wPathCasesOn P f' fun i => (f i).snd) =
    g a f' f fun i => wRec P g (f i)
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ (match
      let g := fun i => (f i).fst;
      let g' := wPathCasesOn P f' fun i => (f i).snd;
      { fst := WType.mk a g, snd := g' } with
    | { fst := a, snd := f' } =>
      let g' := fun a f h h' => g a (wPathDestLeft P h) (fun i => { fst := f i, snd := wPathDestRight P h i }) h';
      wpRec P g' a f') =
    g a f' f fun i => wRec P g (f i)
dsimp
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ (g a (wPathDestLeft P (wPathCasesOn P f' fun i => (f i).snd))
      (fun i => { fst := (f i).fst, snd := wPathDestRight P (wPathCasesOn P f' fun i => (f i).snd) i }) fun i =>
      wpRec P (fun a f h h' => g a (wPathDestLeft P h) (fun i => { fst := f i, snd := wPathDestRight P h i }) h')
        (f i).fst (wPathDestRight P (wPathCasesOn P f' fun i => (f i).snd) i)) =
    g a f' f fun i => wRec P g (f i)
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ wpRec P (fun a f h h' => g a (wPathDestLeft P h) (fun i => { fst := f i, snd := wPathDestRight P h i }) h')
      (WType.mk a fun i => (f i).fst) (wPathCasesOn P f' fun i => (f i).snd) =
    g a f' f fun i => wRec P g (f i)
rw [wpRec_eq]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ (g a f' (fun i => { fst := (f i).fst, snd := (f i).snd }) fun i =>
      wpRec P (fun a f h h' => g a (wPathDestLeft P h) (fun i => { fst := f i, snd := wPathDestRight P h i }) h')
        (f i).fst (f i).snd) =
    g a f' f fun i => wRec P g (f i)
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ (g a (wPathDestLeft P (wPathCasesOn P f' fun i => (f i).snd))
      (fun i => { fst := (f i).fst, snd := wPathDestRight P (wPathCasesOn P f' fun i => (f i).snd) i }) fun i =>
      wpRec P (fun a f h h' => g a (wPathDestLeft P h) (fun i => { fst := f i, snd := wPathDestRight P h i }) h')
        (f i).fst (wPathDestRight P (wPathCasesOn P f' fun i => (f i).snd) i)) =
    g a f' f fun i => wRec P g (f i)
dsimp only [wPathDestLeft_wPathCasesOn, wPathDestRight_wPathCasesOn]
no goals
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ (g a f' (fun i => { fst := (f i).fst, snd := (f i).snd }) fun i =>
      wpRec P (fun a f h h' => g a (wPathDestLeft P h) (fun i => { fst := f i, snd := wPathDestRight P h i }) h')
        (f i).fst (f i).snd) =
    g a f' f fun i => wRec P g (f i)
congr