This should presumably read “from values to terms”. I suspect your target audience won’t be confused by this, but it took me a minute or two to figure it out.

To typecheck a term, it must be beta-normal. Environment-body pairs cannot be typechecked without substituting them out (hereditarily).
To match on a term, it must be beta-delta-normal and of positive type. (Positive types are Set, Prop, enumerations, datatypes. Not Pi, Sig, proofs, codatatypes.)
To update a term, we care only that it is represented in a first-order way.
To construct a term, e.g. when implementing an operator, we like some sort of lambda (Haskell or de Bruijn), not environment-body pairs.
To go from functional binding or environment-body pairs to a first-order lambda requires a name supply.
To typecheck requires a name supply and bidirectional type information.
To eta-expand requires a name supply and bidirectional type information.
To beta-normalize or beta-delta-normalize requires only a name supply.
Whatever ‘values’ operators consume must be easily embedded anywhere in whatever they produce, without a name supply.

These constraints admit a variety of solutions. Are there more constraints?