Lemma surjective_iscontr_im : ∏ b : B, iscontr (image (λ (x:hfiber p b), f (pr1 x))). Proof. intro b. apply (squash_to_prop (surjectivep b)). { apply isapropiscontr. } intro H. apply iscontraprop1. - apply isapropsubtype. intros x1 x2. apply (@hinhuniv2 _ _ (make_hProp _ (hsc _ _))). simpl; intros y1 y2; simpl. induction y1 as [ [z1 h1] h1' ]. induction y2 as [ [z2 h2] h2' ]. rewrite <- h1' ,<-h2'. apply comp_f_epi;simpl. rewrite h1,h2. apply idpath. - apply prtoimage. apply H. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.