Definition carrierofsubsetwith2binop {X : setwith2binop} (A : subsetswith2binop X) : setwith2binop. Proof. set (aset := (make_hSet (carrier A) (isasetsubset (pr1carrier A) (setproperty X) (isinclpr1carrier A))) : hSet). exists aset. set (subopp1 := (λ a a' : A, make_carrier A (op1 (pr1carrier _ a) (pr1carrier _ a')) (pr1 (pr2 A) a a')) : (A → A → A)). set (subopp2 := (λ a a' : A, make_carrier A (op2 (pr1carrier _ a) (pr1carrier _ a')) (pr2 (pr2 A) a a')) : (A → A → A)). simpl. exact (subopp1 ,, subopp2). Defined.