<div dir="auto"><div>The feature is called "postfix projections", BTW.<div dir="auto"><br></div><div dir="auto"><a href="https://github.com/agda/agda/issues/1963">https://github.com/agda/agda/issues/1963</a><br></div><div dir="auto"><br></div><div dir="auto">Cheers</div><div dir="auto">/Sandro</div><br><div class="gmail_extra"><br><div class="gmail_quote">On Jan 22, 2018 1:07 PM, "a.j.rouvoet" <<a href="mailto:a.j.rouvoet@gmail.com">a.j.rouvoet@gmail.com</a>> wrote:<br type="attribution"><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
  
    
  
  <div 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><div class="elided-text">
    <br>
    <div class="m_-5839020581329741774moz-cite-prefix">On 01/22/2018 12:04 PM, Frederik
      Hanghøj Iversen wrote:<br>
    </div>
    </div><blockquote type="cite"><div class="elided-text">
      <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="m_-5839020581329741774gmail_signature">
            <div>Regards</div>
            <div><i>Frederik Hanghøj Iversen</i></div>
          </div>
        </div>
      </div>
      <br>
      <fieldset class="m_-5839020581329741774mimeAttachmentHeader"></fieldset>
      <br>
      </div><pre>______________________________<wbr>_________________
Agda mailing list
<a class="m_-5839020581329741774moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a class="m_-5839020581329741774moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a>
</pre>
    </blockquote>
    <br>
  </div>

<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div></div></div>