Definition carrierofasubsetwithbinop {X : setwithbinop} (A : subsetswithbinop X) : setwithbinop. Proof. set (aset := (make_hSet (carrier A) (isasetsubset (pr1carrier A) (setproperty X) (isinclpr1carrier A))) : hSet). exists aset. set (subopp := (λ a a' : A, make_carrier A (op (pr1carrier _ a) (pr1carrier _ a')) (pr2 A a a')) : (A → A → A)). simpl. unfold binop. apply subopp. Defined.