\import Algebra.Pointed
\import Category
\import Category.Meta
\import Function (Image, isInj, isSurj)
\import Logic
\import Paths
\import Paths.Meta
\import Set.Category

\record PointedHom \extends SetHom {
  \override Dom : Pointed
  \override Cod : Pointed
  | func-ide : func ide = ide
}

\record AddPointedHom \extends SetHom {
  \override Dom : AddPointed
  \override Cod : AddPointed
  | func-zro : func zro = zro
}

\instance PointedCat : Cat Pointed
  | Hom X Y => PointedHom X Y
  | id => id
  | o {X Y Z : Pointed} (g : PointedHom Y Z) (f : PointedHom X Y) => \new PointedHom {
    | func x => g (f x)
    | func-ide => pmap g f.func-ide *> g.func-ide
  }
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip (\lam p1 p2 => ext (func-ide {p1}))
  \where
    \func id (X : Pointed) : PointedHom X X \cowith
      | func x => x
      | func-ide => idp

\instance AddPointedCat : Cat AddPointed
  | Hom X Y => AddPointedHom X Y
  | id => id
  | o {X Y Z : AddPointed} (g : AddPointedHom Y Z) (f : AddPointedHom X Y) => \new AddPointedHom {
    | func x => g (f x)
    | func-zro => pmap g f.func-zro *> g.func-zro
  }
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip (\lam p1 p2 => ext (func-zro {p1}))
  \where
    \func id (X : AddPointed) : AddPointedHom X X \cowith
      | func x => x
      | func-zro => idp

\type Kernel (f : AddPointedHom) => \Sigma (a : f.Dom) (f a = )

\instance KerAddPointed (f : AddPointedHom) : AddPointed (Kernel f)
  | zro => (, func-zro)

\func KerPointedHom (f : AddPointedHom) : AddPointedHom (KerAddPointed f) f.Dom \cowith
  | func => __.
  | func-zro => idp

\lemma kernel-inj {f : AddPointedHom} : isInj (KerPointedHom f)
  => \lam p => ext p

\instance ImageAddPointed (f : AddPointedHom) : AddPointed (Image f)
  | zro => (, inP (, func-zro))

\instance ImageMulPointed (f : PointedHom) : Pointed (Image f)
  | ide => (ide, inP (ide, func-ide))


\func ImagePointedLeftHom (f : AddPointedHom) : AddPointedHom f.Dom (ImageAddPointed f) \cowith
  | func a => (f a, inP (a, idp))
  | func-zro => ext func-zro

\func ImagePointedRightHom (f : AddPointedHom) : AddPointedHom (ImageAddPointed f) f.Cod \cowith
  | func => __.
  | func-zro => idp

\lemma image-surj {f : AddPointedHom} : isSurj (ImagePointedLeftHom f)
  => \lam y => TruncP.map y. \lam s => (s., ext s.)

\lemma image-inj {f : AddPointedHom} : isInj (ImagePointedRightHom f)
  => \lam p => ext p