<html>
<head>
<style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 12pt;
font-family:·s²Ó©úÅé
}
--></style></head>
<body class='hmmessage'><div dir='ltr'><font size="3" style="font-size:12pt;" color="#000000">Hi ,</font><div><br></div><div>i find many places define identity, symmetric and transitive, how to use monoid solve and which can it solve?</div><div><br></div><div>i would like to define a new set of equivalence relations, is there a light weight version of monoid?</div><div><br></div><div><span style="font-size: 12pt;">assume we do not know monoid, </span>how to build a concept such as monoid based on custom equivalence relations?</div><div><br></div><div>does new custom equivalence relations mainly use for a new kind of polynomials algebra and Natural number system?</div><div><br></div><div>if so, does it mean that i edit transitive in files which have transitive and then recompile std-library of agda, then it will work?</div><div><br></div><div><br></div><div><a href="https://github.com/agda/agda-stdlib/blob/08e95de542ce88d1b1e71ecdce2f57e37f916877/src/Algebra/Monoid-solver.agda" target="_blank">https://github.com/agda/agda-stdlib/blob/08e95de542ce88d1b1e71ecdce2f57e37f916877/src/Algebra/Monoid-solver.agda</a></div><div><br></div><div><a href="https://github.com/agda/agda-stdlib/blob/08e95de542ce88d1b1e71ecdce2f57e37f916877/src/Relation/Binary/PropositionalEquality/Core.agda" target="_blank">https://github.com/agda/agda-stdlib/blob/08e95de542ce88d1b1e71ecdce2f57e37f916877/src/Relation/Binary/PropositionalEquality/Core.agda</a></div><div><br></div><div><a href="https://github.com/agda/agda-stdlib/blob/08e95de542ce88d1b1e71ecdce2f57e37f916877/src/Relation/Binary/Indexed/Core.agda" target="_blank">https://github.com/agda/agda-stdlib/blob/08e95de542ce88d1b1e71ecdce2f57e37f916877/src/Relation/Binary/Indexed/Core.agda</a></div><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><br></div><div>i find this </div><div><a href="http://ocvs.cfv.jp/Agda/big-examples.alfa" target="_blank">http://ocvs.cfv.jp/Agda/big-examples.alfa</a><font size="3" style="font-size:12pt;" color="#000000"><br id="FontBreak"></font><br><br><div>Regards,</div><div><br></div><div>Martin </div></div> </div></body>
</html>