---
description: |
  Idempotent systems.
---
```agda
open import Cat.Diagram.Monad
open import Cat.Prelude

import Cat.Reasoning
import Cat.Functor.Reasoning
import Cat.Diagram.Idempotent

module Cat.Morphism.Idempotent.System where
```

# Idempotent systems

Let $C$ be a category, $F : C \to C$ be an endofunctor, and $e_{A} : C(F(A), F(A))$
be a family of morphisms in $C$. We say that $e_{A}$ is an **idempotent system**
if for all $f : C(A,B)$, $e_{B} \circ F(f) \circ e_{A}  = e_{B} \circ F(f)$.

```agda
module _ {o ℓ} {C : Precategory o ℓ} (F : Functor C C) where
  private
    open Cat.Reasoning C
    open Cat.Diagram.Idempotent C
    open Functor F
    module F = Cat.Functor.Reasoning

  is-idempotent-system : (∀ (a : Ob) → Hom (F₀ a) (F₀ a)) → Type _
  is-idempotent-system e = ∀ {a b} (f : Hom a b) → e b ∘ F₁ f ∘ e a ≡ e b ∘ F₁ f

  record Idempotent-system : Type (o ⊔ ℓ) where
    no-eta-equality
    field
      η        : ∀ a → Hom (F₀ a) (F₀ a)
      idem-sys : is-idempotent-system η
```

Note that every component of an idempotent system is idempotent.

```agda
  is-idempotent-system→is-idempotent
    : {e : ∀ (a : Ob) → Hom (F₀ a) (F₀ a)}
    → is-idempotent-system e
    → ∀ a → is-idempotent (e a)
  is-idempotent-system→is-idempotent {e = e} nat-idem a =
    e a ∘ e a         ≡⟨ refl⟩∘⟨ introl F-id ⟩
    e a ∘ F₁ id ∘ e a ≡⟨ nat-idem id ⟩
    e a ∘ F₁ id       ≡⟨ elimr F-id ⟩
    e a               ∎
```

An idempotent system is **split** if every component of the family
is a split idempotent.

```agda
  record Split-idempotent-system : Type (o ⊔ ℓ) where
    field
      S : Ob → Ob
      ηₛ : ∀ a → Hom (S a) (F₀ a)
      ηᵣ : ∀ a → Hom (F₀ a) (S a)
      retracts : ∀ a → ηᵣ a retract-of ηₛ a

    ηₛ-has-retract : ∀ a → has-retract (ηₛ a)
    ηₛ-has-retract a = make-retract (ηᵣ a) (retracts a)

    ηᵣ-has-section : ∀ a → has-section (ηᵣ a)
    ηᵣ-has-section a = make-section (ηₛ a) (retracts a)

    field
      idem-sys : is-idempotent-system (λ a → ηₛ a ∘ ηᵣ a)

    ηᵣ-sys
      : ∀ {a b} (f : Hom a b)
      → ηᵣ b ∘ F₁ f ∘ (ηₛ a ∘ ηᵣ a) ≡ ηᵣ b ∘ F₁ f
    ηᵣ-sys f = has-retract→monic (ηₛ-has-retract _) _ _ $
      ηₛ _ ∘ ηᵣ _ ∘ F₁ f ∘ ηₛ _ ∘ ηᵣ _   ≡⟨ assoc _ _ _ ⟩
      (ηₛ _ ∘ ηᵣ _) ∘ F₁ f ∘ ηₛ _ ∘ ηᵣ _ ≡⟨ idem-sys f ⟩
      (ηₛ _ ∘ ηᵣ _) ∘ F₁ f               ≡˘⟨ assoc _ _ _ ⟩
      ηₛ _ ∘ ηᵣ _ ∘ F₁ f                 ∎

    system : Idempotent-system
    system .Idempotent-system.η a = ηₛ a ∘ ηᵣ a
    system .Idempotent-system.idem-sys = idem-sys
```

The existence of a split idempotent system induces a new endofunctor
on $C$, which we call the *idempotent restriction* of $F$.

```agda
  module _ (e : Split-idempotent-system) where
    open Split-idempotent-system e

    Idem : Functor C C
    Idem .Functor.F₀ = S 
    Idem .Functor.F₁ f = ηᵣ _ ∘ F₁ f ∘ ηₛ _
    Idem .Functor.F-id =
      ηᵣ _ ∘ F₁ id ∘ ηₛ _ ≡⟨ refl⟩∘⟨ eliml F-id ⟩
      ηᵣ _ ∘ ηₛ _         ≡⟨ retracts _ ⟩
      id ∎
    Idem .Functor.F-∘ f g =
      ηᵣ _ ∘ F₁ (f ∘ g) ∘ ηₛ _                    ≡⟨ extendl (pushr (F-∘ _ _)) ⟩
      (ηᵣ _ ∘ F₁ f) ∘ (F₁ g ∘ ηₛ _)               ≡⟨ pushl (sym (ηᵣ-sys f) ∙ pushr (assoc _ _ _)) ⟩
      (ηᵣ _ ∘ F₁ f ∘ ηₛ _) ∘ (ηᵣ _ ∘ F₁ g ∘ ηₛ _) ∎
```

## Monadic Idempotent Systems

Let $e$ be an idempotent system on a monad $(M, \eta, \mu)$. We say that $e$ is **monadic** if:
* $e_{A} \circ \eta_{A} = \eta_{A}$, and
* $M(e_{A}) \circ \mu_{A} \circ M(e_{A}) = e_{A} \circ \mu_A$, and
* $M(e_{A}) \circ \mu_{A} e_{M(A)} = e_{A} \circ \mu_A$

```agda
module _
  {o ℓ} {C : Precategory o ℓ}
  (monad : Monad C)
  where
  open Cat.Reasoning C
  open Monad monad
  open _=>_

  record is-monadic-idempotent-system (e : Idempotent-system M) : Type (o ⊔ ℓ) where
    no-eta-equality
    private
      module e = Idempotent-system e
    field
      unit-sys : ∀ a → e.η a ∘ unit.η a ≡ unit.η a
      mult-sys-inner : ∀ a → e.η a ∘ mult.η a ∘ M₁ (e.η a) ≡ e.η a ∘ mult.η a
      mult-sys-outer : ∀ a → e.η a ∘ mult.η a ∘ e.η (M₀ a) ≡ e.η a ∘ mult.η a
```

A split idempotent system is **split monadic** if it is monadic, and comes equipped
with the following interchange law for every section/rectraction pair $(s_{a}, r_{a})$:
* $M(s_a) \circ s_{S(a)} \circ r_{S(a) \circ M(r_{a}) = s_{M(a)} \circ r_{M(a)} \circ M(s_{a}) \circ M(r_{a}) }$

```agda
  record is-split-monadic-idempotent-system (e : Split-idempotent-system M) : Type (o ⊔ ℓ) where
    no-eta-equality
    open Split-idempotent-system e
    field
      is-monadic : is-monadic-idempotent-system system

    open is-monadic-idempotent-system is-monadic public
    field
      interchange : ∀ a → (M₁ (ηₛ a) ∘ ηₛ (S a)) ∘ (ηᵣ (S a) ∘ M₁ (ηᵣ a)) ≡ (ηₛ (M₀ a) ∘ ηᵣ (M₀ a)) ∘ M₁ (ηₛ a ∘ ηᵣ a)

    ηᵣ-mult-inner : ∀ a → ηᵣ a ∘ mult.η a ∘ M₁ (ηₛ _ ∘ ηᵣ _) ≡ ηᵣ a ∘ mult.η a
    ηᵣ-mult-inner a = has-retract→monic (ηₛ-has-retract _) _ _ $
      ηₛ a ∘ ηᵣ a ∘ mult.η a ∘ M₁ (ηₛ a ∘ ηᵣ a)   ≡⟨ assoc _ _ _ ⟩
      (ηₛ a ∘ ηᵣ a) ∘ mult.η a ∘ M₁ (ηₛ a ∘ ηᵣ a) ≡⟨ mult-sys-inner a ⟩
      (ηₛ a ∘ ηᵣ a) ∘ mult.η a                    ≡˘⟨ assoc _ _ _ ⟩
      ηₛ a ∘ ηᵣ a ∘ mult.η a                      ∎

    ηᵣ-mult-outer : ∀ a → ηᵣ a ∘ mult.η a ∘ ηₛ _ ∘ ηᵣ _ ≡ ηᵣ a ∘ mult.η a
    ηᵣ-mult-outer a = has-retract→monic (ηₛ-has-retract _) _ _ $
      ηₛ a ∘ ηᵣ a ∘ mult.η a ∘ ηₛ (M₀ a) ∘ ηᵣ (M₀ a)   ≡⟨ assoc _ _ _ ⟩
      (ηₛ a ∘ ηᵣ a) ∘ mult.η a ∘ ηₛ (M₀ a) ∘ ηᵣ (M₀ a) ≡⟨ mult-sys-outer a ⟩
      (ηₛ a ∘ ηᵣ a) ∘ mult.η a                         ≡˘⟨ assoc _ _ _ ⟩
      ηₛ a ∘ ηᵣ a ∘ mult.η a                           ∎
```

If $e$ is split monadic, then the idempotent restriction of $M$ along
$e$ inherits the monadic structure of $M$.

```agda
  module _
    (e : Split-idempotent-system M)
    (monadic : is-split-monadic-idempotent-system e)
    where
    private
      open Split-idempotent-system e
      open is-split-monadic-idempotent-system monadic
      module M = Cat.Functor.Reasoning M

    Idem-monad : Monad C
    Idem-monad .Monad.M = Idem M e
    Idem-monad .Monad.unit .η a = ηᵣ a ∘ unit.η a
    Idem-monad .Monad.unit .is-natural x y f =
      (ηᵣ y ∘ unit.η y) ∘ f  ≡⟨ pullr (unit.is-natural x y f) ⟩
      ηᵣ y ∘ M₁ f ∘ unit.η x ≡⟨ extendl (sym (ηᵣ-sys f) ∙ pushr (assoc _ _ _)) ⟩
      (ηᵣ y ∘ M₁ f ∘ ηₛ x) ∘ (ηᵣ x ∘ unit.η x) ∎
    Idem-monad .Monad.mult .η a = ηᵣ a ∘ mult.η a ∘ M₁ (ηₛ a) ∘ ηₛ (S a)
    Idem-monad .Monad.mult .is-natural x y f =
      (ηᵣ y ∘ mult.η y ∘ M₁ (ηₛ y) ∘ ηₛ (S y)) ∘ (ηᵣ (S y) ∘ M₁ (ηᵣ y ∘ M₁ f ∘ ηₛ x) ∘ ηₛ (S x))             ≡⟨ (refl⟩∘⟨ pushη) ⟩
      (ηᵣ y ∘ mult.η y ∘ M₁ (ηₛ y) ∘ ηₛ (S y)) ∘ ((ηᵣ (S y) ∘ M₁ (ηᵣ y)) ∘ M₁ (M₁ f) ∘ M₁ (ηₛ x) ∘ ηₛ (S x)) ≡⟨ extendr (extendr (extendl (interchange y))) ⟩
      (ηᵣ y ∘ mult.η y ∘ ηₛ (M₀ y) ∘ ηᵣ (M₀ y)) ∘ (M₁ (ηₛ y ∘ ηᵣ y) ∘ M₁ (M₁ f) ∘ M₁ (ηₛ x) ∘ ηₛ (S x))      ≡⟨ (ηᵣ-mult-outer _ ⟩∘⟨refl) ⟩
      (ηᵣ y ∘ mult.η y) ∘ (M₁ (ηₛ y ∘ ηᵣ y) ∘ M₁ (M₁ f) ∘ M₁ (ηₛ x) ∘ ηₛ (S x))                              ≡⟨ pulll (sym (assoc _ _ _) ∙ ηᵣ-mult-inner _) ⟩
      (ηᵣ y ∘ mult.η y) ∘ (M₁ (M₁ f) ∘ M₁ (ηₛ x) ∘ ηₛ (S x))                                                 ≡⟨ extendr (extendl (mult.is-natural _ _ _)) ⟩
      (ηᵣ y ∘ M₁ f) ∘ (mult.η x ∘ M₁ (ηₛ x) ∘ ηₛ (S x))                                                      ≡˘⟨ ηᵣ-sys f ⟩∘⟨refl ⟩
      (ηᵣ y ∘ M₁ f ∘ ηₛ x ∘ ηᵣ x) ∘ (mult.η x ∘ M₁ (ηₛ x) ∘ ηₛ (S x))                                        ≡⟨ extendr (extendr (sym (assoc _ _ _))) ⟩
      (ηᵣ y ∘ M₁ f ∘ ηₛ x) ∘ (ηᵣ x ∘ mult.η x ∘ M₁ (ηₛ x) ∘ ηₛ (S x))                                        ∎
      where
        pushη : ηᵣ (S y) ∘ M₁ (ηᵣ y ∘ M₁ f ∘ ηₛ x) ∘ ηₛ (S x) ≡ (ηᵣ (S y) ∘ M₁ (ηᵣ y)) ∘ M₁ (M₁ f) ∘ M₁ (ηₛ x) ∘ ηₛ (S x)
        pushη = pushr $
          M₁ (ηᵣ y ∘ M₁ f ∘ ηₛ x) ∘ ηₛ (S x)      ≡⟨ pushl (M-∘ _ _) ⟩
          M₁ (ηᵣ y) ∘ M₁ (M₁ f ∘ ηₛ x) ∘ ηₛ (S x) ≡⟨ refl⟩∘⟨ (pushl (M-∘ _ _)) ⟩
          M₁ (ηᵣ y) ∘ M₁ (M₁ f) ∘ M₁ (ηₛ x) ∘ ηₛ (S x) ∎
    Idem-monad .Monad.left-ident =
      (ηᵣ _ ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _) ∘ (ηᵣ _ ∘ M₁ (ηᵣ _ ∘ unit.η _) ∘ ηₛ _)        ≡⟨ refl⟩∘⟨ (pushr (pushl (M-∘ _ _))) ⟩
      (ηᵣ _ ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _) ∘ ((ηᵣ _ ∘ M₁ (ηᵣ _)) ∘ M₁ (unit.η _) ∘ ηₛ _) ≡⟨ extendr (extendr (extendl (interchange _))) ⟩
      (ηᵣ _ ∘ mult.η _ ∘ (ηₛ _ ∘ ηᵣ _)) ∘ (M₁ (ηₛ _ ∘ ηᵣ _) ∘ M₁ (unit.η _) ∘ ηₛ _)      ≡⟨ ap₂ _∘_ (ηᵣ-mult-outer _) (M.pulll (unit-sys _)) ⟩
      (ηᵣ _ ∘ mult.η _) ∘ (M₁ (unit.η _) ∘ ηₛ _)                                         ≡⟨ cancel-inner left-ident ⟩
      ηᵣ _ ∘ ηₛ _                                                                        ≡⟨ retracts _ ⟩
      id                                                                                 ∎
    Idem-monad .Monad.right-ident =
      (ηᵣ _ ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _) ∘ (ηᵣ _ ∘ unit.η _) ≡⟨ extendr (extendr (pullr (assoc _ _ _ ∙ unit-sys _))) ⟩
      (ηᵣ _ ∘ mult.η _ ∘ M₁ (ηₛ _)) ∘ unit.η _                 ≡⟨ extendr (pullr (sym (unit .is-natural _ _ _))) ⟩
      (ηᵣ _ ∘ mult.η _) ∘ (unit.η _ ∘ ηₛ _)                    ≡⟨ cancel-inner right-ident ⟩
      ηᵣ _ ∘ ηₛ _                                              ≡⟨ retracts _ ⟩
      id                                                       ∎
    Idem-monad .Monad.mult-assoc =
      (ηᵣ _ ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _) ∘ (ηᵣ _ ∘ M₁ (ηᵣ _ ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _) ∘ ηₛ _)                  ≡⟨ refl⟩∘⟨ pushη ⟩
      (ηᵣ _ ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _) ∘ ((ηᵣ _ ∘ M₁ (ηᵣ _)) ∘ M₁ (mult.η _) ∘ M₁ (M₁ (ηₛ _)) ∘ M₁ (ηₛ _) ∘ ηₛ _) ≡⟨ extendr (extendr (extendl (interchange _))) ⟩
      (ηᵣ _ ∘ mult.η _ ∘ ηₛ _ ∘ ηᵣ _) ∘ (M₁ (ηₛ _ ∘ ηᵣ _) ∘ M₁ (mult.η _) ∘ M₁ (M₁ (ηₛ _)) ∘ M₁ (ηₛ _) ∘ ηₛ _)        ≡⟨ ap₂ _∘_ (ηᵣ-mult-outer _) refl ⟩
      (ηᵣ _ ∘ mult.η _) ∘ (M₁ (ηₛ _ ∘ ηᵣ _) ∘ M₁ (mult.η _) ∘ M₁ (M₁ (ηₛ _)) ∘ M₁ (ηₛ _) ∘ ηₛ _)                      ≡⟨ pulll (sym (assoc _ _ _ ) ∙ ηᵣ-mult-inner _) ⟩
      (ηᵣ _ ∘ mult.η _) ∘ (M₁ (mult.η _) ∘ M₁ (M₁ (ηₛ _)) ∘ M₁ (ηₛ _) ∘ ηₛ _)                                         ≡⟨ extendr (extendl mult-assoc) ⟩
      (ηᵣ _ ∘ mult.η _) ∘ (mult.η _ ∘ M₁ (M₁ (ηₛ _)) ∘ M₁ (ηₛ _) ∘ ηₛ _)                                              ≡⟨ (refl⟩∘⟨ extendl (mult.is-natural _ _ _)) ⟩
      (ηᵣ _ ∘ mult.η _) ∘ (M₁ (ηₛ _) ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _)                                                   ≡⟨ pushl (sym (ηᵣ-mult-outer _) ∙ assoc _ _ _) ⟩
      (ηᵣ _ ∘ mult.η _) ∘ (ηₛ _ ∘ ηᵣ _) ∘ (M₁ (ηₛ _) ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _)                                   ≡⟨ (refl⟩∘⟨ extendl (sym (idem-sys _))) ⟩
      (ηᵣ _ ∘ mult.η _) ∘ (ηₛ _ ∘ ηᵣ _) ∘ ((M₁ (ηₛ _) ∘ ηₛ _ ∘ ηᵣ _) ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _)                   ≡⟨ pulll (sym (assoc _ _ _) ∙ ηᵣ-mult-outer _) ⟩
      (ηᵣ _ ∘ mult.η _) ∘ ((M₁ (ηₛ _) ∘ ηₛ _ ∘ ηᵣ _) ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _)                                   ≡⟨ cat! C ⟩
      (ηᵣ _ ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _) ∘ (ηᵣ _ ∘ mult.η _ ∘ M₁ (ηₛ _) ∘ ηₛ _)                                     ∎
      where
        pushη
          : ∀ {a}
          → ηᵣ (S a) ∘ M₁ (ηᵣ a ∘ mult.η a ∘ M₁ (ηₛ a) ∘ ηₛ (S a)) ∘ ηₛ (S (S a))
          ≡ (ηᵣ (S a) ∘ M₁ (ηᵣ a)) ∘ M₁ (mult.η a) ∘ M₁ (M₁ (ηₛ a)) ∘ M₁ (ηₛ (S a)) ∘ ηₛ (S (S a))
        pushη {a = a} = pushr $
          M₁ (ηᵣ a ∘ mult.η a ∘ M₁ (ηₛ a) ∘ ηₛ (S a)) ∘ ηₛ (S (S a))                ≡⟨ pushl (M-∘ _ _) ⟩
          M₁ (ηᵣ a) ∘ M₁ (mult.η a ∘ M₁ (ηₛ a) ∘ ηₛ (S a)) ∘ ηₛ (S (S a))           ≡⟨ (refl⟩∘⟨ pushl (M-∘ _ _)) ⟩
          (M₁ (ηᵣ a) ∘ M₁ (mult.η a) ∘ M₁ (M₁ (ηₛ a) ∘ ηₛ (S a)) ∘ ηₛ (S (S a)))    ≡⟨ (refl⟩∘⟨ (refl⟩∘⟨ pushl (M-∘ _ _))) ⟩
          M₁ (ηᵣ a) ∘ M₁ (mult.η a) ∘ M₁ (M₁ (ηₛ a)) ∘ M₁ (ηₛ (S a)) ∘ ηₛ (S (S a)) ∎
```

## Examples

Clearly, both sorting and deduplicating give rise to split idempotent systems.
Moreover, they are both split monadic.

## Notes

It feels like the interchange law should come from somewhere else?