Definition isweqezmappr1 {Z : UU} (P : Z -> UU) (z : Z) : isweq (ezmappr1 P z). Proof. intros. assert (egf : ∏ x: P z , (invezmappr1 _ z ((ezmappr1 P z) x)) = x). intro. unfold ezmappr1. unfold invezmappr1. simpl. apply idpath. assert (efg : ∏ x: hfiber (@pr1 Z P) z , (ezmappr1 _ z (invezmappr1 P z x)) = x). intros. induction x as [ x t0 ]. induction t0. simpl in x. simpl. induction x. simpl. unfold transportf. unfold ezmappr1. apply idpath. apply (isweq_iso _ _ egf efg). Defined.