<p dir="ltr">I&#39;m not sure what you mean. When using (X : Type) in my proposed syntax, you don&#39;t give a name to the i, hence it will be autogenerated by Agda so there will be no way to refer back to it by name.<br>
What you can do instead if you need the level somewhere, is to define the following function:</p>
<p dir="ltr">get-level : (X : Type) -&gt; Level<br>
get-level {i} _ = i</p>
<p dir="ltr">And then [get-level X] returns the universe level of X.</p>
<p dir="ltr">Also, in Coq why do you have to give specific names to be generalized? Why not generalize every variable which is not in scope?<br></p>
<p dir="ltr">Le 27 nov. 2014 00:07, &quot;Matthieu Sozeau&quot; &lt;<a href="mailto:matthieu.sozeau@gmail.com">matthieu.sozeau@gmail.com</a>&gt; a écrit :<br>
&gt;<br>
&gt; Hi,<br>
&gt;<br>
&gt;   It seems you’re gonna have to invent names for the i’s…<br>
&gt; Coq has a similar feature using a generalizable variables syntax<br>
&gt; whereby you can declare some names to be generalized (e.g. A B i j k)<br>
&gt; and then writing `(X : Type i) will add an implicit {i} binder just before<br>
&gt; (x : Type i). The backquote can actually be put anywhere and will introduce<br>
&gt; pi’s or lambdas according to whether we’re in type or (term or unknown)<br>
&gt; position for the generalizable variable occurrences appearing in it’s scope.<br>
&gt; It was introduced for type class instance arguments mainly, allowing<br>
&gt; compact `{Eq A} binders for example. It can also introduce automagically named<br>
&gt; binders for superclasses but it’s seldom used. I just want to point out that<br>
&gt; if you allow this then further references to constants using telsyntax<br>
&gt; should probably not be allowed to refer to the generated names :)<br>
&gt;<br>
&gt; Best,<br>
&gt; — Matthieu<br>
&gt;<br>
&gt; On 26 nov. 2014, at 22:11, Andy Morris &lt;<a href="mailto:andy@adradh.org.uk">andy@adradh.org.uk</a>&gt; wrote:<br>
&gt;<br>
&gt; &gt; It&#39;s backwards the same way the current syntax declarations are, and presumably for the same reason.<br>
&gt; &gt;<br>
&gt; &gt;&gt; On 26 Nov 2014, at 22:08, Felipe Lessa &lt;<a href="mailto:felipe.lessa@gmail.com">felipe.lessa@gmail.com</a>&gt; wrote:<br>
&gt; &gt;&gt;<br>
&gt; &gt;&gt; On 26-11-2014 11:33, Guillaume Brunerie wrote:<br>
&gt; &gt;&gt;&gt; telsyntax {i : Level} (X : Set i) = (X : Type)<br>
&gt; &gt;&gt;<br>
&gt; &gt;&gt; I hope this isn&#39;t an obvious question, but isn&#39;t this syntax backwards?<br>
&gt; &gt;&gt; Shouldn&#39;t it be like below?<br>
&gt; &gt;&gt;<br>
&gt; &gt;&gt; telsyntax (X : Type) = {i : Level} (X : Set i)<br>
&gt; &gt;&gt;<br>
&gt; &gt;&gt; Cheers, :)<br>
&gt; &gt;&gt;<br>
&gt; &gt;&gt; --<br>
&gt; &gt;&gt; Felipe.<br>
&gt; &gt;&gt;<br>
&gt; &gt;&gt; _______________________________________________<br>
&gt; &gt;&gt; Agda mailing list<br>
&gt; &gt;&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; &gt;&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt; &gt;<br>
&gt; &gt; _______________________________________________<br>
&gt; &gt; Agda mailing list<br>
&gt; &gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; &gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;<br>
&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</p>