From b9b9349fcebac862e77ccefb24f3b1c86298c711 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Tue, 24 Mar 2026 16:20:19 -0500
Subject: Add split idempotents

---
 Morphism/SplitIdempotent.agda | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 Morphism/SplitIdempotent.agda

(limited to 'Morphism')

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
-- 
cgit v1.2.3