  We explore a data structure that generalises rectangular multi-dimensional
arrays. The shape of an n-dimensional array is typically given by a tuple of n
natural numbers. Each element in that tuple defines the length of the
corresponding axis. If we treat this tuple as an array, the shape of that array
is described by the single natural number n. A natural number itself can be
also treated as an array with the shape described by the natural number 1 (or
the element of any singleton set). This observation gives rise to the hierarchy
of array types where the shape of an array of level l+1 is a level-l array of
natural numbers. Such a hierarchy occurs naturally when treating arrays as
containers, which makes it possible to define both rank- and level-polymorphic
operations. The former can be found in most array languages, whereas the latter
gives rise to partial selections on a large set of hyperplanes, which is often
useful in practice. In this paper we present an Agda formalisation of arrays
with levels. We show that the proposed formalism supports standard
rank-polymorphic array operations, while type system gives static guarantees
that indexing is within bounds. We generalise the notion of ranked operator so
that it becomes applicable on arrays of arbitrary levels and we show why this
may be useful in practice.
