[Agda] forced arguments in EqReasoning

[James Wood]

In particular, the definition of _=fr_ forgets about the denom≠0 field 
from each side, so they cannot be reconstructed by unification.

James

On 28/11/2020 13:12, Sandro Stucki wrote:
> 
>      > 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 
> <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fagda%2Fagda-categories%2Fblob%2F9e603a3dd00be0b6040f13db38967ecff085e05b%2Fsrc%2FCategories%2FMorphism%2FIsoEquiv.agda%23L55&data=04%7C01%7Cjames.wood.100%40strath.ac.uk%7C17a6b02f5b6a4c96a52c08d8939f46df%7C631e0763153347eba5cd0457bee5944e%7C0%7C1%7C637421660175400421%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=TwCCAIwKEFy8y23huMuTzJ41gqQiYhEokaJWoPMzHQg%3D&reserved=0> 
> )
> 
> Cheers
> /Sandro
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=04%7C01%7Cjames.wood.100%40strath.ac.uk%7C17a6b02f5b6a4c96a52c08d8939f46df%7C631e0763153347eba5cd0457bee5944e%7C0%7C1%7C637421660175430405%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=AS6G7ZZiPz8jb4wUO20GvIp6JrCmKxeqOxUZamrsa9w%3D&reserved=0
>