Base.agda contains basic ordered category theory. All categories in the code are ordered and all functors preserve order. Therefore in the code, we just say categories and functors when talking about ordered categories and ordered functors (monotone on hom-posets). Also strict and lax functors, the terminal category, product of categories.
Monoidal.agda contains the specification of monoidal categories, op/lax-monoidal functors, monoidal-like categories.
Concurrent.agda contains specification of a concurrent monad, concurrent category, J as an oplax-monoidal functor, K as a lax-monoidal functor.
Kleisli.agda constructs the concurrent Kleisli category and the proof that it is in fact a concurrent category.
Adjoint.agda contains proofs that J and K as defined in Kleisli.agda form a monoidal adjunction and that their composite is a concurrent monad.
Posets.agda contains the proof that Poset is a category.
State.agda contains the proof that the State monad is a concurrent monad in Poset a la Rivas and Uustalu.
For an index of all the hyperlinked agda code, see here.