proposition: Lemma if_hprop_then_equiv_Unit (hprop : Type) `{IsHProp hprop} : hprop -> hprop <~> Unit.
proof: Proof. intro p. apply equiv_iff_hprop. - exact (fun _ => tt). - exact (fun _ => p). Defined.
imports: HoTT.Basics HoTT.Types