    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- An effectful view of the Sum type (Left-biased)
    ------------------------------------------------------------------------

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

    open import Level

    module Data.Sum.Effectful.Left.Transformer {a} (A : Set a) (b : Level) where

    open import Data.Sum.Base using (map₂ ; inj₁ ; inj₂; _⊎_; [_,_]′)
    open import Effect.Choice using (RawChoice)
    open import Effect.Empty using (RawEmpty)
    open import Effect.Functor using (RawFunctor)
    open import Effect.Applicative
      using (RawApplicative; RawApplicativeZero; RawAlternative)
    open import Effect.Monad using (RawMonad; RawMonadT)
    open import Function.Base using (const; flip; _∘_; _∘′_; _$_)

    private
      variable
        M : Set (a ⊔ b) → Set (a ⊔ b)

    -- To minimize the universe level of the RawFunctor, we require that
    -- elements of B are "lifted" to a copy of B at a higher universe level
    -- (a ⊔ b). See the examples for how this is done.

    open import Data.Sum.Effectful.Left A b using (Sumₗ)

    ------------------------------------------------------------------------
    -- Left-biased monad transformer instance for _⊎_

    record SumₗT
             (M : Set (a ⊔ b) → Set (a ⊔ b))
             (B : Set (a ⊔ b)) : Set (a ⊔ b) where
      constructor mkSumₗT
      field runSumₗT : M (Sumₗ B)
    open SumₗT public

    ------------------------------------------------------------------------
    -- Structure

    functor : RawFunctor M → RawFunctor (SumₗT M)
    functor M = record
      { _<$>_ = λ f → mkSumₗT ∘′ (map₂ f <$>_) ∘′ runSumₗT
      } where open RawFunctor M

    applicative : RawApplicative M → RawApplicative (SumₗT M)
    applicative M = record
      { rawFunctor = functor rawFunctor
      ; pure = mkSumₗT ∘′ pure ∘′ inj₂
      ; _<*>_ = λ mf mx → mkSumₗT ([ const ∘′ inj₁ , map₂ ]′ <$> runSumₗT mf <*> runSumₗT mx)
      } where open RawApplicative M

    empty : RawApplicative M → A → RawEmpty (SumₗT M)
    empty M a = record
      { empty = mkSumₗT (pure (inj₁ a))
      } where open RawApplicative M

    choice : RawApplicative M → RawChoice (SumₗT M)
    choice M = record
      { _<|>_ = λ ma₁ ma₂ → mkSumₗT ([ flip const , const ∘ inj₂ ]′ <$> runSumₗT ma₁ <*> runSumₗT ma₂)
      } where open RawApplicative M

    applicativeZero : RawApplicative M → A → RawApplicativeZero (SumₗT M)
    applicativeZero M a = record
      { rawApplicative = applicative M
      ; rawEmpty = empty M a
      }

    alternative : RawApplicative M → A → RawAlternative (SumₗT M)
    alternative M a = record
      { rawApplicativeZero = applicativeZero M a
      ; rawChoice = choice M
      }

    monad : RawMonad M → RawMonad (SumₗT M)
    monad M = record
      { rawApplicative = applicative rawApplicative
      ; _>>=_ = λ ma f → mkSumₗT $ do
                           a ← runSumₗT ma
                           [ pure ∘′ inj₁ , runSumₗT ∘′ f ]′ a
      } where open RawMonad M

    monadT : RawMonadT SumₗT
    monadT M = record
      { lift = mkSumₗT ∘′ (inj₂ <$>_)
      ; rawMonad = monad M
      } where open RawMonad M