From bf7177add78c682673b59d422135e52e4daf2f0d Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Fri, 12 Dec 2025 08:07:42 +0100 Subject: [PATCH 1/3] Add Action monad --- src/Categories/Monad/Construction/Action.agda | 95 +++++++++++++++++++ 1 file changed, 95 insertions(+) create mode 100644 src/Categories/Monad/Construction/Action.agda diff --git a/src/Categories/Monad/Construction/Action.agda b/src/Categories/Monad/Construction/Action.agda new file mode 100644 index 000000000..c8f8e3547 --- /dev/null +++ b/src/Categories/Monad/Construction/Action.agda @@ -0,0 +1,95 @@ +-- The monad of actions of a monoid in a monoidal category +-- See https://ncatlab.org/nlab/show/action+monad + +-- With the Cartesian monoidal structure on Sets or Setoids, this gives us the +-- Writer monad familiar from Haskell. With the Cocartesian monoidal structure, +-- noting that all objects in that monoidal category are monoids in a unique +-- way, this gives us the Either monad. + +{-# OPTIONS --safe --without-K #-} + +open import Categories.Category +open import Categories.Category.Monoidal + +module Categories.Monad.Construction.Action {o ℓ e} {C : Category o ℓ e} (CM : Monoidal C) where + +open import Categories.Category.Monoidal.Properties CM using (coherence-inv₁) +open import Categories.Category.Monoidal.Reasoning CM +open import Categories.Category.Monoidal.Utilities CM using (module Shorthands; pentagon-inv; triangle-inv) +open import Categories.Monad using (Monad) +open import Categories.Morphism.Reasoning C +open import Categories.NaturalTransformation using (ntHelper) +open import Categories.Functor using (Endofunctor; Functor) +open import Categories.Functor.Bifunctor.Properties using ([_]-commute) +open import Categories.Functor.Properties using ([_]-resp-∘; [_]-resp-square; [_]-resp-inverse) +open import Categories.Object.Monoid CM using (Monoid) +open import Function.Base using (_$_) + +open Category C +open Monoidal CM +open Shorthands + +module _ (m : Monoid) where + + private + module m = Monoid m + + ActionF : Endofunctor C + ActionF = m.Carrier ⊗- + + private + module A = Functor ActionF + + η : ∀ X → X ⇒ A.₀ X + η X = m.η ⊗₁ id ∘ unitorˡ.to + + η-commute : ∀ {X Y} (f : X ⇒ Y) → η Y ∘ f ≈ A.₁ f ∘ η X + η-commute f = glue (Equiv.sym [ ⊗ ]-commute) unitorˡ-commute-to + + μ : ∀ X → A.₀ (A.₀ X) ⇒ A.₀ X + μ X = m.μ ⊗₁ id ∘ associator.to + + μ-commute : ∀ {X Y} (f : X ⇒ Y) → μ Y ∘ A.₁ (A.₁ f) ≈ A.₁ f ∘ μ X + μ-commute f = glue (Equiv.sym [ ⊗ ]-commute) (assoc-commute-to ○ ∘-resp-≈ˡ (⊗-resp-≈ˡ ⊗.identity)) + + μ-assoc : ∀ {X} → μ X ∘ A.₁ (μ X) ≈ μ X ∘ μ (A.₀ X) + μ-assoc = begin + (m.μ ⊗₁ id ∘ α⇐) ∘ id ⊗₁ (m.μ ⊗₁ id ∘ α⇐) ≈⟨ refl⟩∘⟨ Functor.homomorphism (_ ⊗-) ⟩ + (m.μ ⊗₁ id ∘ α⇐) ∘ (id ⊗₁ (m.μ ⊗₁ id) ∘ id ⊗₁ α⇐) ≈⟨ extend² assoc-commute-to ⟩ + (m.μ ⊗₁ id ∘ (id ⊗₁ m.μ) ⊗₁ id) ∘ (α⇐ ∘ id ⊗₁ α⇐) ≈⟨ [ -⊗ _ ]-resp-square (switch-fromtoʳ associator (assoc ○ Equiv.sym m.assoc)) ⟩∘⟨refl ⟩ + ((m.μ ∘ m.μ ⊗₁ id) ⊗₁ id ∘ α⇐ ⊗₁ id) ∘ (α⇐ ∘ id ⊗₁ α⇐) ≈⟨ pullʳ (sym-assoc ○ pentagon-inv) ⟩ + (m.μ ∘ m.μ ⊗₁ id) ⊗₁ id ∘ (α⇐ ∘ α⇐) ≈⟨ Functor.homomorphism (-⊗ _) ⟩∘⟨refl ⟩ + (m.μ ⊗₁ id ∘ (m.μ ⊗₁ id) ⊗₁ id) ∘ (α⇐ ∘ α⇐) ≈⟨ extend² (Equiv.sym assoc-commute-to ○ ∘-resp-≈ʳ (⊗-resp-≈ʳ ⊗.identity)) ⟩ + (m.μ ⊗₁ id ∘ α⇐) ∘ (m.μ ⊗₁ id ∘ α⇐) ∎ + + μ-identityˡ : ∀ {X} → μ X ∘ A.₁ (η X) ≈ id + μ-identityˡ = begin + (m.μ ⊗₁ id ∘ α⇐) ∘ id ⊗₁ (m.η ⊗₁ id ∘ λ⇐) ≈⟨ refl⟩∘⟨ Functor.homomorphism (_ ⊗-) ⟩ + (m.μ ⊗₁ id ∘ α⇐) ∘ (id ⊗₁ (m.η ⊗₁ id) ∘ id ⊗₁ λ⇐) ≈⟨ extend² assoc-commute-to ⟩ + (m.μ ⊗₁ id ∘ (id ⊗₁ m.η) ⊗₁ id) ∘ (α⇐ ∘ id ⊗₁ λ⇐) ≈⟨ [ -⊗ _ ]-resp-∘ (Equiv.sym m.identityʳ) ⟩∘⟨ triangle-inv ⟩ + ρ⇒ ⊗₁ id ∘ ρ⇐ ⊗₁ id ≈⟨ [ -⊗ _ ]-resp-inverse unitorʳ.isoʳ ⟩ + id ∎ + + μ-identityʳ : ∀ {X} → μ X ∘ η (A.₀ X) ≈ id + μ-identityʳ = begin + (m.μ ⊗₁ id ∘ α⇐) ∘ (m.η ⊗₁ id ∘ λ⇐) ≈⟨ extend² (∘-resp-≈ʳ (⊗-resp-≈ʳ (Equiv.sym ⊗.identity)) ○ assoc-commute-to) ⟩ + (m.μ ⊗₁ id ∘ (m.η ⊗₁ id) ⊗₁ id) ∘ (α⇐ ∘ λ⇐) ≈⟨ [ -⊗ _ ]-resp-∘ (Equiv.sym m.identityˡ) ⟩∘⟨ coherence-inv₁ ⟩ + λ⇒ ⊗₁ id ∘ λ⇐ ⊗₁ id ≈⟨ [ -⊗ _ ]-resp-inverse unitorˡ.isoʳ ⟩ + id ∎ + + ActionM : Monad C + ActionM = record + { F = ActionF + ; η = ntHelper record + { η = η + ; commute = η-commute + } + ; μ = ntHelper record + { η = μ + ; commute = μ-commute + } + ; assoc = μ-assoc + ; sym-assoc = Equiv.sym μ-assoc + ; identityˡ = μ-identityˡ + ; identityʳ = μ-identityʳ + } From 1631f5faca0fbc4bbc3bdf8fee0da2b23194272d Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Fri, 12 Dec 2025 08:29:32 +0100 Subject: [PATCH 2/3] Add morphism transformation --- src/Categories/Monad/Construction/Action.agda | 24 +++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/src/Categories/Monad/Construction/Action.agda b/src/Categories/Monad/Construction/Action.agda index c8f8e3547..b4ceb02a7 100644 --- a/src/Categories/Monad/Construction/Action.agda +++ b/src/Categories/Monad/Construction/Action.agda @@ -17,12 +17,13 @@ open import Categories.Category.Monoidal.Properties CM using (coherence-inv₁) open import Categories.Category.Monoidal.Reasoning CM open import Categories.Category.Monoidal.Utilities CM using (module Shorthands; pentagon-inv; triangle-inv) open import Categories.Monad using (Monad) +open import Categories.Monad.Morphism using (Monad⇒-id) open import Categories.Morphism.Reasoning C open import Categories.NaturalTransformation using (ntHelper) open import Categories.Functor using (Endofunctor; Functor) -open import Categories.Functor.Bifunctor.Properties using ([_]-commute) +open import Categories.Functor.Bifunctor.Properties using ([_]-commute; [_]-decompose₁) open import Categories.Functor.Properties using ([_]-resp-∘; [_]-resp-square; [_]-resp-inverse) -open import Categories.Object.Monoid CM using (Monoid) +open import Categories.Object.Monoid CM using (Monoid; Monoid⇒) open import Function.Base using (_$_) open Category C @@ -93,3 +94,22 @@ module _ (m : Monoid) where ; identityˡ = μ-identityˡ ; identityʳ = μ-identityʳ } + +-- a monoid morphism induces a monad morphism +Monoid⇒-Monad⇒ : ∀ {m n} → Monoid⇒ m n → Monad⇒-id (ActionM n) (ActionM m) +Monoid⇒-Monad⇒ {m} {n} f = record + { α = ntHelper record + { η = λ X → arr ⊗₁ id + ; commute = λ f → Equiv.sym [ ⊗ ]-commute + } + ; unit-comp = pullˡ ([ -⊗ _ ]-resp-∘ preserves-η) + ; mult-comp = begin + arr ⊗₁ id ∘ m.μ ⊗₁ id ∘ α⇐ ≈⟨ extendʳ ([ -⊗ _ ]-resp-square preserves-μ) ⟩ + n.μ ⊗₁ id ∘ (arr ⊗₁ arr) ⊗₁ id ∘ α⇐ ≈⟨ pullʳ assoc-commute-to ⟨ + (n.μ ⊗₁ id ∘ α⇐) ∘ arr ⊗₁ (arr ⊗₁ id) ≈⟨ refl⟩∘⟨ [ ⊗ ]-decompose₁ ⟩ + (n.μ ⊗₁ id ∘ α⇐) ∘ arr ⊗₁ id ∘ id ⊗₁ (arr ⊗₁ id) ∎ + } + where + module m = Monoid m + module n = Monoid n + open Monoid⇒ f From d01c3003a46422ab191f56be4e6560c4bbcf900d Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 17 Dec 2025 07:27:30 +0100 Subject: [PATCH 3/3] Review comments --- src/Categories/Monad/Construction/Action.agda | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Categories/Monad/Construction/Action.agda b/src/Categories/Monad/Construction/Action.agda index b4ceb02a7..d3c3066a2 100644 --- a/src/Categories/Monad/Construction/Action.agda +++ b/src/Categories/Monad/Construction/Action.agda @@ -8,8 +8,8 @@ {-# OPTIONS --safe --without-K #-} -open import Categories.Category -open import Categories.Category.Monoidal +open import Categories.Category.Core using (Category) +open import Categories.Category.Monoidal.Core using (Monoidal) module Categories.Monad.Construction.Action {o ℓ e} {C : Category o ℓ e} (CM : Monoidal C) where @@ -42,13 +42,13 @@ module _ (m : Monoid) where module A = Functor ActionF η : ∀ X → X ⇒ A.₀ X - η X = m.η ⊗₁ id ∘ unitorˡ.to + η _ = m.η ⊗₁ id ∘ λ⇐ η-commute : ∀ {X Y} (f : X ⇒ Y) → η Y ∘ f ≈ A.₁ f ∘ η X η-commute f = glue (Equiv.sym [ ⊗ ]-commute) unitorˡ-commute-to μ : ∀ X → A.₀ (A.₀ X) ⇒ A.₀ X - μ X = m.μ ⊗₁ id ∘ associator.to + μ _ = m.μ ⊗₁ id ∘ α⇐ μ-commute : ∀ {X Y} (f : X ⇒ Y) → μ Y ∘ A.₁ (A.₁ f) ≈ A.₁ f ∘ μ X μ-commute f = glue (Equiv.sym [ ⊗ ]-commute) (assoc-commute-to ○ ∘-resp-≈ˡ (⊗-resp-≈ˡ ⊗.identity)) @@ -99,8 +99,8 @@ module _ (m : Monoid) where Monoid⇒-Monad⇒ : ∀ {m n} → Monoid⇒ m n → Monad⇒-id (ActionM n) (ActionM m) Monoid⇒-Monad⇒ {m} {n} f = record { α = ntHelper record - { η = λ X → arr ⊗₁ id - ; commute = λ f → Equiv.sym [ ⊗ ]-commute + { η = λ _ → arr ⊗₁ id + ; commute = λ _ → Equiv.sym [ ⊗ ]-commute } ; unit-comp = pullˡ ([ -⊗ _ ]-resp-∘ preserves-η) ; mult-comp = begin