proposition: Lemma path_bool_subsingleton : (Unit -> HProp) = Bool.
proof: Proof. rewrite <- path_unit_fun. apply path_bool_prop. Qed.
imports: HoTT(TruncType ExcludedMiddle abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Spaces.Nat.Core Spaces.Card) HoTT(Equiv.BiInv) HoTT(HIT.unique_choice) HoTT.Sets(Ordinals Hartogs Powers GCH AC)