(hprop : Type) `{IsHProp hprop} `{Decidable hprop} : (hprop <~> Unit) + (hprop <~> Empty). Proof. destruct (dec hprop) as [x|nx]. - exact (inl (if_hprop_then_equiv_Unit hprop x)). - exact (inr (if_not_hprop_then_equiv_Empty hprop nx)). Defined.
Require Import HoTT.Basics HoTT.Types.