proposition: Lemma path_dec (A :Type) `{IsHProp A} `{Decidable A} `{Univalence} : A = is_inl (dec A).
proof: 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.
imports: HoTT.Basics HoTT.Types TruncType HProp Truncations.Core Modalities.ReflectiveSubuniverse