Theorem iscontrfunfromempty2 (X : UU) {Y : UU} (is : neg Y) : iscontr (Y -> X). Proof. intros. set (w := weqtoempty is). set (w' := weqbfun X (invweq w)). apply (iscontrweqb w' (iscontrfunfromempty X)). Defined.