data N  = Z | S (n :: N)

(+) (n,m:: N)
    :: N
    = case m of {
        (Z) -> n;
        (S m') -> S (n + m');}

-- False in Agda:
data False =

-- True in Agda:
data True = true


-- Equality on N
(==) (n,m::N)
     :: Set
      = case n of
            { (Z)       -> case m of
                                { (Z)     -> True;
                                  (S m')  -> False;};
              (S n')    -> case m of
                                { (Z)     -> False;
                                  (S m')  -> n' == m';};}


one :: N
   = S Z

trans (n::N)(m::N)(k::N)(p::(==) n m)(q::(==) m k) :: (==) n k
  = case n of {
      (Z) ->
        case m of {
          (Z) ->
            case k of {
              (Z) -> true;
              (S k') -> q;};
          (S m') -> case p of { };};
      (S n') ->
        case m of {
          (Z) -> case p of { };
          (S m') ->
            case k of {
              (Z) -> q;
              (S k') -> trans n' m' k' p q;};};}