[Agda] forced arguments in EqReasoning

[Sandro Stucki]

>
>
> > The workaround is to wrap the direct definition in a data-type or
> > record. That requires some extra constructors/projections to convert
> > between direct proofs of equality and the wrapped ones, but the
> > problem with implicit arguments seems to disappear.
> >
>
> In my example with Fraction and Prefraction (in my last letter)
> everything looks wrapped enough, I do not know what kind of wrapping
> do you mean.
>

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.

   _=fr_ :  Rel Fraction α=
   f =fr g =  (num f * denom g) ≈ (num g * denom f)

Have a look at the example I linked to to see what I mean by wrapping:

record _≃_ (i j : A ≅ B) : Set e where
  constructor ⌞_⌟
  open _≅_ using (from)
  field from-≈ : from i ≈ from j

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

  (num f * denom g) ≈ (num g * denom f)

You can then provide a proof of the equality using ⌞ p ⌟ instead of p.
The 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.

(More details at
https://github.com/agda/agda-categories/blob/9e603a3dd00be0b6040f13db38967ecff085e05b/src/Categories/Morphism/IsoEquiv.agda#L55
)

Cheers
/Sandro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201128/51cd4705/attachment.html>