Add looped wiring diagrams and merge functor

1 files changed, 16 insertions, 0 deletions

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