[Agda] algebra libraries

[Serge D. Mechveliani]

People,
As I see, Standard library lib-0.6  has the classical algebraic categories
from  Setoid  up to  CommutativeRing. 
I am investigating the possibility to continue this hierarchy
(trying the proof support from tiny to full one):  EntireRing, 
EuclideanRing, Module, Field, FiniteField,  and so on, with defining their 
instances for various domain constructors (like in the DoCon library).
This aims at trying the principle possibility of an advanced application 
(not for standard), with estimating the overhead.

Does there exist this kind of algebra library in Agda ?  

in Coq ? 

Regards,

------
Sergei