blob: a9b439603f3e7fd6a74cccc5befdf666172b719e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
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
|
