case refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
x : PFunctor.M (last P)
a₁ : P.A
f₁ : PFunctor.B (last P) a₁ → PFunctor.M (last P)
h₁ : PFunctor.M.dest x = { fst := a₁, snd := f₁ }
f' : Path P x ⟹ α
h₂ : PFunctor.M.dest x = { fst := a₁, snd := f₁ }
⊢ dest' P h₁ f' = dest' P h₂ f'
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
x : PFunctor.M (last P)
a₁ : P.A
f₁ : PFunctor.B (last P) a₁ → PFunctor.M (last P)
h₁ : PFunctor.M.dest x = { fst := a₁, snd := f₁ }
a₂ : P.A
f₂ : PFunctor.B (last P) a₂ → PFunctor.M (last P)
h₂ : PFunctor.M.dest x = { fst := a₂, snd := f₂ }
f' : Path P x ⟹ α
⊢ dest' P h₁ f' = dest' P h₂ f'
cases h₁.symm.trans h₂
no goals
case refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
x : PFunctor.M (last P)
a₁ : P.A
f₁ : PFunctor.B (last P) a₁ → PFunctor.M (last P)
h₁ : PFunctor.M.dest x = { fst := a₁, snd := f₁ }
f' : Path P x ⟹ α
h₂ : PFunctor.M.dest x = { fst := a₁, snd := f₁ }
⊢ dest' P h₁ f' = dest' P h₂ f'
rfl