[Agda] Re: How to define subsemigroups

[N. Raghavendra]

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.

Best regards,
Raghu.

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