Formalization of dependent record types/kinds in MLTT or variant thereof?
I do not know how much of the paper it covers but we do have a module based on it in the standard library:

https://agda.github.io/agda-stdlib/Data.Record.html