{-# OPTIONS --without-K --safe #-}
open import Categories.Category
open import Categories.Object.Zero
module Categories.Object.Cokernel {o ℓ e} {𝒞 : Category o ℓ e} (𝟎 : Zero 𝒞) where
open import Level
open import Categories.Morphism 𝒞
open import Categories.Morphism.Reasoning 𝒞
hiding (glue)
open Category 𝒞
open Zero 𝟎
open HomReasoning
private
variable
A B X : Obj
f h i j k : A ⇒ B
record IsCokernel {A B K} (f : A ⇒ B) (k : B ⇒ K) : Set (o ⊔ ℓ ⊔ e) where
field
commute : k ∘ f ≈ zero⇒
universal : ∀ {X} {h : B ⇒ X} → h ∘ f ≈ zero⇒ → K ⇒ X
factors : ∀ {eq : h ∘ f ≈ zero⇒} → h ≈ universal eq ∘ k
unique : ∀ {eq : h ∘ f ≈ zero⇒} → h ≈ i ∘ k → i ≈ universal eq
universal-resp-≈ : ∀ {eq : h ∘ f ≈ zero⇒} {eq′ : i ∘ f ≈ zero⇒} →
h ≈ i → universal eq ≈ universal eq′
universal-resp-≈ h≈i = unique (⟺ h≈i ○ factors)
universal-∘ : h ∘ k ∘ f ≈ zero⇒
universal-∘ {h = h} = begin
h ∘ k ∘ f ≈⟨ refl⟩∘⟨ commute ⟩
h ∘ zero⇒ ≈⟨ zero-∘ˡ h ⟩
zero⇒ ∎
record Cokernel {A B} (f : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where
field
{cokernel} : Obj
cokernel⇒ : B ⇒ cokernel
isCokernel : IsCokernel f cokernel⇒
open IsCokernel isCokernel public
IsCokernel⇒Cokernel : IsCokernel f k → Cokernel f
IsCokernel⇒Cokernel {k = k} isCokernel = record
{ cokernel⇒ = k
; isCokernel = isCokernel
}