open import Cat.Diagram.Equaliser.Kernel
open import Cat.Instances.Shape.Terminal
open import Cat.Functor.FullSubcategory
open import Cat.Diagram.Initial
open import Cat.Instances.Comma
open import Cat.Instances.Slice
open import Cat.Abelian.Base
open import Cat.Prelude

open /-Obj
open /-Hom
open ↓Obj
open ↓Hom

module wip.image {o ℓ} {C : Precategory o ℓ} (A : is-abelian C) where
  open is-abelian A

  -- images : ∀ {A B} (f : Hom A B) → Image f
  -- images f = im where
    -- obj : ↓Obj (const! (cut f)) Forget-full-subcat
    -- obj .x = tt  images : ∀ {A B} (f : Hom A B) → Image f
  -- images f = im where
    -- obj .y .object = cut (Ker.kernel (Coker.coeq f))
    -- obj .y .witness {c} = kernels-are-subobjects C ∅ _ (Ker.has-is-kernel _)
    -- -- obj .map ./-Hom.map = decompose f .fst ∘ Coker.coeq _
    -- -- obj .map ./-Hom.commutes = pulll (Ker.universal _) ∙ Coker.universal _