[Agda] How to define subsemigroups

[Harley Eades III]

Hi, Raghavendra.

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.

Very best,
Harley

On Feb 14, 2015, at 5:06 AM, N. Raghavendra <raghu at hri.res.in> 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.
> 
> -- 
> N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
> Harish-Chandra Research Institute, http://www.hri.res.in/
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda