proposition: Lemma Book_3_1_solution_3 {A B} : A <~> B -> IsHSet A -> IsHSet B.
proof: Proof. intros equivalent_A_B isHSet_A. elim equivalent_A_B; intros f isequiv_f. elim isequiv_f; intros g retr_f_g sect_f_g coh. apply (retr_f_g_isHSet_A_so_B f g); assumption. 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)