Kleisli and Eilenberg-Moore decompositions and their corresponding monad transformers

EM.agda

open import Agda.Primitive

module _ {l : Level} where
  record Category : Set (lsuc l) where
    infixr 10 _~>_
    infixr 90 _o_
    field
      Obj : Set l
      _~>_ : Obj -> Obj -> Set
      id : forall {x} -> x ~> x
      _o_ : forall {x y z} -> y ~> z -> x ~> y -> x ~> z

  record Functor (c d : Category) : Set l where
    open Category c renaming (Obj to C)
    open Category d renaming (Obj to D ; _~>_ to _>~_)
    field
      F : C -> D
      map : forall {x y} -> x ~> y -> F x >~ F y

  record Monad (c : Category) : Set l where
    open Category c
    open Functor
    field
      endofunctor : Functor c c
      return : forall {x} -> x ~> F endofunctor x
      join : forall {x} -> F endofunctor (F endofunctor x) ~> F endofunctor x
    M = Functor.F endofunctor
    liftM = Functor.map endofunctor


  record Adjunction (c d : Category) : Set l where
    open Category c renaming (Obj to C)
    open Category d renaming (Obj to D ; _~>_ to _>~_ ; _o_ to _O_)
    open Functor

    field
      left : Functor c d
      right : Functor d c
      unit : forall {x} -> x ~> (F right (F left x))
      counit : forall {x} -> F left (F right x) >~ x

    open Functor left renaming (F to L ; map to lmap) public
    open Functor right renaming (F to R ; map to rmap) public

    monad : Monad c
    monad = record {
      endofunctor = record {
        F = \x -> R (L x);
        map = \f -> rmap (lmap f)
        };
      return = unit;
      join = rmap counit
      }

    trans : Monad d -> Monad c
    trans m = record {
      endofunctor = record {
        F = \x -> R (M (L x));
        map = \f -> rmap (liftM (lmap f))
        };
      return = rmap return o unit;
      join = rmap join o rmap (liftM counit)
      }
      where open Monad m


  module Decomp {c : Category} (m : Monad c) where
    open Category c
    open Monad m

    kleisli : Category
    kleisli = record {
      Obj = Obj;
      _~>_ = \x y -> x ~> M y;
      id = return;
      _o_ = \f g -> join o liftM f o g
      }
    kleisliAdj : Adjunction c kleisli
    kleisliAdj = record {
      left = record {
        F = \x -> x;
        map = \f -> return o f
        };
      right = record {
        F = M;
        map = \f -> join o liftM f
        };
      unit = return;
      counit = id
      }

    record Alg : Set l where
      field
        Carrier : Obj
        eval : M Carrier ~> Carrier
    open Alg

    em : Category
    em = record {
      Obj = Alg;
      _~>_ = \a1 a2 -> Carrier a1 ~> Carrier a2;
      id = id;
      _o_ = _o_
      }
    emAdj : Adjunction c em
    emAdj = record {
      left = record {
        F = \c -> record { Carrier = M c ; eval = join };
        map = liftM
        };
      right = record {
        F = \c -> Carrier c;
        map = \f -> f
        };
      unit = return;
      counit = \{x} → eval x
      }