-- The Agda standard library
-- Instances for the writer monad

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

module Effect.Monad.Writer.Instances where

open import Effect.Monad.Writer.Transformer

  writerTFunctor = λ {s} {S} {f} {M} {{fun}} {{mo}}  functor {s} {S} {f} {M} {mo} fun
  writerTApplicative = λ {s} {S} {f} {M} {{mo}} {{mon}}  applicative {s} {S} {f} {M} {mo} mon
  writerTEmpty = λ {s} {S} {f} {M} {{e}} {{mo}}  empty {s} {S} {f} {M} {mo} e
  writerTChoice = λ {s} {S} {f} {M} {{ch}} {{mo}}  choice {s} {S} {f} {M} {mo} ch
  writerTApplicativeZero = λ {s} {S} {f} {M} {{mo}} {{mon}}  applicativeZero {s} {S} {f} {M} {mo} mon
  writerTAlternative = λ {s} {S} {f} {M} {{mo}} {{mpl}}  alternative {s} {S} {f} {M} {mo} mpl
  writerTMonad = λ {s} {S} {f} {M} {{mo}} {{mon}}  monad {s} {S} {f} {M} {mo} mon
  writerTMonadZero = λ {s} {S} {f} {M} {{mo}} {{mz}}  monadZero {s} {S} {f} {M} {mo} mz
  writerTMonadPlus = λ {s} {S} {f} {M} {{mo}} {{mpl}}  monadPlus {s} {S} {f} {M} {mo} mpl
  writerTMonadT = λ {s} {S} {f} {M} {{mo}} {{mon}}  monadT {s} {S} {f} {M} {mo} mon
  writerTMonadWriter = λ {s} {S} {f} {M} {{mo}} {{mon}}  monadWriter {s} {S} {f} {M} {mo} mon
  writerTLiftReaderT = λ {s} {S₁} {S₂} {f} {g} {M} {{fun}} {{mw}}  liftReaderT {s} {S₁} {S₂} {f} {g} {M} fun mw
  writerTLiftStateT = λ {s} {S₁} {S₂} {f} {g} {M} {{fun}} {{mw}}  liftStateT {s} {S₁} {S₂} {f} {g} {M} fun mw