[Agda] Re: How to define subsemigroups

[N. Raghavendra]

At 2015-02-14T07:39:09-05:00, Harley Eades III wrote:

> The definition of a subsetoid can be found here:
>
> https://github.com/heades/law/blob/master/Setoid/Total.agda#L83
>
> That file is based on a few papers:
>
> http://www.cs.ru.nl/~venanzio/publications/Setoids_JFP_2003.pdf and 
> http://www.cs.ru.nl/~venanzio/publications/Universal_Algebra_TPHOLs_1999.pdf
>
> I hope it helps.

Hi Harley,

Thanks for the pointers.  Yes, I saw that section 5.1 in the paper of
Barthe and Capretta defines subsetoids.  Your code looks clear and
self-explanatory.  I'll ask if I have any questions about it.

Best regards,
Raghu.

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