proposition: Theorem onefiber {X : UU} (P : X -> UU) (x : X) (c : ∏ x' : X, (x = x') ⨿ ¬ P x') : isweq (λ p, tpair P x p).
proof: Proof. intros. set (f := λ p : P x, tpair _ x p). set (cx := c x). transparent assert (cnew : (∏ x' : X, (x = x') ⨿ ¬ P x')). { intro x'. refine (coprod_rect (λ _, _) _ _ (cx)). - intro x0. refine (coprod_rect (λ _, _) _ _ (c x')). + intro ee. apply ii1; exact (pathscomp0 (pathsinv0 x0) ee). + intro phi. apply ii2, phi. - intro phi. exact (c x'). } set (g := λ pp : total2 P, match (cnew (pr1 pp)) with | ii1 e => transportb P e (pr2 pp) | ii2 phi => fromempty (phi (pr2 pp)) end). assert (efg : ∏ pp : total2 P, (f (g pp)) = pp). intro. induction pp as [ t x0 ]. set (cnewt := cnew t). unfold g. unfold f. simpl. change (cnew t) with cnewt. induction cnewt as [ x1 | y ]. apply (pathsinv0 (pr1 (pr2 (constr1 P (pathsinv0 x1))) x0)). induction (y x0). set (cnewx := cnew x). assert (e1 : (cnew x) = cnewx). apply idpath. unfold cnew in cnewx. change (c x) with cx in cnewx. induction cx as [ x0 | e0 ]. assert (e : (cnewx) = (ii1 (idpath x))). apply (maponpaths (@ii1 (x = x) (P x -> empty)) (pathsinv0l x0)). assert (egf : ∏ p: P x, (g (f p)) = p). intro. simpl in g. unfold g. unfold f. simpl. set (ff := λ cc:(x = x) ⨿ (P x -> empty), match cc with | ii1 e0 => transportb P e0 p | ii2 phi => fromempty (phi p) end). assert (ee : (ff (cnewx)) = (ff (@ii1 (x = x) (P x -> empty) (idpath x)))). apply (maponpaths ff e). assert (eee : (ff (@ii1 (x = x) (P x -> empty) (idpath x))) = p). apply idpath. fold (ff (cnew x)). assert (e2 : (ff (cnew x)) = (ff cnewx)). apply (maponpaths ff e1). apply (pathscomp0 (pathscomp0 e2 ee) eee). apply (isweq_iso f g egf efg). unfold isweq. intro y0. induction (e0 (g y0)). Defined.
imports: UniMath.Foundations.Preamble