fact: Definition path_universe_uncurried_transport_idmap {A B : Type} (p : A = B) : path_universe_uncurried (equiv_transport idmap p) = p := eissect (equiv_path A B) p.
imports: HoTT.Basics Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod