open import Cat.Monoidal.Instances.Cartesian
open import Cat.Monoidal.Diagram.Monoid
open import Cat.Diagram.Product.Solver
open import Cat.Diagram.Terminal
open import Cat.Diagram.Comonad
open import Cat.Diagram.Product
open import Cat.Diagram.Monad
open import Cat.Prelude

import Cat.Reasoning as Cat

open Comonad-on
open Monad-on
open Functor
open _=>_

module Cat.Diagram.Comonad.Writer where

Writer (co)monads🔗

If $A$ is an object in a Cartesian monoidal category $\mathcal{C}\text{,}$ then the functor “product with $A$” functor, $A\times (-)\text{,}$ can naturally be equipped with the structure of a comonad. This structure embodies a particular view of $A$ as a resource, which in particular can be freely dropped and duplicated. Dropping is necessary to form the counit map ${\eta }_X:A\times X\to X\text{,}$ and duplicating becomes the comultiplication ${\delta }_X:A\times X\to A\times (A\times X)\text{.}$

module _ {o ℓ} (C : Precategory o ℓ) (A : ⌞ C ⌟) (prod : ∀ B → Product C A B) where
  open Cat C

  private module _ {B} where open Product (prod B) using (⟨_,_⟩ ; π₁ ; π₂ ; π₁∘⟨⟩ ; π₂∘⟨⟩ ; ⟨⟩∘ ; unique ; unique₂) public
  private module _ B where open Product (prod B) renaming (apex to A×) using () public

To functional programmers, the functor $A\times (-)$ is of particular importance when $A$ is equipped with a monoid structure, in which case we can make $A\times (-)$ into a monad: the Writer monad with values in $A\text{.}$ We will keep with this name even in the comonadic setting.

  Writer : Functor C C
  Writer .F₀   = A×
  Writer .F₁ f = ⟨ π₁ , f ∘ π₂ ⟩
  Writer .F-id = sym (unique (idr _) id-comm)
  Writer .F-∘ f g = sym (unique (pulll π₁∘⟨⟩ ∙ π₁∘⟨⟩) (pulll π₂∘⟨⟩ ∙ extendr π₂∘⟨⟩))

Since we’ve already decided that the comonad structure is built on dropping and duplicating, our structure maps are essentially forced on us:

  Writer-comonad : Comonad-on Writer
  Writer-comonad .counit .η x = π₂
  Writer-comonad .comult .η x = ⟨ π₁ , id ⟩

  Writer-comonad .counit .is-natural x y f = π₂∘⟨⟩
  Writer-comonad .comult .is-natural x y f = unique₂
    (pulll π₁∘⟨⟩ ∙ π₁∘⟨⟩) (pulll π₂∘⟨⟩ ∙ idl _)
    (pulll π₁∘⟨⟩ ∙ π₁∘⟨⟩) (pulll π₂∘⟨⟩ ∙ cancelr π₂∘⟨⟩)
  Writer-comonad .δ-idl = unique₂
    (pulll π₁∘⟨⟩ ∙ π₁∘⟨⟩) (pulll π₂∘⟨⟩ ∙ cancelr π₂∘⟨⟩)
    (idr _) (idr _)
  Writer-comonad .δ-idr = π₂∘⟨⟩
  Writer-comonad .δ-assoc = ⟨⟩∘ _ ∙ ap₂ ⟨_,_⟩ refl (pullr π₂∘⟨⟩ ∙ id-comm) ∙ sym (⟨⟩∘ _)

Writer monads🔗

We will now prove that the construction of Writer as a monad, familiar from functional programming, works in the generality of letting $\mathcal{C}$ be an arbitrary Cartesian monoidal category, and with $A$ equipped with an arbitrary monoid structure.

module _ {o ℓ} (C : Precategory o ℓ) (prods : ∀ A B → Product C A B) (term : Terminal C) (A : ⌞ C ⌟) where
  open Binary-products C prods
  open Terminal term
  open Cat C

The key take-away is that the usual definition works: at the level of generalised elements, the unit of the monad maps $x$ to $⟨1,x⟩\text{,}$ where $1$ is the unit of the monoid; similarly, the multiplication sends $⟨x,⟨y,z⟩⟩$ to $⟨xy,z⟩\text{,}$ where we write the monoid’s multiplication by juxtaposition.

  monoid→writer-monad
    : Monoid-on (Cartesian-monoidal prods term) A → Monad-on (Writer C A (prods A))
  monoid→writer-monad monoid = mk where
    module m = Monoid-on monoid

    mk : Monad-on _
    mk .unit .η x = ⟨ m.η ∘ ! , id ⟩
    mk .mult .η x = ⟨ m.μ ∘ ⟨ π₁ , π₁ ∘ π₂ ⟩ , π₂ ∘ π₂ ⟩

Above, we have written these structure maps in point-free style. The proof strategy for showing that these obey the monad laws is noting that this can be shown componentwise. On the “$A$ component” of the pair, we have a monoid law; and the right component is preserved. Implementing this is, again, mostly an exercise in dealing with products.

    mk .unit .is-natural x y f = ⟨⟩-unique₂ (pulll π₁∘⟨⟩) (pulll π₂∘⟨⟩ ∙ idl f)
      (pulll π₁∘⟨⟩ ∙ π₁∘⟨⟩ ∙ sym (pullr (sym (!-unique _))))
      (pulll π₂∘⟨⟩ ∙ pullr π₂∘⟨⟩ ∙ idr f)
    mk .mult .is-natural x y f = products! prods
    mk .μ-unitr =
      let
        lemma =
          m.μ ∘ ⟨ π₁ , m.η ∘ ! ∘ π₂ ⟩               ≡˘⟨ ap₂ _∘_ refl (⟨⟩-unique (pulll π₁∘⟨⟩ ∙ pullr π₁∘⟨⟩ ∙ idl π₁) (pulll π₂∘⟨⟩ ∙ pullr π₂∘⟨⟩ ∙ ap₂ _∘_ refl (!-unique _))) ⟩≡˘
          m.μ ∘ ⟨ id ∘ π₁ , m.η ∘ π₂ ⟩ ∘ ⟨ π₁ , ! ⟩ ≡⟨ pulll m.μ-unitr ⟩≡
          π₁ ∘ ⟨ π₁ , ! ⟩                           ≡⟨ π₁∘⟨⟩ ⟩≡
          π₁                                        ∎
      in ⟨⟩-unique₂ (products! prods ∙ lemma) (products! prods) (idr π₁) (idr π₂)
    mk .μ-unitl =
      let
        lemma =
          m.μ ∘ ⟨ m.η ∘ ! , π₁ ⟩                    ≡˘⟨ ap₂ _∘_ refl (⟨⟩-unique (pulll π₁∘⟨⟩ ∙ pullr π₁∘⟨⟩) (pulll π₂∘⟨⟩ ∙ pullr π₂∘⟨⟩ ∙ idl π₁)) ⟩≡˘
          m.μ ∘ ⟨ m.η ∘ π₁ , id ∘ π₂ ⟩ ∘ ⟨ ! , π₁ ⟩ ≡⟨ pulll m.μ-unitl ⟩≡
          π₂ ∘ ⟨ ! , π₁ ⟩                           ≡⟨ π₂∘⟨⟩ ⟩≡
          π₁                                        ∎
      in ⟨⟩-unique₂ (products! prods ∙ lemma) (products! prods) (idr π₁) (idr π₂)
    mk .μ-assoc {x} =
      let
        lemma =
          π₁ ∘ ⟨ m.μ ∘ ⟨ π₁ , π₁ ∘ π₂ ⟩ , π₂ ∘ π₂ ⟩ ∘ ⟨ π₁ , ⟨ m.μ ∘ ⟨ π₁ , π₁ ∘ π₂ ⟩ , π₂ ∘ π₂ ⟩ ∘ π₂ ⟩
            ≡˘⟨ products! prods ⟩≡˘
          m.μ ∘ ⟨ id ∘ π₁ , m.μ ∘ π₂ ⟩ ∘ ⟨ π₁ , ⟨ π₁ , π₁ ∘ π₂ ⟩ ∘ π₂ ⟩
            ≡⟨ extendl m.μ-assoc ⟩≡
          m.μ ∘ (⟨ m.μ ∘ π₁ , id ∘ π₂ ⟩ ∘ ⟨ ⟨ π₁ , π₁ ∘ π₂ ⟩ , π₂ ∘ π₂ ⟩) ∘ ⟨ π₁ , ⟨ π₁ , π₁ ∘ π₂ ⟩ ∘ π₂ ⟩
            ≡⟨ products! prods ⟩≡
          m.μ ∘ ⟨ m.μ ∘ ⟨ π₁ , π₁ ∘ π₂ ⟩ , π₁ ∘ π₂ ∘ π₂ ⟩
            ∎
      in ⟨⟩-unique₂ lemma (products! prods)
        (pulll π₁∘⟨⟩ ∙ pullr (⟨⟩-unique (pulll π₁∘⟨⟩ ∙ π₁∘⟨⟩) (pulll π₂∘⟨⟩ ∙ pullr π₂∘⟨⟩)))
        (pulll π₂∘⟨⟩ ∙ pullr π₂∘⟨⟩)