Add split idempotents

1 files changed, 161 insertions, 0 deletions

diff --git a/SplitIdempotents/Monoids.agda b/SplitIdempotents/Monoids.agda
new file mode 100644
index 0000000..e175b76
--- /dev/null
+++ b/SplitIdempotents/Monoids.agda
@@ -0,0 +1,161 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; _⊔_; suc)
+
+module SplitIdempotents.Monoids {c ℓ : Level} where
+
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-monoidal′)
+
+open import Categories.Category using (Category)
+open import Categories.Category.Construction.Monoids Setoids-×.monoidal using (Monoids)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Object.Monoid Setoids-×.monoidal using (Monoid; Monoid⇒)
+open import Data.Product using (_,_)
+open import Data.Setoid using (∣_∣)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_; id)
+open import Function.Construct.Identity using () renaming (function to Id)
+open import Function.Construct.Setoid using (_∙_)
+open import Morphism.SplitIdempotent Monoids using (IsSplitIdempotent)
+open import Relation.Binary using (Setoid)
+open import SplitIdempotents.Setoids using () renaming (Q to Q′)
+
+open Category Monoids using (_∘_; _≈_) renaming (id to Id⇒)
+open Func
+open Monoidal Setoids-×.monoidal using (_⊗₀_; unit; _⊗₁_)
+
+module _ {M : Monoid} (F : Monoid⇒ M M) where
+
+  private
+    module M = Monoid M
+    module F = Monoid⇒ F
+
+  X′ : Setoid c ℓ
+  X′ = Q′ F.arr
+
+  private
+    module S = Setoid M.Carrier
+    module X′ = Setoid X′
+
+  open ≈-Reasoning M.Carrier
+
+  opaque
+    unfolding ×-monoidal′
+    μ : X′ ⊗₀ X′ ⟶ₛ X′
+    μ = record
+        { to = λ (x , y) → M.μ ⟨$⟩ (x , y)
+        ; cong = λ { {A , B} {C , D} (FA≈FB , FC≈FD) → begin
+            F.arr ⟨$⟩ (M.μ ⟨$⟩ (A , B))         ≈⟨ F.preserves-μ ⟩
+            M.μ ⟨$⟩ (F.arr ⟨$⟩ A , F.arr ⟨$⟩ B) ≈⟨ cong M.μ (FA≈FB , FC≈FD) ⟩
+            M.μ ⟨$⟩ (F.arr ⟨$⟩ C , F.arr ⟨$⟩ D) ≈⟨ F.preserves-μ ⟨
+            F.arr ⟨$⟩ (M.μ ⟨$⟩ (C , D))         ∎
+          }
+        }
+
+  η : unit ⟶ₛ X′
+  η = record
+      { to = to M.η
+      ; cong = λ { {A} {B} eq → begin
+          F.arr ⟨$⟩ (M.η ⟨$⟩ A) ≈⟨ F.preserves-η ⟩
+          M.η ⟨$⟩ A             ≈⟨ cong M.η eq ⟩
+          M.η ⟨$⟩ B             ≈⟨ F.preserves-η ⟨
+          F.arr ⟨$⟩ (M.η ⟨$⟩ B) ∎
+        }
+      }
+
+  opaque
+    unfolding μ
+    assoc
+        : {x : ∣ (X′ ⊗₀ X′) ⊗₀ X′ ∣}
+        → μ ∙ μ ⊗₁ Setoids-×.id ⟨$⟩ x
+        X′.≈ (μ ∙ Id X′ ⊗₁ μ ∙ Setoids-×.associator.from ⟨$⟩ x)
+    assoc {(x , y) , z} = begin
+        F.arr ⟨$⟩ (μ ⟨$⟩ (μ ⟨$⟩ (x , y) , z))                   ≈⟨ F.preserves-μ ⟩
+        μ ⟨$⟩ (F.arr ⟨$⟩ (μ ⟨$⟩ (x , y)) , F.arr ⟨$⟩ z)         ≈⟨ cong M.μ (F.preserves-μ , X′.refl) ⟩
+        μ ⟨$⟩ (μ ⟨$⟩ (F.arr ⟨$⟩ x , F.arr ⟨$⟩ y) , F.arr ⟨$⟩ z) ≈⟨ M.assoc ⟩
+        μ ⟨$⟩ (F.arr ⟨$⟩ x , μ ⟨$⟩ (F.arr ⟨$⟩ y , F.arr ⟨$⟩ z)) ≈⟨ cong M.μ (X′.refl , F.preserves-μ) ⟨
+        μ ⟨$⟩ (F.arr ⟨$⟩ x , F.arr ⟨$⟩ (μ ⟨$⟩ (y , z)))         ≈⟨ F.preserves-μ ⟨
+        F.arr ⟨$⟩ (μ ⟨$⟩ (x , μ ⟨$⟩ (y , z)))                   ∎
+
+  opaque
+    unfolding μ
+    identityˡ
+        : {x : ∣ unit ⊗₀ X′ ∣}
+        → (Setoids-×.unitorˡ.from ⟨$⟩ x)
+        X′.≈ (μ ∙ η ⊗₁ Id X′ ⟨$⟩ x)
+    identityˡ {_ , x} = begin
+        F.arr ⟨$⟩ x                               ≈⟨ M.identityˡ ⟩
+        μ ⟨$⟩ (η ⟨$⟩ _ , F.arr ⟨$⟩ x)             ≈⟨ cong M.μ (F.preserves-η , X′.refl) ⟨
+        μ ⟨$⟩ (F.arr ⟨$⟩ (η ⟨$⟩ _) , F.arr ⟨$⟩ x) ≈⟨ F.preserves-μ ⟨
+        F.arr ⟨$⟩ (μ ⟨$⟩ (η ⟨$⟩ _ , x))           ∎
+
+  opaque
+    unfolding μ
+    identityʳ
+        : {x : ∣ X′ ⊗₀ unit ∣}
+        → (Setoids-×.unitorʳ.from ⟨$⟩ x)
+        X′.≈ (μ ∙ Id _ ⊗₁ η ⟨$⟩ x)
+    identityʳ {x , _} = begin
+        F.arr ⟨$⟩ x                               ≈⟨ M.identityʳ ⟩
+        μ ⟨$⟩ (F.arr ⟨$⟩ x , η ⟨$⟩ _)             ≈⟨ cong M.μ (X′.refl , F.preserves-η) ⟨
+        μ ⟨$⟩ (F.arr ⟨$⟩ x , F.arr ⟨$⟩ (η ⟨$⟩ _)) ≈⟨ F.preserves-μ ⟨
+        F.arr ⟨$⟩ (μ ⟨$⟩ (x , to M.η _))          ∎
+
+  Q : Monoid
+  Q = record
+      { Carrier = X′
+      ; isMonoid = record
+          { μ = μ
+          ; η = η
+          ; assoc = assoc
+          ; identityˡ = identityˡ
+          ; identityʳ = identityʳ
+          }
+      }
+
+  M⇒Q : Monoid⇒ M Q
+  M⇒Q = record
+      { arr = arr
+      ; preserves-μ = preserves-μ
+      ; preserves-η = S.refl
+      }
+    where
+      arr : M.Carrier ⟶ₛ X′
+      arr = record
+          { to = id
+          ; cong = cong F.arr
+          }
+      opaque
+        unfolding μ
+        preserves-μ : {x : ∣ M.Carrier ⊗₀ M.Carrier ∣} → (arr ∙ M.μ ⟨$⟩ x) X′.≈ (μ ∙ arr ⊗₁ arr ⟨$⟩ x)
+        preserves-μ = S.refl
+
+  Q⇒M : Monoid⇒ Q M
+  Q⇒M = record
+      { arr = arr
+      ; preserves-μ = preserves-μ
+      ; preserves-η = F.preserves-η
+      }
+    where
+      arr : X′ ⟶ₛ M.Carrier
+      arr = record
+          { to = to F.arr
+          ; cong = id
+          }
+      opaque
+        unfolding μ
+        preserves-μ : {x : ∣ X′ ⊗₀ X′ ∣} → arr ∙ μ ⟨$⟩ x S.≈ M.μ ∙ arr ⊗₁ arr ⟨$⟩ x
+        preserves-μ = F.preserves-μ
+
+  module _ (idem : F ∘ F ≈ F) where
+
+    split : IsSplitIdempotent F
+    split = record
+        { B = Q
+        ; r = M⇒Q
+        ; s = Q⇒M
+        ; s∘r = S.refl
+        ; r∘s = idem
+        }