Definition squash_to_hSet_2 {X Y : UU} {Z : hSet} (f : X -> Y -> Z) : isconst_2 f -> ∥ X ∥ -> ∥ Y ∥ -> Z. Proof. intros c. use squash_to_set. { apply isaset_forall_hSet. } { intros x. use squash_to_hSet. exact (f x). intros y y'. exact (c x x y y'). } { intros x x'. apply funextfun; intros yn. apply (squash_to_prop yn). { apply setproperty. } intros y. assert (e : hinhpr y = yn). { apply propproperty. } induction e. change ( f x y = f x' y ). exact (c x x' y y). } Defined.