Type Theory with Records for Natural Language Semantics