fact: Definition transport_path_universe_V_equiv_path {A B : Type} (p : A = B) (z : B) : transport_path_universe_V (equiv_path A B p) z = ap (fun s => transport idmap s z) (inverse2 (eissect _ p)) := equiv_ind_comp _ _ _.
imports: HoTT.Basics Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod