Add split idempotents

3 files changed, 307 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
+        }
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
+        }
diff --git a/SplitIdempotents/Setoids.agda b/SplitIdempotents/Setoids.agda
new file mode 100644
index 0000000..e295cb8
--- /dev/null
+++ b/SplitIdempotents/Setoids.agda
@@ -0,0 +1,61 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module SplitIdempotents.Setoids {c ℓ : Level} where
+
+open import Categories.Category using (Category)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_; id)
+open import Function.Construct.Identity using () renaming (function to Id)
+open import Function.Construct.Setoid using (_∙_)
+open import Relation.Binary using (Setoid)
+open import Morphism.SplitIdempotent (Setoids c ℓ) using (IsSplitIdempotent)
+
+open Category (Setoids c ℓ) using (_≈_)
+open Func using (cong)
+
+module _ {S : Setoid c ℓ} (f : S ⟶ₛ S)  where
+
+  private
+    module S = Setoid S
+
+  Q : Setoid c ℓ
+  Q = record
+      { Carrier = S.Carrier
+      ; _≈_ = λ a b → f ⟨$⟩ a S.≈ f ⟨$⟩ b
+      ; isEquivalence = record
+          { refl = S.refl
+          ; sym = S.sym
+          ; trans = S.trans
+          }
+      }
+
+  to : S ⟶ₛ Q
+  to = record
+      { to = id
+      ; cong = cong f
+      }
+
+  from : Q ⟶ₛ S
+  from = record
+      { to = f ⟨$⟩_
+      ; cong = id
+      }
+
+  from∘to : from ∙ to ≈ f
+  from∘to = S.refl
+
+  module _ (idem : (f ∙ f) ≈ f) where
+
+    to∘from : to ∙ from ≈ Id Q
+    to∘from = idem
+
+    split : IsSplitIdempotent f
+    split = record
+        { B = Q
+        ; r = to
+        ; s = from
+        ; s∘r = from∘to
+        ; r∘s = to∘from
+        }