(A :Type) `{IsHProp A} `{Decidable A} `{Univalence} : A = is_inl (dec A). Proof. refine (path_universe_uncurried _). apply equiv_iff_hprop_uncurried. split. - intros b. destruct (dec A); simpl; auto. - destruct (dec A); simpl; auto. intros []. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HProp. Require Import Truncations.Core Modalities.ReflectiveSubuniverse.