[Agda] Subsetoid, Subgroup ...

Serge D. Mechveliani mechvel at botik.ru
Wed Jan 30 13:17:52 CET 2013


People,
I think of implementing  Subsetoid, Subsemigroup, Subgroup ...,
by using an injective \~~-conrguent map, using 
Function.Injection.Injection  and a membership predicate. 
At least, SubDecSetoid is compiled.

But for any occasion, may be, these Sub- guys are in Standard library?

Thanks, 

------
Sergei


More information about the Agda mailing list