Lemma isweqpr1 {Z : UU} (P : Z -> UU) (is1 : ∏ z : Z, iscontr (P z)) : isweq (@pr1 Z P). Proof. intros. unfold isweq. intro y. set (isy := is1 y). apply (iscontrweqf (ezweqpr1 P y)). assumption. Defined.