[Agda] is there an example to create algebra from congruence distributive variety

[Mandy Martino]

Hi  
i use book  polynomial completeness in algebraic system,
it mentions to  create variety  first  then  it  can  create algebra

f(x,y,x) =  f(x,y,y) = xf(z,y,z) =  f(y,y,z) =  z
variety  with  pixley  term  t  and  t(x,t(x,y,z),y) =  y
pair of equivalence relations must  satisfy  x*y  =  y*x  this  permute
i search code  in  agda  standard library, there is no variety this name,  is  it  using another  method to create algebra?
Regards,
Martin Lee 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151217/c4a8e874/attachment.html