From 348f5615631fff3279049ab930fd51ec4442f44f Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 25 Mar 2026 14:08:17 -0500 Subject: Use agda-categories definition of split idempotent --- Morphism/SplitIdempotent.agda | 22 ---------------------- 1 file changed, 22 deletions(-) delete mode 100644 Morphism/SplitIdempotent.agda (limited to 'Morphism/SplitIdempotent.agda') diff --git a/Morphism/SplitIdempotent.agda b/Morphism/SplitIdempotent.agda deleted file mode 100644 index a9b4396..0000000 --- a/Morphism/SplitIdempotent.agda +++ /dev/null @@ -1,22 +0,0 @@ -{-# 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