Add the final (non-finalized) fork of CBPV{Term,Type}

This kind-of matches the calculus I sketched on paper, though there are
a few issues left.
CachingEvaluation: switch to M{Type,Term}
CachingEvaluation: add TODO
CachingEvaluation: try addressing TODO

That is, try actually saving the intermediate results. Turns out that
treating types (instead of type codes) as data isn't the best idea.
MType: Fix arity of _v×_
CachingEvalution: do cache intermediate results

As planned, switching to codes allowed me to address the stratification
problem. It also defeats Agda's termination checker: I suspect something
should become coinductive but I'm not sure what.