\import Algebra.Pointed
\import Algebra.Pointed.PointedHom
\import Category
\import Category.Meta
\import Function (Image, IsInj, IsSurj)
\import Logic
\import Paths
\import Paths.Meta

\instance PointedCat : Cat Pointed
  | Hom X Y => PointedHom X Y
  | id _ => PointedHom.id
  | o => PointedHom.∘
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip (\lam p1 p2 => ext (func-ide {p1}))

\instance AddPointedCat : Cat AddPointed
  | Hom X Y => AddPointedHom X Y
  | id => AddPointedHom.id
  | o => AddPointedHom.∘
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip (\lam p1 p2 => ext (func-zro {p1}))

\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 ImagePointed (f : PointedHom) : Pointed (Image f)
  | ide => (ide, inP (ide, func-ide))


\func ImagePointedLeftHom (f : PointedHom)  : PointedHom f.Dom (ImagePointed f) \cowith
  | func a => (f a, inP (a, idp))
  | func-ide => ext func-ide

\func ImagePointedRightHom(f : PointedHom) : PointedHom (ImagePointed f) f.Cod \cowith
  | func => __.
  | func-ide => idp



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

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

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

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