transport_path_universe' {A : Type} (P : A -> Type) {x y : A} (p : x = y) (f : P x <~> P y) (q : ap P p = path_universe f) (u : P x) : transport P p u = f u := transport_compose idmap P p u @ ap10 (ap (transport idmap) q) u @ transport_path_universe f u.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.