Nibbles
Nibbles.
[YP:C] describes \mathbb{Y} as the set of sequences of nibbles,
i.e. half bytes.
[YP] does not use any specific symbol for the set of nibbles
(unlike \mathbb{O} for the set of bytes [YP:B]).
We use the library type nibble to model the set of nibbles.
