3 files changed, 30 insertions, 37 deletions
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
         }
+    }