proposition: Lemma Book_3_13 `{Funext} : (forall A : Type, A + ~A) -> forall X A P, IsHSet X -> (forall x : X, IsHSet (A x)) -> (forall x (a : A x), IsHProp (P x a)) -> (forall x, merely { a : A x & P x a }) -> merely { g : forall x, A x & forall x, P x (g x) }.
proof: Proof. intros LEM X A P HX HA HP H0. apply tr. apply (naive_LEM_implies_AC LEM). intro x. specialize (H0 x). revert H0. apply Trunc_rec. exact (fun x nx => nx x). 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)