`{P : A -> Type} `{forall a, IsHProp (P a)} : (forall x y, P x -> P y -> x = y) -> IsHProp { x : A & P x }. Proof. intros dj; apply hprop_allpath; intros [x px] [y py]. refine (path_sigma' P (dj x y px py) _). apply path_ishprop. Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.