{A B I i j} (l : I) : IW I A B i j l -> hfiber i l. Proof. intros w. exists (iw_label w). apply path_index_iw_label. Defined.
Require Import Basics. Require Import Types.Forall Types.Sigma Types.Prod Types.WType.