proposition: Lemma isweqcontrtounit {T : UU} (is : iscontr T) : isweq (λ (_ : T), tt).
proof: Proof. intros. unfold isweq. intro y. induction y. induction is as [c h]. set (hc := make_hfiber _ c (idpath tt)). split with hc. intros ha. induction ha as [x e]. unfold hc. unfold make_hfiber. unfold isProofIrrelevantUnit. simpl. apply (λ q, two_arg_paths_f (h x) q). apply ifcontrthenunitl0. Defined.
imports: UniMath.Foundations.Preamble