[Agda] Re: How to define subsemigroups

[Sergei Meshveliani]

On Sat, 2015-02-14 at 21:16 +0530, N. Raghavendra wrote:
> At 2015-02-14T15:40:35+04:00, Sergei Meshveliani wrote:
> 
> > 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 _≈_
> > --------------------------------------------------------------------
> > 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
> > --------------------------------------------------------------------
> 
> Hi Sergei,
> 
> Thanks!
> 
> Your definition seems similar to the one pointed out by Harley in his
> reply.  If I understand correctly, CongMember is the set of
> setoid-predicates, and Subset A cMem is the carrier of the subsetoid of
> A separated out by the predicate cMem.


Yes -- with the addition that  cMem  also contains a witness (proof) for
that the membership predicate is agreed with the relation _≈_.
That is:  for x ≈ y,  it holds  (member x) iff (member y).

Regards,

------
Sergei