[Agda] Level symbols

Sergei Meshveliani mechvel at botik.ru
Sat Aug 31 15:19:30 CEST 2013


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 ?



More information about the Agda mailing list