From 11e8c93b5426ddfd75f1c9c495e4da0defbc08a6 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 25 Mar 2026 08:53:18 -0500
Subject: Add looped wiring diagrams and merge functor

---
 Category/KaroubiComplete.agda | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 Category/KaroubiComplete.agda

(limited to 'Category')

diff --git a/Category/KaroubiComplete.agda b/Category/KaroubiComplete.agda
new file mode 100644
index 0000000..e4005d1
--- /dev/null
+++ b/Category/KaroubiComplete.agda
@@ -0,0 +1,16 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Level using (Level; suc; _⊔_)
+
+module Category.KaroubiComplete {o ℓ e : Level} (𝒞 : Category o ℓ e) where
+
+open import Categories.Morphism.Idempotent 𝒞 using (IsSplitIdempotent)
+
+open Category 𝒞
+
+-- A Karoubi complete category is one in which all idempotents split
+record KaroubiComplete : Set (suc (o ⊔ ℓ ⊔ e)) where
+
+  field
+    split : {A : Obj} {f : A ⇒ A} → f ∘ f ≈ f → IsSplitIdempotent f
-- 
cgit v1.2.3