proposition: Lemma eta2_sigma_helper 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: Proof. destruct x as [? [? [? ?]]]; cbn in *. repeat f_ap; apply path_ishprop. Defined.
imports: Category.Core HoTT.Basics.Equivalences HoTT.Basics.PathGroupoids HoTT.Basics.Trunc HoTT.Basics.Tactics HoTT.Types.Sigma HoTT.Types.Arrow HoTT.Types.Forall HoTT.Tactics