<p dir="ltr">I'm not sure what you mean. When using (X : Type) in my proposed syntax, you don'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) -> 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, "Matthieu Sozeau" <<a href="mailto:matthieu.sozeau@gmail.com">matthieu.sozeau@gmail.com</a>> a écrit :<br>
><br>
> Hi,<br>
><br>
> It seems you’re gonna have to invent names for the i’s…<br>
> Coq has a similar feature using a generalizable variables syntax<br>
> whereby you can declare some names to be generalized (e.g. A B i j k)<br>
> and then writing `(X : Type i) will add an implicit {i} binder just before<br>
> (x : Type i). The backquote can actually be put anywhere and will introduce<br>
> pi’s or lambdas according to whether we’re in type or (term or unknown)<br>
> position for the generalizable variable occurrences appearing in it’s scope.<br>
> It was introduced for type class instance arguments mainly, allowing<br>
> compact `{Eq A} binders for example. It can also introduce automagically named<br>
> binders for superclasses but it’s seldom used. I just want to point out that<br>
> if you allow this then further references to constants using telsyntax<br>
> should probably not be allowed to refer to the generated names :)<br>
><br>
> Best,<br>
> — Matthieu<br>
><br>
> On 26 nov. 2014, at 22:11, Andy Morris <<a href="mailto:andy@adradh.org.uk">andy@adradh.org.uk</a>> wrote:<br>
><br>
> > It's backwards the same way the current syntax declarations are, and presumably for the same reason.<br>
> ><br>
> >> On 26 Nov 2014, at 22:08, Felipe Lessa <<a href="mailto:felipe.lessa@gmail.com">felipe.lessa@gmail.com</a>> wrote:<br>
> >><br>
> >> On 26-11-2014 11:33, Guillaume Brunerie wrote:<br>
> >>> telsyntax {i : Level} (X : Set i) = (X : Type)<br>
> >><br>
> >> I hope this isn't an obvious question, but isn't this syntax backwards?<br>
> >> Shouldn't it be like below?<br>
> >><br>
> >> telsyntax (X : Type) = {i : Level} (X : Set i)<br>
> >><br>
> >> Cheers, :)<br>
> >><br>
> >> --<br>
> >> Felipe.<br>
> >><br>
> >> _______________________________________________<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">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> ><br>
> > _______________________________________________<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">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
> _______________________________________________<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">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</p>