The description is missing semantics, and the skeleton code only very briefly implicitly describes some semantics. Semantics for some functions can be extracted from the sample tests. This is however assuming too much on the part of the reader. Please add at least some semantic comments to functions plus, pred, and mult.

Should add test case for pred, its much harder than succ/mult. Heres the one I used:

it "pred (x+1) = x" $ do 
        property $ \(NonNegative x) ->
          let x' = fromPeano (from $ x+1) :: D
          in showPeano (toPeano (pred `app` x')) == x

What is abs in the description? A typo for lam ? Or am I really missing something?