Lemma iscontrhfibereqbx (X : UU) (x : X) (is : isisolated X x) : iscontr (hfiber (eqbx X x is) true). Proof. intros. assert (b : (eqbx X x is x) = true). { unfold eqbx. induction (is x) as [ e | ne ]. - apply idpath. - induction (ne (idpath _)). } set (i := make_hfiber (eqbx X x is) x b). split with i. unfold eqbx. induction (boolchoice (eqbx X x is x)) as [ b' | nb' ]. - intro t. induction t as [ x' e ]. assert (e' : x' = x). { induction (is x') as [ ee | nee ]. apply (pathsinv0 ee). induction (nopathsfalsetotrue e) . } apply (invmaponpathsincl _ (isinclfromhfiber (eqbx X x is) isasetbool true) (make_hfiber _ x' e) i e'). - induction (nopathstruetofalse (pathscomp0 (pathsinv0 b) nb')). Defined.