proposition: Lemma Book_7_1_part_ii (H : forall A B (f : A -> B), (forall b, merely (hfiber f b)) -> forall b, hfiber f b) : forall A, IsHSet A.
proof: Proof. apply Book_7_1_part_i. intros A a. apply (fun H' => (@H A (merely A) tr H' a).1). clear a. apply Trunc_ind; try exact _. intro x; compute; apply tr. exists x; reflexivity. 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)