Michael Hedberg. A coherence theorem for Martin-Löf's type theory. Journal of Functional Programming, 8(4):413--436, 1998-07. https://doi.org/10.1017/S0956796898003153