Spatial descriptions in Type Theory with Records