[Agda] Infix-notation and TDNR

[Frederik Hanghøj Iversen]

I just discovered a new feature in Agda. I don't know what's it's called
(haven't been able to find any documentation on it) so let me just name it
Type-Directed Name-space Resolution (TDNR).

The feature I'm talking about it the one that e.g lets you project a field
`Object` of a term `ℂ` of type `Category` that has this field like so:

     ℂ .Object

What I would like to do is use the infix version of this. So for instance
for a field `_⊕_` I would like to express the distributive properties of
functors like so:

    func→ (g (ℂ .⊕) f) ≡ func→ g (𝔻 .⊕) func→ f

Or perhaps even with backticks (as in Haskell) like so:

    func→ (g `ℂ .⊕` f) ≡ func→ g `𝔻 .⊕` func→ f

In stead I am left with writing it like so:

    func→ (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (func→ g) (func→ f)

Which is not so readable.

I've attached an MWE.

-- 
Regards
*Frederik Hanghøj Iversen*
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180122/a513e9cc/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: T.agda
Type: application/octet-stream
Size: 689 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180122/a513e9cc/attachment.obj>