Corollary isweqpr1pr1 (T : UU) : isweq (λ (a : pathsspace' T), pr1 (pr1 a)). Proof. intros. set (f := λ (a : pathsspace' T), pr1 (pr1 a)). set (g := λ (t : T), tpair _ (make_dirprod t t) (idpath t) : pathsspace' T). assert (efg : ∏ t : T, f (g t) = t). { intros t. unfold f. unfold g. simpl. apply idpath. } assert (egf : ∏ a : _, g (f a) = a). { intros a. induction a as [xy e]. induction xy as [x y]. simpl in e. induction e. unfold f. unfold g. apply idpath. } apply (isweq_iso _ _ egf efg). Defined.