@misc{indiciae3874d8883006,
  title = {Normalisation by Evaluation for Type Theory, in Type Theory},
  author = {Thorsten Altenkirch and Ambrus Kaposi},
  year = {2017},
  doi = {10.23638/lmcs-13(4:1)2017},
  url = {https://arxiv.org/abs/1612.02462},
  note = {Source identifier: 1612.02462}
}