Lets tuck into some term-indexed types!

Well see what it means to reify definitional equality of terms as a type, and how to use equality to rewrite types. Well reinvent Sigma and Pi types, starting from the simple sums and products we all know and love.

---