https://gitlab.com/JasonHuZS/practice/-/tree/master/MLTT contains a mechanization of an NbE proof in Agda of MLTT. Our first task is to port this proof from Agda to Coq. We operate it purely inside of Prop. This means that the proof is only logical; it does not compute automatically. After this, we can then use Equations to construct executable functions.

For a very similar effort, c.f. https://dl.acm.org/doi/10.1145/3167091