(x : I) (a b : IW I A B i j x) : IW I' A' B' i' j' (x; (a, b)) <~> a = b. Proof. change (IW I' A' B' i' j' (x; (a, b)) <~> IWPath (x; (a,b))). snrapply equiv_adjointify. { intros y. induction y as [e f g]. apply iwpath_sup. intros y. apply g. } { intros y. induction y as [e f g] using IWPath_ind. apply iw_sup. intros y. apply g. } { intros y; cbn. induction y as [a' b' IH] using IWPath_ind. rewrite IWPath_ind_beta_iwpath_sup. simpl; f_ap. funext c. apply IH. } intros y; cbn. induction y as [e f IH]. rewrite IWPath_ind_beta_iwpath_sup. f_ap; funext c. apply IH. Defined.
Require Import Basics. Require Import Types.Forall Types.Sigma Types.Prod Types.WType.