<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>You can locally declare two modules with the same name as the
record instances<br>
to accomplish what you want; e.g.:<br>
</p>
<p> record Functor (ℂ : Category) (𝔻 : Category) : Set where<br>
module ℂ = Category ℂ<br>
module 𝔻 = Category 𝔻<br>
field<br>
distrib : {A B C : ℂ.Object} {g : ℂ.Arrow B C} {f : ℂ.Arrow
A B} → func→ (g ℂ.⊕ f) ≡ (func→ g) 𝔻.⊕ (func→ f)<br>
<br>
<br>
Regards,<br>
<br>
Arjen<br>
</p>
<br>
<div class="moz-cite-prefix">On 01/22/2018 12:04 PM, Frederik
Hanghøj Iversen wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAD4k_qAp1uP8W_rxyDEowzi__Qy8mzu8-yDBm5=AxXw4f8h9jQ@mail.gmail.com">
<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>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>