<div dir="ltr">Ok, let me try to be more precise. In your example you are defining a single thing (id)<div>with multiple properties. You can read it as something like this:</div><div><br></div><div>```</div><div>id.TYPE = <span style="color:rgb(80,0,80);font-size:12.8px">{A : Type} → A → A</span></div><div><span style="color:rgb(80,0,80);font-size:12.8px">id.VALUE = </span><span style="color:rgb(80,0,80);font-size:12.8px">{A} x </span><font color="#500050"><span style="font-size:12.8px">↦</span></font><span style="color:rgb(80,0,80);font-size:12.8px"> x</span></div><div><span style="color:rgb(80,0,80);font-size:12.8px">id.SYNTAX = {A} x </span><font color="#500050"><span style="font-size:12.8px">↦ x "</span></font><span style="color:rgb(80,0,80);font-size:12.8px">∶" A</span></div><div><span style="color:rgb(80,0,80);font-size:12.8px">id.FIXITY = infixl 0</span></div><div><span style="color:rgb(80,0,80);font-size:12.8px">```</span></div><div><span style="color:rgb(80,0,80);font-size:12.8px"><br></span></div><div><font color="#500050"><span style="font-size:12.8px">Contrary to your intuition </span></font><font color="#500050"><span style="font-size:12.8px">"</span></font><span style="color:rgb(80,0,80);font-size:12.8px">∶" is not a thing in its own right, but simply a terminal symbol in</span></div><div><span style="color:rgb(80,0,80);font-size:12.8px">the parsing rule for id.</span></div><div><span style="color:rgb(80,0,80);font-size:12.8px"><br></span></div><div><font color="#500050"><span style="font-size:12.8px">/ Ulf</span></font></div><div><span style="color:rgb(80,0,80);font-size:12.8px"><br></span></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Nov 4, 2017 at 8:44 AM, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Thanks for you answer, Ulf.<br>
<br>
On 04/11/17 06:33, <a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a> wrote:<span class=""><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
On Fri, Nov 3, 2017 at 11:37 PM, Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a> <mailto:<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.u<wbr>k</a>>> wrote:<br>
<br>
    Can I say some things about Agda's syntax declaration?<br>
<br>
    * Why are the definitions backwards (what you define is in the<br>
    right-hand side)?<br>
<br>
<br>
They're not. You are defining the syntax for a particular name in the same way that<br>
you define the value of a particular name (`syntax f x = bla` vs `f x = bla`). If syntax<br>
declarations were the other way around you would be very surprised to find that you<br>
can't have multiple syntax declarations for the same name (which you can't).<br>
</blockquote>
<br></span>
I don't understand this remark. Consider again<span class=""><br>
<br>
```<br>
id : {A : Type} → A → A<br>
id {A} x = x<br>
<br>
syntax id {A} x = x ∶ A<br>
<br>
infixl 0 id<br>
```<br>
<br></span>
In the syntax definition, I have *already* define id (occurring in the left-hand side), and the new thing I am *defining* in the syntax declaration is ":", which occurs in the *right*-hand side.<br>
<br>
At first I tried to define ":" to be left-associative, but this didn't work. Then cheating from other people's examples I realized that one is expected to define `id` to be left-associative. I didn't answer the question myself as you suggest: I still don't know what it means for id to be left-associative. :-) The above works and is useful, but I don't understand it.<br>
<br>
Best,<br>
Martin<br>
</blockquote></div><br></div>