Lemma centralfiber {X : UU} (P : X -> UU) (x : X) : isweq (λ p : P x, tpair (λ u : coconusfromt X x, P (pr1 u)) (coconusfromtpair X (idpath x)) p). Proof. intros. set (f := λ p: P x, tpair (λ u: coconusfromt X x, P(pr1 u)) (coconusfromtpair X (idpath x)) p). set (g := λ z: total2 (λ u: coconusfromt X x, P (pr1 u)), transportf P (pathsinv0 (pr2 (pr1 z))) (pr2 z)). assert (efg : ∏ z : total2 (λ u : coconusfromt X x, P (pr1 u)), (f (g z)) = z). intro. induction z as [ t x0 ]. induction t as [ t x1 ]. simpl. induction x1. simpl. apply idpath. assert (egf : ∏ p : P x , (g (f p)) = p). intro. apply idpath. apply (isweq_iso f g egf efg). Defined.