Add split idempotents

1 files changed, 22 insertions, 0 deletions

diff --git a/Morphism/SplitIdempotent.agda b/Morphism/SplitIdempotent.agda
new file mode 100644
index 0000000..a9b4396
--- /dev/null
+++ b/Morphism/SplitIdempotent.agda
@@ -0,0 +1,22 @@
+{-# 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