\import Paths
\import Set

\class Pointed \extends BaseSet
  | ide : E
  \where {
    \func equals {X Y : Pointed} (p : X = {\Set} Y) (q : coe (p @) ide right = ide) : X = Y
      => path (\lam i => \new Pointed (p @ i) (pathOver {p @} q @ i))
  }

\class AddPointed \extends BaseSet
  | zro : E
  \where {
    \use \coerce fromPointed (P : Pointed) => \new AddPointed P.E P.ide
    \use \coerce toPointed (P : AddPointed) => \new Pointed P.E P.zro
  }