Corollary isweqdeltap (T : UU) : isweq (deltap T). Proof. intros. set (ff := deltap T). set (gg := λ (z : pathsspace T), pr1 z). assert (egf : ∏ t : T, gg (ff t) = t). { intro. apply idpath. } assert (efg : ∏ (tte : _), ff (gg tte) = tte). { intro tte. induction tte as [t c]. induction c as [x e]. induction e. apply idpath. } apply (isweq_iso _ _ egf efg). Defined.