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