fact: Definition equiv_path_wtype {A B} (z z' : W A B) : (w_label z;w_arg z) = (w_label z';w_arg z') :> {a : _ & B a -> W A B} <~> z = z' := (equiv_ap' (issig_W A B)^-1%equiv z z')^-1%equiv.
imports: HoTT.Basics Types.Forall Types.Sigma