HProp = Bool. Proof. apply path_universe_uncurried. srapply equiv_adjointify. - exact (fun P => if LEM P _ then true else false). - exact (fun b : Bool => if b then merely Unit else merely Empty). - intros []; destruct LEM as [H|H]; auto. + destruct (H (tr tt)). + apply (@merely_destruct Empty); try done. exact _. - intros P. destruct LEM as [H|H]; apply equiv_path_iff_hprop. + split; auto. intros _. apply tr. exact tt. + split; try done. intros HE. apply (@merely_destruct Empty); try done. exact _. 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.