proposition: Lemma Book_3_3_solution_2 (A : Type) (B : A -> Type) : IsHSet A -> (forall x:A, IsHSet (B x)) -> IsHSet { x:A | B x}.
proof: Proof. intros isHSet_A allBx_HSet. srapply hset_axiomK. intros x xx. pose (path_path_sigma B x x xx 1) as useful. apply (useful (axiomK_hset _ _ _) (hset_path2 _ _)). 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)