proposition: Lemma idisweq (T : UU) : isweq (idfun T).
proof: 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.
imports: UniMath.Foundations.Preamble