1 files changed, 85 insertions, 0 deletions
diff --git a/SplitIdempotents/CMonoids.agda b/SplitIdempotents/CMonoids.agda
new file mode 100644
index 0000000..86111de
--- /dev/null
+++ b/SplitIdempotents/CMonoids.agda
@@ -0,0 +1,85 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; _⊔_; suc)
+
+module SplitIdempotents.CMonoids {c ℓ : Level} where
+
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+import SplitIdempotents.Monoids as SIM
+
+open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-symmetric′)
+
+open import Categories.Category using (Category)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
+open import Categories.Object.Monoid Setoids-×.monoidal using (Monoid)
+open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids)
+open import Data.Product using (_,_)
+open import Data.Setoid using (∣_∣)
+open import Function using (_⟶ₛ_; _⟨$⟩_)
+open import Function.Construct.Setoid using (_∙_)
+open import Morphism.SplitIdempotent CMonoids using (IsSplitIdempotent)
+open import Object.Monoid.Commutative Setoids-×.symmetric using (CommutativeMonoid; CommutativeMonoid⇒)
+open import Relation.Binary using (Setoid)
+
+open Category CMonoids using (_∘_; _≈_)
+open Symmetric Setoids-×.symmetric using (_⊗₀_; unit; _⊗₁_)
+
+module _ {M : CommutativeMonoid} (F : CommutativeMonoid⇒ M M) where
+
+  private
+    module M = CommutativeMonoid M
+    module F = CommutativeMonoid⇒ F
+
+  module MQ = Monoid (SIM.Q F.monoid⇒)
+
+  X : Setoid c ℓ
+  X = MQ.Carrier
+
+  private
+    module X = Setoid X
+    module S = Setoid M.Carrier
+
+  open ≈-Reasoning M.Carrier
+
+  opaque
+    unfolding ×-symmetric′ SIM.μ
+    comm
+        : {x : ∣ MQ.Carrier ⊗₀ MQ.Carrier ∣}
+        → (MQ.μ ⟨$⟩ x)
+        X.≈ (MQ.μ ∙ Setoids-×.braiding.⇒.η (X , X) ⟨$⟩ x)
+    comm {x , y} = begin
+        F.arr ⟨$⟩ (MQ.μ ⟨$⟩ (x , y))          ≈⟨ F.preserves-μ ⟩
+        MQ.μ ⟨$⟩ (F.arr ⟨$⟩ x , F.arr ⟨$⟩ y)  ≈⟨ M.commutative ⟩
+        MQ.μ ⟨$⟩ (F.arr ⟨$⟩ y , F.arr ⟨$⟩ x)  ≈⟨ F.preserves-μ ⟨
+        F.arr ⟨$⟩ (MQ.μ ⟨$⟩ (y , x))          ∎
+
+  Q : CommutativeMonoid
+  Q = record
+      { Carrier = X
+      ; isCommutativeMonoid = record
+          { isMonoid = MQ.isMonoid
+          ; commutative = comm
+          }
+      }
+
+  M⇒Q : CommutativeMonoid⇒ M Q
+  M⇒Q = record
+      { monoid⇒ = SIM.M⇒Q F.monoid⇒
+      }
+
+  Q⇒M : CommutativeMonoid⇒ Q M
+  Q⇒M = record
+      { monoid⇒ = SIM.Q⇒M F.monoid⇒
+      }
+
+  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
+        }