This is an experimental library for multidimensionial data types (Morton numbers, n-dimensional trees, etc.) in Cubical Agda. See Morton and RegionTrees for comparable libraries in Julia.
The goal is to explore potential uses of transport in obtaining efficiencies in computations on multidimensonal spatial data; see the BinNat module of the Cubical Agda library for an example of this approach.
DISCLAIMER: The library is intended by the author to be a project for learning Agda and cubical type theory, so expect the code to be naive, inefficient, and possibly incorrect, in an unconventional style. Suggestions for improvement would be warmly welcomed.