<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"><<a href="mailto:gabrno@gmail.com" target="_blank">gabrno@gmail.com</a>></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't have to be reduced) and use what we call "definable quotient structure" 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's work on "pragmatic" 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>