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

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

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

module Category.Comonad where

open import Level
open import Function

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  _=>>_ _=>=_
  infixr  _<<=_ _=<=_

  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 _=>=_