`(P : A -> Type) (u v : sig P) : {p : u.1 = v.1 & p # u.2 = v.2} <~> (u = v) := Build_Equiv _ _ (path_sigma_uncurried P u v) _. Global Instance isequiv_path_sigma_contra `{P : A -> Type} {u v : sig P} : IsEquiv (path_sigma_uncurried_contra P u v) | 0. Proof. apply (isequiv_adjointify (path_sigma_uncurried_contra P u v) (fun r => match r with idpath => (1; 1) end)). - by intro r; induction r; destruct u as [u1 u2]; reflexivity. - destruct u, v; intros [p q]. simpl in *. destruct p; simpl in q. destruct q; reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.