Example of a setoid: N+
Setoid
The positive natural numbers N+ will be defined as a subsetoid of the natural numbers.Definition N+ := Build_SubCSetoid nat_as_CSetoid (fun n : N => n <> 0).
Definition NposP := (fun n : nat_as_CSetoid => n <> 0).
One and two are elements of it.
Definition ONEpos := Build_subcsetoid_crr _ NposP 1 (S_O 0).
Definition TWOpos := Build_subcsetoid_crr _ NposP 2 (S_O 1).
Addition and multiplication
Because addition and multiplication preserve positivity, we can define them on this subsetoid.Lemma plus_resp_Npos : bin_op_pres_pred _ NposP plus_is_bin_fun.
Definition Npos_plus := Build_SubCSetoid_bin_op _ _ plus_is_bin_fun plus_resp_Npos.
Lemma mult_resp_Npos : bin_op_pres_pred _ NposP mult_as_bin_fun.
Definition Npos_mult := Build_SubCSetoid_bin_op _ _ mult_as_bin_fun mult_resp_Npos.
The addition has no right unit on this set.
And the multiplication doesn't have an inverse, because there can't be an
inverse for 2.