equiv_path_dhprop' `{Funext} (P Q : DHProp) : (P = Q :> HProp) <~> (P = Q :> DHProp). Proof. destruct P as [P dP]. destruct Q as [Q dQ]. refine (((equiv_ap' issig_dhprop^-1 _ _)^-1) oE _); cbn. refine ((equiv_path_sigma_hprop (P; dP) (Q; dQ))). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HProp. Require Import Truncations.Core Modalities.ReflectiveSubuniverse.