Fix internalized as a computational description.

The idea is that the core could have computatial descriptions,
which do not mention things like which arguments are implicit,
and Desc can be internalized as a description like the current
primitive (non-computational) description that also mentions
which arguments are implicit. Then you can define the fixpoint
of that description as a computational description, parameterized
by (I : Set) (D : DescI) and indexed by (i : I) (E : Desc I).

It's cool that you can do this but I think it's one step too far
in the direction of making the core type theory simple in exchange
for more complicated derivable programs.

If anything, defining `Desc, making an interpretation function for
it, along with a toDesc function might be okay. But, again I think
defining `Fix is probably not worthwhile.