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