proposition: Theorem iscontrfuntocontr (X : UU) {Y : UU} (is : iscontr Y) : iscontr (X -> Y).
proof: Proof. set (w := weqcontrtounit is). set (w' := weqffun X w). apply (iscontrweqb w' (iscontrfuntounit X)). Defined.
imports: UniMath.Foundations.PartC