proposition: Lemma Book_3_4_solution_1 `{Funext} (A : Type) : IsHProp A <-> Contr (A -> A).
proof: Proof. split. - intro isHProp_A. apply (Build_Contr _ idmap). apply path_ishprop. - intro contr_AA. apply hprop_allpath; intros a1 a2. exact (ap10 (path_contr (fun x:A => a1) (fun x:A => a2)) a1). 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)