`{Funext} (x : I) : IW' x <~> IW I A B i j x. Proof. snrapply equiv_adjointify. { rapply (IW'_ind (fun l _ => IW I A B i j l)). intros a b c. apply iw_sup. intros y. apply c. } { rapply (IW_rect I A B i j (fun l _ => IW' l)). intros a b c. apply iw_sup'. intros y. apply c. } { rapply (IW_rect I A B i j (fun x y => IW'_ind _ _ x _ = y)). cbn; intros a b c. apply ap. funext y. apply c. } simpl. intro y. rapply (IW'_ind (fun x y => IW_rect I A B i j _ _ x _ = y)). cbn; intros a b c. apply ap. funext d. apply c. Defined.
Require Import Basics. Require Import Types.Forall Types.Sigma Types.Prod Types.WType.