Lemma idisweq (T : UU) : isweq (idfun T). Proof. intros. unfold isweq. intro y. unfold iscontr. split with (make_hfiber (idfun T) y (idpath y)). intro t. induction t as [x e]. induction e. apply idpath. Defined.