proposition: Fact path_infinite_power (X : HSet) : infinite X -> (X -> HProp) + (X -> HProp) = (X -> HProp).
proof: Proof. intros H. rewrite path_sum_bool. rewrite <- path_bool_subsingleton. rewrite path_sum_prod. now rewrite path_infinite_unit. 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)