Last active
March 15, 2024 20:34
-
-
Save TOTBWF/25190ae6705b0381740dd16ad75ea956 to your computer and use it in GitHub Desktop.
Revisions
-
TOTBWF revised this gist
Mar 14, 2024 . 1 changed file with 2 additions and 2 deletions.There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -109,8 +109,8 @@ on $C$, which we call the *idempotent restriction* of $F$. 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 * $e_{A} \circ \mu_{A} \circ M(e_{A}) = e_{A} \circ \mu_A$, and * $e_{A} \circ \mu_{A} \circ e_{M(A)} = e_{A} \circ \mu_A$ ```agda module _ -
Mar 14, 2024 . No changes.There are no files selected for viewing
-
Mar 14, 2024 . 1 changed file with 1 addition and 1 deletion.There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -162,7 +162,7 @@ with the following interchange law for every section/rectraction pair $(s_{a}, r ``` If $e$ is split monadic, then the idempotent restriction of $M$ along $e$ inherits the monadic structure of $M$. The proof of this is quite brutal though! ```agda module _ -
Mar 14, 2024 . 1 changed file with 1 addition and 1 deletion.There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -133,7 +133,7 @@ module _ 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 -
Mar 14, 2024 . 1 changed file with 1 addition and 1 deletion.There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -110,7 +110,7 @@ on $C$, which we call the *idempotent restriction* of $F$. 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} \circ e_{M(A)} = e_{A} \circ \mu_A$ ```agda module _ -
Mar 14, 2024 . 1 changed file with 1 addition and 2 deletions.There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -1,5 +1,4 @@ --- description: | Idempotent systems. --- -
Mar 14, 2024 .There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -0,0 +1,245 @@ -- - 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?