X (p : X -> HProp) : X = sig p + sig (fun x => ~ p x). Proof. apply path_universe_uncurried. srapply equiv_adjointify. - intros x. destruct (LEM (p x) _) as [H|H]; [left | right]; by exists x. - intros [[x _]|[x _]]; exact x. - cbn. intros [[x Hx]|[x Hx]]; destruct LEM as [H|H]; try contradiction. + enough (H = Hx) as -> by reflexivity. apply path_ishprop. + enough (H = Hx) as -> by reflexivity. apply path_forall. by intros HP. - cbn. intros x. by destruct LEM. 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.