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 _ monad .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⊣Forget _ monad)
idempotent→reflective idem = full+faithful→ff (Forget _ monad)
  (Ξ» {(A , a)} {(B , b)} f β†’ inc (algebra-hom f
    (sym (swizzle (sym (unit.is-natural _ _ _))
      (η≑MΞ·β†’algebra-invertible (idempotent→η≑MΞ· idem) (A , a) .is-invertible.invr)
      (b .Ξ½-unit)))
    , refl))
  (Forget-is-faithful _ monad)

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⊣Forget _ monad) β†’ is-idempotent-monad
reflectiveβ†’idempotent ref = invertibleβ†’invertibleⁿ _ Ξ» A β†’
  iso→invertible (F-map-iso (Forget _ monad)
    (is-reflectiveβ†’counit-is-iso (Free⊣Forget _ monad) ref
      {Free _ monad .Fβ‚€ A}))

idempotent≃reflective : is-idempotent-monad ≃ is-reflective (Free⊣Forget _ monad)
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₁ Ξ΄                                                             ∎