{ X : Type & { _ : Funext -> IsHProp X & Decidable X } } <~> DProp. Proof. issig. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HProp. Require Import Truncations.Core Modalities.ReflectiveSubuniverse.