[Agda] How to define subsemigroups

[N. Raghavendra]

Hi,

How does one define subobjects of algebraic objects in Agda?  E.g., a
subsemigroup of a semigroup, taking semigroup as defined in the Algebra
module of stdlib?

According to that definition, a semigroup has an underlying setoid
(S,~), i.e., a set S with equivalence relation ~, and an associative
binary operation * on S which preserves the relation ~.  So a
subsemigroup should be given by a subsetoid of (S,~) stable under the
operation *.  So another question: how does one define a subsetoid of a
setoid?

Thanks,
Raghavendra.

-- 
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/