blob: e4005d1d100156df8e73e2ef4397b760cfdcc42e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
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
|
