<div dir="ltr">When I was programming with rationals in Agda, I also found the approach of maintaining coprime proofs intractable, especially since I wanted the typechecker to perform actual arithmetic and it was expensive to compute these proofs.  I ended up settling on a purely axiomatic approach, including a patch to Agda to support BUILTIN RATIONAL.<br>

<div class="gmail_extra"><br><div class="gmail_quote">On Tue, Mar 11, 2014 at 11:43 AM, Li Nuo <span dir="ltr">&lt;<a href="mailto:gabrno@gmail.com" target="_blank">gabrno@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">

<div dir="ltr">Hi,<div><br></div><div>I think you can use an alternative approach to make the definition simpler. You could define the setoid version (namely fractions which doesn&#39;t have to be reduced) and use what we call &quot;definable quotient structure&quot; to relate the setoid definition with the normal form definition (which you can find here <a href="http://www.cs.nott.ac.uk/~txa/publ/defquotients.pdf" target="_blank">http://www.cs.nott.ac.uk/~txa/publ/defquotients.pdf</a>).</div>

</div></blockquote><div><br></div><div>Incidentally, have you tried to relate this notion to Cyril Cohen&#39;s work on &quot;pragmatic&quot; quotient types in Coq (see <a href="http://perso.crans.org/cohen/work/quotients/">http://perso.crans.org/cohen/work/quotients/</a>)?  </div>

<div><br></div><div>Noam</div><div><br></div></div></div></div>