case a.h
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : TypeVec n
h : α ⟹ β
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
i : Fin2 n
x : WPath P (WType.mk a fun j => f j) i
⊢ (h ⊚ wPathCasesOn P g' g) i x = wPathCasesOn P (h ⊚ g') (fun i => h ⊚ g i) i x
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : TypeVec n
h : α ⟹ β
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
⊢ h ⊚ wPathCasesOn P g' g = wPathCasesOn P (h ⊚ g') fun i => h ⊚ g i
ext (i x)
no goals
case a.h
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : TypeVec n
h : α ⟹ β
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
i : Fin2 n
x : WPath P (WType.mk a fun j => f j) i
⊢ (h ⊚ wPathCasesOn P g' g) i x = wPathCasesOn P (h ⊚ g') (fun i => h ⊚ g i) i x
cases x <;> rfl