open import Cat.Functor.Adjoint.Reflective
open import Cat.Monoidal.Strength.Monad
open import Cat.Functor.Naturality
open import Cat.Functor.Properties
open import Cat.Monoidal.Diagonals
open import Cat.Monoidal.Functor
open import Cat.Displayed.Total
open import Cat.Diagram.Monad
open import Cat.Monoidal.Base
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Functor.Reasoning
import Cat.Reasoning

open Algebra-on
open Functor

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

Idempotent monads🔗

open Cat.Reasoning C
open Monad monad
private
  module M = Cat.Functor.Reasoning M

A monad $M$ is said to be idempotent if it “squares to itself” in the sense that its multiplication is a natural isomorphism $\mu :M^2\cong M\text{.}$

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

The intuition is that an idempotent monad on $\mathcal{C}$ equips its algebras with property, rather than structure: in that sense, it contains exactly as much information as a reflective subcategory of $\mathcal{C}\text{.}$ More precisely, the forgetful functor from the Eilenberg-Moore category of an idempotent monad is a reflective subcategory inclusion, and conversely any reflective adjunction $F⊣U$ yields an idempotent monad $UF\text{.}$

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

We start by showing the following elementary characterisation: a monad is idempotent if and only if $\eta M,M\eta :M\Rightarrow M^2$ are equal. In the forwards direction, the monad laws tell us that $\mu \circ \eta M\equiv \mu \circ M\eta \text{,}$ and we’ve assumed that $\mu$ 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 $\eta M\equiv M\eta \text{,}$ any $M\text{-}$algebra $\nu :MA\to A$ is invertible. Indeed, algebra laws guarantee that $\eta M$ is a right inverse of $\nu \text{;}$ we check that it is also a left inverse by a short computation involving the naturality of $\eta \text{.}$

η≡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 $\mu$ 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 $\mu$ is only componentwise monic, then we can still conclude that $\eta M\equiv M\eta$ and hence that $M$ 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 $f:A\to B$ between $M\text{-algebras}$ is an algebra morphism, in that it makes the outer square commute:

As we showed earlier, the algebras $a$ and $b$ are both inverses of $\eta \text{,}$ so this reduces to showing that the inner square commutes, which is just the naturality of $\eta \text{.}$

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

_ = is-reflective→is-monadic

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

Since the adjunction is reflective, we know the counit of the adjunction $\epsilon :F\circ U\Rightarrow \mathrm{Id}$ is an isomorphism; hence the whiskering $U\epsilon F$ 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.

module _ (idem : is-idempotent-monad) (Cᵐ : Monoidal-category C) (s : Monad-strength Cᵐ monad) where
  open Monoidal-category Cᵐ
  open Monad-strength s

  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₁ δ                                                             ∎