equiv_path_wtype' {A B} (z z' : W A B) : {p : w_label z = w_label z' & w_arg z = w_arg z' o transport B p} <~> z = z'. Proof. refine (equiv_path_wtype _ _ oE equiv_path_sigma _ _ _ oE _). apply equiv_functor_sigma_id. destruct z as [z1 z2], z' as [z1' z2']. cbn; intros p. destruct p. reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Forall Types.Sigma.