Corollary isweqcontrcontr {X Y : UU} (f : X -> Y) (isx : iscontr X) (isy: iscontr Y): isweq f. Proof. intros. set (py := λ (y : Y), tt). apply (twooutof3a f py (isweqcontrtounit isx) (isweqcontrtounit isy)). Defined.