\import Algebra.Pointed
\import Paths
\import Set.SetHom

\record PointedHom \extends SetHom {
  \override Dom : Pointed
  \override Cod : Pointed
  | func-ide : func ide = ide
} \where {
  \func id {X : Pointed} : PointedHom X X \cowith
    | func x => x
    | func-ide => idp

  \func \fixl  compose \alias \infixl  ∘ {X Y Z : Pointed} (g : PointedHom Y Z) (f : PointedHom X Y) : PointedHom X Z \cowith
    | func x => g (f x)
    | func-ide => pmap g f.func-ide *> g.func-ide
}

\record AddPointedHom \extends SetHom {
  \override Dom : AddPointed
  \override Cod : AddPointed
  | func-zro : func zro = zro
} \where {
  \func id (X : AddPointed) : AddPointedHom X X \cowith
    | func x => x
    | func-zro => idp

  \func \fixl  compose \alias \infixl  ∘ {A B C : AddPointed} (g : AddPointedHom B C) (f : AddPointedHom A B) : AddPointedHom A C \cowith
    | func x => g (f x)
    | func-zro => pmap g f.func-zro *> g.func-zro
}