Lemma sum_of_fibers {A B:Type} (f: A -> B) : (∑ b:B, hfiber f b) ≃ A. Proof. use make_weq. - intro bap. exact (pr1 (pr2 bap)). - intro a. use make_iscontr. + use make_hfiber. * exists (f a). use make_hfiber. { exact a. } { reflexivity. } * cbn. reflexivity. + intro b1a1p1p. induction b1a1p1p as [b1a1p1 p]. induction p. induction b1a1p1 as [b1 [a1 p1]]. induction p1. reflexivity. Defined.