[Agda] Level symbols

[Wolfram Kahl]

On Sat, Aug 31, 2013 at 05:19:30PM +0400, Sergei Meshveliani wrote:
> This is about mnemonics for Level.
> 
> The standard library  lib-0.7  uses the symbols  a, b, c, p, ℓ  to
> denote  Level  values.
> 
> ℓ  is all right,  but  a, b, c, p  are likely to be used as variables of
> another type.
> Are there possible `italic' variants for  a, b, c ...  in Unicode ?
> 
> a -> \alpha, b -> \beta  also looks all right,   
> but what to choose for  `p'  as a level for a predicate P ?


I nowadays tend to have, for example:

  {ℓS ℓs : Level} {S : Setoid ℓS ℓs}

  {ℓP : Level} {P : Set ℓP}



Wolfram