(l : I) (a b : IW I A B i j l) : iw_to_hfiber_index l a = iw_to_hfiber_index l b <~> hfiber i' (l; (a, b)). Proof. srapply equiv_adjointify. + apply path_iw_to_hfiber. + apply hfiber_to_path_iw. + rapply path_iw_to_hfiber_to_path_iw. + rapply hfiber_to_path_iw_to_hfiber. Defined.
Require Import Basics. Require Import Types.Forall Types.Sigma Types.Prod Types.WType.