Skip to content

Setoid.Categories.Monad

Monads on a minimal category

This is the Setoid.Categories.Monad module of the Agda Universal Algebra Library.

A monad is the categorical abstraction of the notion of

a formal expression that can be nested and then flattened.

It consists of an endofunctor T : 𝐂 → 𝐂 — read T A as "formal expressions over A" — together with two natural transformations:

  • the unit η : Id ⟹ T, which regards a plain A as a trivial expression (a variable is already a term; an element is already a just-value);
  • the multiplication μ : T ∘ T ⟹ T, which flattens an expression whose leaves are themselves expressions into a single expression (substituting terms for variables; collapsing Maybe (Maybe A) to Maybe A).

Three laws make the metaphor exact, and each says something a working algebraist already believes about substitution. Writing μ_A : T (T A) → T A for the component at A:

            T η_A                  η_{T A}                     T μ_A
      T A ────────→ T (T A)    T A ────────→ T (T A)    T³ A ─────────→ T² A

          ╲         │             ╲          │          │               │
           ╲        │ μ_A          ╲         │ μ_A      │ μ_{T A}       │ μ_A
        id  ╲       │            id ╲        │          │               │
             ╲      │                ╲       │          │               │
              ╲     │                 ╲      │          │               │
               ╲    │                  ╲     │          │               │
                ↘   ↓                  ↘     ↓          ↓               ↓
                 T A                      T A         T² A ─────────→  T A
                                                               μ_A
  • identityˡ (left triangle): wrapping every leaf as a trivial expression and then flattening changes nothing — substituting the variable x for each variable x is the identity substitution.
  • identityʳ (right triangle): wrapping the whole expression as a trivial expression-of-expressions and flattening changes nothing.
  • assoc (the square): given three layers of nesting, flattening the inner two layers first or the outer two layers first yields the same result — exactly the associativity of substitution composition.

The slogan "a monad is a monoid in the category of endofunctors" is visible in the field names: μ is the multiplication, η the unit, and the laws are the monoid laws, written with ∘ because the elements being multiplied are functors.

This record is the M4-5e extension of the self-contained ADR-006 vocabulary, built on NaturalTransformation exactly as promised by the footnote of Setoid.Categories.Adjunction: the unit and multiplication are bundled natural transformations (so their naturality squares come packaged), while the three monad laws are stated componentwise against 𝐂's hom-equality — the same convention as Adjunction's componentwise fields, and for the same reason: componentwise statements are what instances can prove pointwise under --safe, with no function extensionality.

Two instances anchor the abstraction in this library:

  • From an adjunction. Every adjunction L ⊣ R induces a monad on the domain of L, with T = R ∘F L, unit the adjunction's unit, and multiplication obtained by running the counit inside R. This is proved in general below (adjunction→monad) and instantiated in Classical.Categories.AdjoinUnit: adjoining a unit to a semigroup and then forgetting down again is a monad on the category of semigroups (the "Maybe monad on semigroups").
  • The term monad — the motivating example, where T X is the type of terms over variables X, η is the generator injection ℊ, and μ is substitution. In a predicative universe hierarchy Term raises levels (Term X : Type (ov χ) for X : Type χ), so it is not an endofunctor of any one category Setoid α ρ and cannot inhabit this record; it is a relative monad, and its laws are stated in the equivalent Kleisli form in Setoid.Terms.Monad. See docs/notes/m4-5e-term-monad.md for why this is a fact about predicativity, not a defect of the formalization.
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Categories.Monad where

open import Agda.Primitive  using ( _⊔_ ) renaming ( Set to Type )
open import Level           using ( Level )

open import Setoid.Categories.Category               using ( Category )
open import Setoid.Categories.Functor                using ( Functor ; idF ; _∘F_ )
open import Setoid.Categories.NaturalTransformation  using ( NaturalTransformation )
open import Setoid.Categories.Adjunction             using ( Adjunction )

private variable o ℓ e o′ ℓ′ e′ : Level

The record

record Monad (𝐂 : Category o ℓ e) : Type (o ⊔ ℓ ⊔ e) where
  open Category 𝐂 using (_≈_ ; _∘_ ) renaming (Hom to 𝐂[_,_]; id to idC; Obj to 𝐂₀)

  field
    T     : Functor 𝐂 𝐂
    unit  : NaturalTransformation (idF {𝐂 = 𝐂}) T
    mult  : NaturalTransformation (T ∘F T) T

  -- Component shorthands: η_A : A ⟶ T A and μ_A : T (T A) ⟶ T A.
  open Functor T renaming ( F₀ to T₀ ; F₁ to T₁ ) public

  η : (A : 𝐂₀) → 𝐂[ A , T₀ A ]
  η = NaturalTransformation.component unit

  μ : (A : 𝐂₀) → 𝐂[ T₀ (T₀ A) , T₀ A ]
  μ = NaturalTransformation.component mult

  field
    -- Flattening three layers from the inside or from the outside agrees.
    assoc : (A : 𝐂₀) → μ A ∘ T₁ (μ A) ≈ μ A ∘ μ (T₀ A)

    -- Wrapping each leaf trivially, then flattening, is the identity.
    identityˡ : (A : 𝐂₀) → μ A ∘ T₁ (η A) ≈ idC

    -- Wrapping the whole expression trivially, then flattening, is the identity.
    identityʳ : (A : 𝐂₀) → μ A ∘ η (T₀ A) ≈ idC

Every adjunction induces a monad

This is the classical Huber/Eilenberg–Moore observation, and it is the bridge from the free-expansion adjunction of M4-5d to the monad vocabulary of M4-5e. Given L ⊣ R with unit η and counit ε, the composite T = R ∘F L is a monad on 𝐂:

  • the monad unit is the adjunction unit η_A : A ⟶ R (L A);
  • the multiplication is the counit, transported into 𝐂 by R: μ_A = R₁ (ε_{L A}) : R (L (R (L A))) ⟶ R (L A) — flattening means "evaluate the inner formal layer with the counit."

The intuition for the proof obligations: everything about μ is a statement about ε wearing an R₁ coat. Each proof below therefore has the same three moves — collect the two R₁s into one (homomorphism, read right to left), rewrite inside R₁ using a fact about the counit (its naturality, or a triangle identity), and redistribute. The monad's right unit law needs no moves at all: it is the zag triangle identity, on the nose.

module _
  {𝐂 : Category o ℓ e} {𝐃 : Category o′ ℓ′ e′}
  {L : Functor 𝐂 𝐃} {R : Functor 𝐃 𝐂}
  (adj : Adjunction L R)
  where
  open Category 𝐂 using ( ≈-sym ; ≈-trans )
  open Functor L using () renaming ( F₀ to L₀ ; F₁ to L₁ )
  open Functor R using ( F-resp-≈ ; identity ; homomorphism ) renaming ( F₁ to R₁ )
  open Adjunction adj

  adjunction→monad : Monad 𝐂
  adjunction→monad = record
    { T     = R ∘F L
    ; unit  = record  { component = unit ; natural = unit-natural }
    ; mult  = record  { component = λ A → R₁ (ε (L₀ A))

                        -- Naturality of μ: push both R₁s together, apply the counit's
                        -- naturality square inside R₁, and split them apart again.
                      ; natural = λ f → ≈-trans  (≈-sym homomorphism)
                                                 (≈-trans  (F-resp-≈ (counit-natural (L₁ f)))
                                                           homomorphism)
                      }

    -- In R₁, the two flattenings differ by the counit's naturality square taken at ε itself.
    ; assoc = λ A → ≈-trans  (≈-sym homomorphism)
                             (≈-trans  (F-resp-≈ (counit-natural (counit (L₀ A))))
                                       homomorphism)

    -- In R₁, the composite is the zig triangle, which collapses to the id; R₁ id is id.
    ; identityˡ  = λ A → ≈-trans (≈-sym homomorphism) (≈-trans (F-resp-≈ (zig A)) identity)

    -- This is literally the zag triangle identity at L₀ A.
    ; identityʳ  = λ A → zag (L₀ A)
    }

For the reader meeting this for the first time, it is worth unwinding identityʳ by hand once: the law asks for

μ_A ∘ η_{T A} ≈ id

i.e. R₁ (ε_{L A}) ∘ η_{R (L A)} ≈ id, and that is exactly the zag field of the adjunction at the object L₀ A — the triangle identities of an adjunction are the unit laws of its monad; this is no accident and is the historical origin of both.