[Agda] Formalization of a system dependently-typed records in Agda?

[Jacques Carette]

As the subject says: are you aware of a formalization of a system of 
dependently-typed records in Agda?  A module system would also be fine.

The most important requirement: it must be based on *names* for fields. 
No de Bruijn levels / indices / what-have-you.  I understand the 
meta-theory of Sigma types just fine, thanks. The part I am really 
interested in are the subtleties involved when alpha-renaming is not 
only not-free, it is meaningful. Records / modules with differently 
named fields are different as far as humans are concerned, and this is 
an important usability requirements that ought to be modeled too.

I have attempted to do this myself.  Adding a free-for predicate to 
telescopes is not hard. What is hard is the exact specification of how 
it should be preserved under renaming and substitution.

Jacques

PS: responses along the lines of "oh, you should use theory X" are 
unlikely to be helpful.  I have pursued the rabbit hole of many 
different X already, and they all hit some substantial brick walls when 
came the time to truly be formal about it all.  Thus the important 'in 
Agda' qualifier.