Port dependent type theory `TT` to the zoo

[andrejbauer]

I explained in three blog posts (parts one, two, three) how to implement a small dependent type theory. The language tt is suitable for the PL zoo (and in fact, I stole code from the old PL zoo to implement tt). The repo for tt is at https://github.com/andrejbauer/andromeda (branches blog-part-I, blog-part-II and blog-part-III). Probably the part-III version is most suitable for the PL Zoo.