{ dprop_type : Type ; ishprop_dprop : Funext -> IsHProp dprop_type ; dec_dprop : Decidable dprop_type }.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HProp. Require Import Truncations.Core Modalities.ReflectiveSubuniverse.