Thanks! Three comments.

1. Suggested edit: "A value A≲B is definitionally ..." --> "A record value is definitionally ..."

2. I didn't understand the explanation of how eta expansion of records enables the use of records. If one applies the eta expansion to A≲B and then simplifies to A≲B the result is to A≲B, so I fail to see how this helps.

3. I think it's overkill to define ≲-antisym twice. What would you think about removing the first definition and replacing it by the second?

All good suggestions! Implemented.