Added elimination principle for (-1)-truncation and "showed" that (-1)-truncation is a monad.