# [Agda] Level symbols

Wolfram Kahl kahl at cas.mcmaster.ca
Sat Aug 31 21:24:29 CEST 2013

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