proposition: Lemma isfibseqpr1 {Z : UU} (P : Z -> UU) (z : Z) : isfibseq (λ p : P z, tpair _ z p) (@pr1 Z P) z (λ p : P z, idpath z).
proof: Proof. intros. unfold isfibseq. unfold ezmap. apply isweqezmappr1. Defined.
imports: UniMath.Foundations.Preamble