proposition: Lemma Book_3_9_solution_1 `{Univalence} : LEM -> HProp <~> Bool.
proof: Proof. intro lem. apply (equiv_adjointify (LEM_hProp_Bool lem) is_true). - intros []; simpl. + unfold LEM_hProp_Bool. elim (lem Unit_hp _). * exact (fun _ => 1). * intro nUnit. elim (nUnit tt). + unfold LEM_hProp_Bool. elim (lem False_hp _). * intro fals. elim fals. * exact (fun _ => 1). - intro hprop. unfold LEM_hProp_Bool. elim (lem hprop _). + intro p. apply path_hprop; simpl. exact ((if_hprop_then_equiv_Unit hprop p)^-1)%equiv. + intro np. apply path_hprop; simpl. exact ((if_not_hprop_then_equiv_Empty hprop np)^-1)%equiv. Defined.
imports: HoTT(Basics Types HProp HSet Projective TruncType Truncations Modalities.Notnot Modalities.Open Modalities.Closed BoundedSearch Equiv.BiInv Spaces.Nat Spaces.Torus.TorusEquivCircles Metatheory.Core Metatheory.FunextVarieties)