\import Paths
\import Set

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

\class AddPointed \extends BaseSet {
  | zro : E

  \protected \func IsZero : \Prop
    => \Pi (x : E) -> x = 
} \where {
    \use \coerce fromPointed (P : Pointed) => \new AddPointed P.E P.ide
    \use \coerce toPointed (P : AddPointed) => \new Pointed P.E P.zro
  }