(x : A') : (forall y : B' x, IWPath (j' x y)) -> IWPath (i' x). Proof. destruct x as [x [c1 c2]]. intros y. unfold IWPath. cbn; apply ap. funext l. apply y. Defined.
Require Import Basics. Require Import Types.Forall Types.Sigma Types.Prod Types.WType.