```------------------------------------------------------------------------
-- The Agda standard library
--
------------------------------------------------------------------------

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

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

open import Algebra using (RawMonoid)
open import Data.Product using (_×_; _,_; map₂; proj₁; proj₂)
open import Data.Unit.Polymorphic.Base
open import Effect.Choice
open import Effect.Empty
open import Effect.Functor
open import Effect.Applicative
open import Function.Base

private
variable
f s : Level
A B : Set s
S S₁ S₂ : Set s
M : Set s → Set f

------------------------------------------------------------------------
-- Re-export the basic type and definitions

; StateT
; mkStateT
; runStateT
; evalStateT
; execStateT
)

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

functor : RawFunctor M → RawFunctor (StateT S M)
functor M = record
{ _<\$>_ = λ f ma → mkStateT (λ s → map₂ f <\$> StateT.runStateT ma s)
} where open RawFunctor M

applicative : RawMonad M → RawApplicative (StateT S M)
applicative M = record
{ rawFunctor = functor rawFunctor
; pure = λ a → mkStateT (pure ∘′ (_, a))
; _<*>_ = λ mf mx → mkStateT \$ λ s →
do (s , f) ← StateT.runStateT mf s
(s , x) ← StateT.runStateT mx s
pure (s , f x)

empty : RawEmpty M → RawEmpty (StateT S M)
empty M = record
{ empty = mkStateT (const (RawEmpty.empty M))
}

choice : RawChoice M → RawChoice (StateT S M)
choice M = record
{ _<|>_ = λ ma₁ ma₂ → mkStateT \$ λ s →
StateT.runStateT ma₁ s
<|> StateT.runStateT ma₂ s
} where open RawChoice M

applicativeZero : RawMonadZero M → RawApplicativeZero (StateT S M)
applicativeZero M = record
; rawEmpty = empty (RawMonadZero.rawEmpty M)
}

alternative : RawMonadPlus M → RawAlternative (StateT S M)
alternative M = record
; rawChoice = choice rawChoice

{ rawApplicative = applicative M
; _>>=_ = λ ma f → mkStateT \$ λ s →
do (s , a) ← StateT.runStateT ma s
StateT.runStateT (f a) s

; rawEmpty = empty (RawMonadZero.rawEmpty M)
}

; rawChoice = choice rawChoice

------------------------------------------------------------------------

monadT : RawMonadT {f = s} {g₁ = f} {g₂ = s ⊔ f} (StateT S)
{ lift = λ ma → mkStateT (λ s → (s ,_) <\$> ma)

{ gets   = λ f → mkStateT (λ s → pure (s , f s))
; modify = λ f → mkStateT (λ s → pure (f s , _))

------------------------------------------------------------------------

liftStateT M Mon = record
{ gets   = λ f₁ → lift (gets f₁)
; modify = λ f₁ → lift (modify f₁)

{ gets   = λ f → mkReaderT (const (gets f))
; modify = λ f → mkReaderT (const (modify f))