`{Funext} (P Q : DProp) : (P = Q :> Type) <~> (P = Q :> DProp). Proof. destruct P as [P hP dP]. destruct Q as [Q hQ dQ]. refine (((equiv_ap' issig_dprop^-1 _ _)^-1) oE _); cbn. refine ((equiv_ap' (equiv_sigma_assoc' _ _)^-1 ((P;hP);dP) ((Q;hQ);dQ)) oE _). refine (equiv_path_sigma_hprop _ _ oE _); cbn. { intros [X hX]; exact _. } refine (equiv_path_sigma_hprop (P;hP) (Q;hQ)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HProp. Require Import Truncations.Core Modalities.ReflectiveSubuniverse.