module Cat.Diagram.Monad.Idempotent {o }
  {C : Precategory o } (monad : Monad C)
  where

Idempotent monads🔗

A monad is said to be idempotent if it “squares to itself” in the sense that its multiplication is a natural isomorphism

is-idempotent-monad : Type (o  )
is-idempotent-monad = is-invertibleⁿ mult

The intuition is that an idempotent monad on equips its algebras with property, rather than structure: in that sense, it contains exactly as much information as a reflective subcategory of More precisely, the forgetful functor from the Eilenberg-Moore category of an idempotent monad is a reflective subcategory inclusion, and conversely any reflective adjunction yields an idempotent monad

This means that idempotent monads may be used to interpret modalities in type theory. As a motivating, if informal, example, think of the ( of types and functions: the property of being an -type defines a reflective subuniverse whose corresponding idempotent monad is the truncation operator.

We start by showing the following elementary characterisation: a monad is idempotent if and only if are equal. In the forwards direction, the monad laws tell us that and we’ve assumed that is invertible, hence in particular monic.

opaque
  idempotent→η≡Mη : is-idempotent-monad   A  η (M₀ A)  M₁ (η A)
  idempotent→η≡Mη idem A = invertible→monic
    (is-invertibleⁿ→is-invertible idem A) _ _
    (right-ident  sym left-ident)

For the other direction, we can prove a slightly more general result: assuming any algebra is invertible. Indeed, algebra laws guarantee that is a right inverse of we check that it is also a left inverse by a short computation involving the naturality of

η≡Mη→algebra-invertible
  : (∀ A  η (M₀ A)  M₁ (η A))
    (A : Algebra monad)
   is-invertible (A .snd .ν)
η≡Mη→algebra-invertible h (A , alg) = make-invertible (η _) (alg .ν-unit) $
  η A  alg .ν           ≡⟨ unit.is-natural _ _ _ 
  M₁ (alg .ν)  η (M₀ A) ≡⟨ refl⟩∘⟨ h A 
  M₁ (alg .ν)  M₁ (η A) ≡⟨ M.annihilate (alg .ν-unit) 
  id                     

In particular, by applying this to the free algebras we get that is componentwise invertible.

η≡Mη→idempotent : (∀ A  η (M₀ A)  M₁ (η A))  is-idempotent-monad
η≡Mη→idempotent h = invertible→invertibleⁿ _ λ A 
  η≡Mη→algebra-invertible h (Free-EM .F₀ A)

idempotent≃η≡Mη : is-idempotent-monad  (∀ A  η (M₀ A)  M₁ (η A))
idempotent≃η≡Mη = prop-ext! idempotent→η≡Mη η≡Mη→idempotent

As a consequence, if is only componentwise monic, then we can still conclude that and hence that is idempotent.

μ-monic→idempotent : (∀ A  is-monic (μ A))  is-idempotent-monad
μ-monic→idempotent monic = η≡Mη→idempotent λ A 
  monic _ _ _ (right-ident  sym left-ident)

Finally, we turn to showing the equivalence with reflective subcategories.

The forgetful functor out of the Eilenberg-Moore category is always faithful, so we need to show that it is full; that is, that any map between is an algebra morphism, in that it makes the outer square commute:

As we showed earlier, the algebras and are both inverses of so this reduces to showing that the inner square commutes, which is just the naturality of

idempotent→reflective : is-idempotent-monad  is-reflective Free-EM⊣Forget-EM
idempotent→reflective idem = full+faithful→ff Forget-EM
   {(A , a)} {(B , b)} f  inc (total-hom f
    (sym (swizzle (sym (unit.is-natural _ _ _))
      (η≡Mη→algebra-invertible (idempotent→η≡Mη idem) (A , a) .is-invertible.invr)
      (b .ν-unit)))
    , refl))
  Forget-EM-is-faithful

In the other direction, we will show that, if the free-forgetful adjunction is reflective, then is an idempotent monad. Note that this doesn’t lose any generality over our initial claim, since any reflective adjunction is monadic!

Since the adjunction is reflective, we know the counit of the adjunction is an isomorphism; hence the whiskering must be as well, but this is exactly the multiplication of our monad.

reflective→idempotent : is-reflective (Free-EM⊣Forget-EM {M = monad})  is-idempotent-monad
reflective→idempotent ref = invertible→invertibleⁿ _ λ A 
  iso→invertible (F-map-iso Forget-EM
    (is-reflective→counit-is-iso Free-EM⊣Forget-EM ref
      {Free-EM .F₀ A}))

idempotent≃reflective : is-idempotent-monad  is-reflective Free-EM⊣Forget-EM
idempotent≃reflective = prop-ext! idempotent→reflective reflective→idempotent

Strong idempotent monads🔗

Being an idempotent monad is quite a strong property. Indeed, if the monad is also strong, then it has to be commutative.

Source

The following proof comes from the nLab page on idempotent monads; see there for a diagram.

  opaque
    idempotent→commutative : is-commutative-strength s
    idempotent→commutative = ext λ (A , B) 
      μ _  M₁ τ  σ                                              ≡⟨ insertl right-ident 
      μ _  η _  μ _  M₁ τ  σ                                  ≡⟨ refl⟩∘⟨ unit.is-natural _ _ _ 
      μ _  M₁ (μ _  M₁ τ  σ)  η _                             ≡˘⟨ refl⟩∘⟨ refl⟩∘⟨ right-strength-η ≡˘
      μ _  M₁ (μ _  M₁ τ  σ)  τ  ( η _  ⊗₁ id)             ≡⟨ ap! (idempotent→η≡Mη idem _) 
      μ _  M₁ (μ _  M₁ τ  σ)  τ  (M₁ (η _) ⊗₁ id)            ≡⟨ refl⟩∘⟨ refl⟩∘⟨ τ.is-natural _ _ _ 
      μ _  M₁ (μ _  M₁ τ  σ)  M₁ (η _ ⊗₁  id )  τ          ≡˘⟨ ap¡ M-id ≡˘
      μ _  M₁ (μ _  M₁ τ  σ)  M₁ (η _ ⊗₁ M₁ id)  τ           ≡⟨ refl⟩∘⟨ M.popr (M.popr (extendl (M.weave (σ.is-natural _ _ _)))) 
      μ _  M₁ (μ _)  M₁ (M₁ τ)  M₁ (M₁ (η _ ⊗₁ id))  M₁ σ  τ ≡⟨ refl⟩∘⟨ refl⟩∘⟨ M.pulll (M.collapse right-strength-η) 
      μ _  M₁ (μ _)  M₁ (M₁ (η _))  M₁ σ  τ                   ≡⟨ refl⟩∘⟨ M.cancell left-ident 
      μ _  M₁ σ  τ                                              

If furthermore we are in a monoidal category with diagonals, then the monoidal functor induced by the strength is automatically an idempotent monoidal functor.

The proof is by chasing the following slightly wonky diagram.

  module _ (Cᵈ : Diagonals Cᵐ) where
    open Diagonals Cᵈ

    opaque
      idempotent-monad→diagonal
        : is-diagonal-functor _ _ Cᵈ Cᵈ (M , strength→monoidal s)
      idempotent-monad→diagonal =
        (μ _  M₁ σ  τ)  δ                                             ≡⟨ pullr (pullr (insertl right-ident)) 
        μ _  M₁ σ  μ _  η _  τ  δ                                   ≡⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ unit.is-natural _ _ _ 
        μ _  M₁ σ  μ _  M₁ (τ  δ)  η _                              ≡⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ idempotent→η≡Mη idem _ 
        μ _  M₁ σ  μ _  M₁ (τ  δ)  M₁ (η _)                         ≡⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ M.pushl refl 
        μ _  M₁ σ  μ _  M₁ τ  M₁ δ  M₁ (η _)                        ≡⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ M.weave (δ.is-natural _ _ _) 
        μ _  M₁ σ  μ _  M₁ τ  M₁ (η _ ⊗₁ η _)  M₁ δ                 ≡⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ M.pushl (⊗.expand (sym (idr _) ,ₚ sym (idl _))) 
        μ _  M₁ σ  μ _  M₁ τ  M₁ (η _ ⊗₁ id)  M₁ (id ⊗₁ η _)  M₁ δ ≡⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ M.pulll right-strength-η 
        μ _  M₁ σ  μ _  M₁ (η _)  M₁ (id ⊗₁ η _)  M₁ δ              ≡⟨ refl⟩∘⟨ refl⟩∘⟨ cancell left-ident 
        μ _  M₁ σ  M₁ (id ⊗₁ η _)  M₁ δ                               ≡⟨ refl⟩∘⟨ M.pulll left-strength-η 
        μ _  M₁ (η _)  M₁ δ                                            ≡⟨ cancell left-ident 
        M₁ δ