transport_path_prod' {A B} (P : A * B -> Type) {x y : A} {x' y' : B} (HA : x = y) (HB : x' = y') (Px : P (x,x')) : transport P (path_prod' HA HB) Px = transport (fun x => P (x, y')) HA (transport (fun y => P (x, y)) HB Px) := @transport_path_prod _ _ P (x, x') (y, y') HA HB Px. Global Instance isequiv_path_prod {A B : Type} {z z' : A * B} : IsEquiv (path_prod_uncurried z z') | 0. Proof. refine (Build_IsEquiv _ _ _ (fun r => (ap fst r, ap snd r)) eta_path_prod (fun pq => path_prod' (ap_fst_path_prod (fst pq) (snd pq)) (ap_snd_path_prod (fst pq) (snd pq))) _). destruct z as [x y], z' as [x' y']. intros [p q]; simpl in p, q. destruct p, q; reflexivity. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.