<div dir="ltr"><div>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).</div><div><br></div><div>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:</div><div><br></div><div>     ℂ .Object</div><div><br></div><div>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:</div><div><br></div><div>    func→ (g (ℂ .⊕) f) ≡ func→ g (𝔻 .⊕) func→ f</div><div><br></div><div>Or perhaps even with backticks (as in Haskell) like so:</div><div><br></div><div>    func→ (g `ℂ .⊕` f) ≡ func→ g `𝔻 .⊕` func→ f</div><div><br></div><div>In stead I am left with writing it like so:</div><div><br></div><div>    func→ (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (func→ g) (func→ f)</div><div><br></div><div>Which is not so readable.</div><div><br></div><div>I've attached an MWE.<br clear="all"><div><br></div>-- <br><div class="gmail_signature"><div>Regards</div><div><i>Frederik Hanghøj Iversen</i></div></div>
</div></div>