RawMon type checking fails in Properties.agda

When type checking [Properties.agda](https://github.com/crypto-agda/explore/blob/master/lib/Explore/Properties.agda#L51), I get the following error message (with Agda 2.4.2):

```
.../explore.git/lib/Explore/Properties.agda:51,47-48
(Set c) !=< (_A_91 → _A_91 → Set _ℓ_90) of type (Set (ₛ c))
when checking that the expression C has type Rel _A_91 _ℓ_90
```
