A B P Q `{forall a b, IsHProp (Q a b)} (x : { a : A & { b : B a & P a b /\ Q a b }}) q' : (x.1; (x.2.1; (fst x.2.2, q'))) = x. Proof. destruct x as [? [? [? ?]]]; cbn in *. repeat f_ap; apply path_ishprop. Defined.
Require Import Category.Core. Require Import HoTT.Basics.Equivalences HoTT.Basics.PathGroupoids HoTT.Basics.Trunc HoTT.Basics.Tactics. Require Import HoTT.Types.Sigma HoTT.Types.Arrow HoTT.Types.Forall. Require Import HoTT.Tactics.