I am a master's student at the university of Iceland. Interested in category theory, type theory and algebraic topology.
Base.agda contains basic ordered category theory. All categories in the code are ordered and all functors preserve order, so we just call them categories and functors. Also contains 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 Kleisli category of a given monad and the proof that this category is a concurrent category.
Adjoint.agda contains (the incomplete) proofs that J and K as defined in Kleisli.agda form a monoidal adjunction and that their composite is a concurrent monad. In the thesis, there is an explanation why the proofs are incomplete and how we resolve that by introducing a type of category and a type of functors.
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.