Based on the excellent blog post from William Bowman: Normalization by Evaluation Four Ways: Reconstructing NbE Designs from First Principles. I extend the syntax with natural numbers and their recursor to make things more interesting.
It turns out that only Choice12.agda and Choice2.agda satisfy Agda's positivity and termination checks, so I'd recommend starting with those.