open import Cat.Functor.Adjoint
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Reasoning

module Cat.Diagram.Comonad {o ℓ} (C : Precategory o ℓ) where

open Cat.Reasoning C

open Functor
open _=>_

Comonads🔗

A comonad on a category $\mathcal{C}$ is dual to a monad on $\mathcal{C}\text{;}$ instead of a unit $\mathrm{Id}\Rightarrow M$ and multiplication $(M\circ M)\Rightarrow M\text{,}$ we have a counit $M\Rightarrow \mathrm{Id}$ and comultiplication $M\Rightarrow (M\circ M)\text{.}$

record Comonad : Type (o ⊔ ℓ) where
  field
    W : Functor C C
    counit : W => Id
    comult : W => (W F∘ W)

  module counit = _=>_ counit renaming (η to ε)
  module comult = _=>_ comult

  W₀ = W .F₀
  W₁ = W .F₁
  W-id = W .F-id
  W-∘ = W .F-∘

We also have equations governing the counit and comultiplication. Unsurprisingly, these are dual to the equations of a monad.

  field
    left-ident : ∀ {x} → W₁ (counit.ε x) ∘ comult.η x ≡ id
    right-ident : ∀ {x} → counit.ε (W₀ x) ∘ comult.η x ≡ id
    comult-assoc : ∀ {x} → W₁ (comult.η x) ∘ comult.η x ≡ comult.η (W₀ x) ∘ comult.η x