∀ {F : Type u → Type v} [q : QPF F] (a : (QPF.P F).A) (f : (QPF.P F).B a → (QPF.P F).W) (a' : (QPF.P F).A)
  (f' : (QPF.P F).B a' → (QPF.P F).W), QPF.abs ⟨a, f⟩ = QPF.abs ⟨a', f'⟩ → QPF.Wequiv (WType.mk a f) (WType.mk a' f')