Added some library stuff.
Added the interval, circle, (untruncated) quotient, suspension and sphere (almost) as examples of HITs.
Worked out a translation of the Ackermann function and proved it to be (extensionally) equal to the pattern matching definition.
Tried out some stuff with the inconsistencies of pattern matching, as mentioned on the Agda mailing list (https://lists.chalmers.se/pipermail/agda/2014/006271.html and other posts).