(X : HSet) : infinite X -> Unit + X = X. Proof. intros [f Hf]. rewrite (@path_pred_sum X (ran f)). rewrite (path_ran _ Hf). rewrite path_sum_assoc. rewrite path_unit_nat. reflexivity. Qed.
From HoTT Require Import TruncType ExcludedMiddle abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Nat.Core Spaces.Card. From HoTT Require Import Equiv.BiInv. From HoTT Require Import HIT.unique_choice. From HoTT.Sets Require Import Ordinals Hartogs Powers GCH AC.