(b : Bool) : HProp := if b then Unit_hp else False_hp. Global Instance trunc_path_IsHProp X Y `{IsHProp Y} : IsHProp (X = Y). Proof. apply hprop_allpath. intros pf1 pf2. apply (equiv_inj (equiv_path X Y)). apply path_equiv, path_arrow. intros x; by apply path_ishprop. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import HProp.