Use agda-categories definition of split idempotent

4 files changed, 30 insertions, 59 deletions

diff --git a/Morphism/SplitIdempotent.agda b/Morphism/SplitIdempotent.agda
deleted file mode 100644
index a9b4396..0000000
--- a/Morphism/SplitIdempotent.agda
+++ /dev/null
@@ -1,22 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Level using (Level; _⊔_)
-open import Categories.Category using (Category)
-
-module Morphism.SplitIdempotent {o ℓ e : Level} (𝒞 : Category o ℓ e) where
-
-open Category 𝒞
-
-record IsSplitIdempotent {A : Obj} (i : A ⇒ A) : Set (o ⊔ ℓ ⊔ e) where
-  field
-    B : Obj
-    r : A ⇒ B
-    s : B ⇒ A
-    s∘r : s ∘ r ≈ i
-    r∘s : r ∘ s ≈ id
-
-record SplitIdempotent : Set (o ⊔ ℓ ⊔ e) where
-  field
-    {A} : Obj
-    i : A ⇒ A
-    isSplitIdempotent : IsSplitIdempotent i
diff --git a/SplitIdempotents/CMonoids.agda b/SplitIdempotents/CMonoids.agda
index 86111de..af224df 100644
--- a/SplitIdempotents/CMonoids.agda
+++ b/SplitIdempotents/CMonoids.agda
@@ -14,11 +14,11 @@ 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 Category.KaroubiComplete CMonoids using (KaroubiComplete)
 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)
 
@@ -73,13 +73,13 @@ module _ {M : CommutativeMonoid} (F : CommutativeMonoid⇒ M M) where
       { 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
+Monoids-KaroubiComplete : KaroubiComplete
+Monoids-KaroubiComplete = record
+    { split = λ {A} {f} f∘f≈f → record
+        { obj = Q f
+        ; retract = M⇒Q f
+        ; section = Q⇒M f
+        ; retracts = f∘f≈f
+        ; splits = Setoid.refl (CommutativeMonoid.Carrier A)
         }
+    }
diff --git a/SplitIdempotents/Monoids.agda b/SplitIdempotents/Monoids.agda
index e175b76..0f05552 100644
--- a/SplitIdempotents/Monoids.agda
+++ b/SplitIdempotents/Monoids.agda
@@ -13,12 +13,12 @@ open import Categories.Category.Construction.Monoids Setoids-×.monoidal using (
 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 Category.KaroubiComplete Monoids using (KaroubiComplete)
 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′)
 
@@ -149,13 +149,13 @@ module _ {M : Monoid} (F : Monoid⇒ M M) where
         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
+Monoids-KaroubiComplete : KaroubiComplete
+Monoids-KaroubiComplete = record
+    { split = λ {A} {f} f∘f≈f → record
+        { obj = Q f
+        ; retract = M⇒Q f
+        ; section = Q⇒M f
+        ; retracts = f∘f≈f
+        ; splits = Setoid.refl (Monoid.Carrier A)
         }
+    }
diff --git a/SplitIdempotents/Setoids.agda b/SplitIdempotents/Setoids.agda
index e295cb8..dcc72d6 100644
--- a/SplitIdempotents/Setoids.agda
+++ b/SplitIdempotents/Setoids.agda
@@ -6,13 +6,12 @@ module SplitIdempotents.Setoids {c ℓ : Level} where
 
 open import Categories.Category using (Category)
 open import Categories.Category.Instance.Setoids using (Setoids)
+open import Category.KaroubiComplete (Setoids c ℓ) using (KaroubiComplete)
 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
@@ -43,19 +42,13 @@ module _ {S : Setoid c ℓ} (f : S ⟶ₛ S)  where
       ; 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
+Setoids-KaroubiComplete : KaroubiComplete
+Setoids-KaroubiComplete = record
+    { split = λ {A} {f} idem → record
+        { obj = Q f
+        ; retract = to f
+        ; section = from f
+        ; retracts = idem
+        ; splits = Setoid.refl A
         }
+    }