    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Comonads
    ------------------------------------------------------------------------

    -- Note that currently the monad laws are not included here.

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

    module Effect.Comonad where

    open import Level using (Level; suc)
    open import Function.Base using (id; _∘′_; flip)

    private
      variable
        a b c f : Level
        A : Set a
        B : Set b
        C : Set c

    record RawComonad (W : Set f → Set f) : Set (suc f) where

      infixl 1 _=>>_ _=>=_
      infixr 1 _<<=_ _=<=_

      field
        extract : W A → A
        extend  : (W A → B) → (W A → W B)

      duplicate : W A → W (W A)
      duplicate = extend id

      liftW : (A → B) → W A → W B
      liftW f = extend (f ∘′ extract)

      _=>>_ : W A → (W A → B) → W B
      _=>>_ = flip extend

      _=>=_ : (W A → B) → (W B → C) → W A → C
      f =>= g = g ∘′ extend f

      _<<=_ : (W A → B) → W A → W B
      _<<=_ = extend

      _=<=_ : (W B → C) → (W A → B) → W A → C
      _=<=_ = flip _=>=_