fact: Definition pr2_path_sigma `{P : A -> Type} {u v : sig P} (p : u.1 = v.1) (q : p # u.2 = v.2) : (path_sigma _ _ _ p q)..2 = ap (fun s => transport P s u.2) (pr1_path_sigma p q) @ q := pr2_path_sigma_uncurried (p; q).
imports: HoTT.Basics Types.Arrow Types.Paths