This is a formalization of some of the displacement algebras found in mugen, as well as an exploration of some theoretical properties of Hierarchy Theories.

In particular, we present a collection of examples of displacement algebras (See Mugen.Algebra.Displacement), and prove some additional properties (right-invariance, existence of bottoms, and joins). We also show that displacement algebras induce monads on the category of strict orders (See Mugen.Cat.HierarchyTheory) Furthermore, we define the endomorphism displacement algebra (See Mugen.Algebra.Displacement.Endo), and have formalized the first step towards showing that this is generates the "universal hierarchy theory" (See Mugen.Cat.HierarchyTheory.Properties)

This formalization depends on the 1Lab, which can be installed by cloning the repo, and then adding a single line to the ~/.agda/libraries that points to the path where you cloned the repo. This formalization was checked against commit f5465e94.

Furthermore, this formalization requires Agda 2.6.3, which can be obtained by installing from source. Simply clone the Agda repository, and then run cabal install to install. If you do not have a working Haskell toolchain, the best route is to use ghcup. This formalization was checked against efa6fe4cc.

A Dockerfile is also provided that packages the required versions of agda and the 1lab. To run it, first build the image with docker build -t agda-mugen .. Once that completes, you can then run docker run agda-mugen, which will check the formalization.