[Agda] How to define subsemigroups

[Sergei Meshveliani]

On Sat, 2015-02-14 at 15:36 +0530, N. Raghavendra wrote:
> 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.
> 


I did this this way:


-------------------------------------------------------------------------
record CongMember {a ℓ p : Level} (A : Setoid a ℓ) :  Set _ 
  where
  constructor congMember    -- Congruent Membership (to a Subset)
  Carrier = Setoid.Carrier A
  _≈_     = Setoid._≈_ A

  field  member : Carrier → Set p
         congM  : member Respects _≈_
--                                                                              
-- `member'  is a membership for a subset B in A.
--           member x  is non-empty  iff  x ∈ B.                

record DecCongMember {a ℓ p : Level} (A : Setoid a ℓ) : Set _
  where
  constructor decCongMem                         -- Decidable membership

  Carrier = Setoid.Carrier A
  _≈_     = Setoid._≈_ A

  field  cMember : CongMember {a} {ℓ} {p} A
         member? : Decidable (CongMember.member cMember)

------------------------------------------------------------------------------  
record Subset {a ℓ p : Level} (A : Setoid a ℓ)
                              (cMem : CongMember {a} {ℓ} {p} A) :  Set _
  where
  constructor subEl      -- making a subset element      
  open CongMember cMem

  field  elem  : Carrier
         .proof : member elem
---------------------------------------------------------------------------

For example,  (subEl 4 even-4) :  
                       Subset Nat.setoid (congMember even cong-even)

represents 4 as an element of the subset of even numbers in  Nat.
Here  even-4  is a witness for  Even 4,
cong-even  is a witness for that the predicate  even  agrees with  _≈_
on Nat (that is with _≡_).

In my approach of
http://www.botik.ru/pub/local/Mechveliani/agdaNotes/EuclideanResidue-dec13-2014.zip

I use this construct for a  decidable subsetoid, decidable Subsemigroup,
and so on.
I restrict to a decidable equality and decidable membership because
without such a decidability there will remain too poor library of
algorithmic methods.

Also my structures, as  Semigroup, Group etc,  are not of Standard
library, they have certain additional operations. 

But: 
you can use the above approach to Subset without requiring decidability,
and with using Standard library structures for algebra.

Regards,

------
Sergei