Realising level polymorphic subsets within records

Question

Using the notion of subsets as predicates,

ℙ : ∀ {b a} → Set a → Set (a ⊔ suc b)
ℙ {b} {a} X = X → Set b

I'd like to consider structures endowed with a predicate on subsets,

record SetWithAPredicate {a c} : Set {!!} where
  field
   S : Set a
   P : ∀ {b} → ℙ {b} S → Set c

This is an ill-formed construction due to the level quantification used in ℙ. Everything works fine when I use S, P as parameters to a module, but I'd like them to be records so that I can form constructions on them and give instances of them.

I've tried a few other things, such as moving the level b of ℙ inside the definition via an existential but then that led to metavaraible trouble. I also tried changing the type of P,

P : ℙ {a} S → Set c

but then I can no longer ask for, say, the empty set to have the property:

P-⊥ : P(λ _ → ⊥)

This is not well typed since Set != Set a ---I must admit, I tried to use Level.lift here, but failed to do so. More generally, this will also not allow me to express closure properties, such as P is closed under arbitrary unions ---this is what I'm really interested in.

I understand that I can just avoid level polymorphism,

ℙ' : ∀ {a} → Set a → Set (suc zero ⊔ a)
ℙ' {a} X = X → Set

but then simple items such as the largest subset,

ℙ'-⊤ : ∀ {i} {A : Set i} → ℙ' A
ℙ'-⊤ {i} {A} = λ e → Σ a ∶ A • a ≡ e
-- Σ_∶_•_ is just syntax for Σ A (λ a → ...)

will not even typecheck!

Perhaps I did not realise the notion of subset as predicate appropriately ---any advice would be appreciated. Thank-you!

Answer 1

You need to lift b out from P like this

record SetWithAPredicate {a c} b : Set {!!} where
  field
   S : Set a
   P : ℙ {b} S → Set c

Yes, this is ugly and annoying, but that's how it's done in Agda (an example from standard library: _>>=_ is not properly universe polymorphic). Lift can help sometimes, but it quickly gets out of hand.

Perhaps I did not realise the notion of subset as predicate appropriately ---any advice would be appreciated.

Your definition is correct, but there is another one, see 4.8.3 in Conor McBride's lecture notes.