    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- The error monad transformer
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    open import Level using (Level; _⊔_; suc)

    module Effect.Monad.Error.Transformer {e} (E : Set e) (a : Level) where

    open import Effect.Monad using (RawMonad)
    open import Function.Base using (_∘′_; _$_)

    private
      variable
        f ℓ : Level
        A B : Set ℓ
        M : Set f → Set ℓ

    ------------------------------------------------------------------------
    -- Error monad operations

    record RawMonadError
           (M : Set (e ⊔ a) → Set ℓ)
           : Set (suc (e ⊔ a) ⊔ ℓ) where
      field
        throw : E → M A
        catch : M A → (E → M A) → M A

      during : (E → E) → M A → M A
      during f ma = catch ma (throw ∘′ f)

    ------------------------------------------------------------------------
    -- Monad error transformer specifics

    module Sumₗ where

      open import Data.Sum.Base using (inj₁; inj₂; [_,_]′)
      open import Data.Sum.Effectful.Left.Transformer E a

      monadError : RawMonad M → RawMonadError (SumₗT M)
      monadError M = record
        { throw = mkSumₗT ∘′ pure ∘′ inj₁
        ; catch = λ ma k → mkSumₗT $ do
                             a ← runSumₗT ma
                             [ runSumₗT ∘′ k , pure ∘′ inj₂ ]′ a
        } where open RawMonad M

    module Sumᵣ where

      open import Data.Sum.Base using (inj₁; inj₂; [_,_]′)
      open import Data.Sum.Effectful.Right.Transformer a E

      monadError : RawMonad M → RawMonadError (SumᵣT M)
      monadError M = record
        { throw = mkSumᵣT ∘′ pure ∘′ inj₂
        ; catch = λ ma k → mkSumᵣT $ do
                             a ← runSumᵣT ma
                             [ pure ∘′ inj₁ , runSumᵣT ∘′ k ]′ a
        } where open RawMonad M