<div dir="auto"><div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br></blockquote><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
> The workaround is to wrap the direct definition in a data-type or<br>
> record. That requires some extra constructors/projections to convert<br>
> between direct proofs of equality and the wrapped ones, but the<br>
> problem with implicit arguments seems to disappear.<br>
> <br>
<br>
In my example with Fraction and Prefraction (in my last letter)<br>
everything looks wrapped enough, I do not know what kind of wrapping<br>
do you mean.<br></blockquote></div></div><div dir="auto"><br></div><div dir="auto"><span style="font-family:sans-serif">Your definition of _=fr_ is not a data type or record. It's exactly the sort of definition I was referring to, where one relation is defined in terms of another, via computation.</span></div><div dir="auto"><span style="font-family:sans-serif"><br></span></div><div dir="auto"><div dir="auto">   _=fr_ :  Rel Fraction α=</div><div dir="auto">   f =fr g =  (num f * denom g) ≈ (num g * denom f)</div><div dir="auto"><br></div><div dir="auto">Have a look at the example I linked to to see what I mean by wrapping:</div><div dir="auto"><br></div><div dir="auto">record _≃_ (i j : A ≅ B) : Set e where</div><div dir="auto">  constructor ⌞_⌟</div><div dir="auto">  open _≅_ using (from)</div><div dir="auto">  field from-≈ : from i ≈ from j</div><div dir="auto"><br></div><div dir="auto">The record has a single field from-≈ with the type that corresponds exactly to to the derived notion of equation we want. In your case that field would have type</div><div dir="auto"><br></div><div dir="auto">  (num f * denom g) ≈ (num g * denom f)</div><div dir="auto"><br></div><div dir="auto">You can then provide a proof of the equality using <span style="font-family:sans-serif">⌞ p ⌟ instead of p</span><span style="font-family:sans-serif">.</span> The<span style="font-family:sans-serif"> point of the record is for Agda to remember the two parameters f and g, which it 'forgets' when you provide a value of the defined equality type directly.</span></div><div dir="auto"><br></div><div dir="auto">(More details at <a href="https://github.com/agda/agda-categories/blob/9e603a3dd00be0b6040f13db38967ecff085e05b/src/Categories/Morphism/IsoEquiv.agda#L55">https://github.com/agda/agda-categories/blob/9e603a3dd00be0b6040f13db38967ecff085e05b/src/Categories/Morphism/IsoEquiv.agda#L55</a> )</div><div dir="auto"><br></div><div dir="auto">Cheers</div><div dir="auto">/Sandro</div></div></div>