set - 在记录中实现级别多态子集

Question

使用子集的概念作为谓词，

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

我想考虑在子集上赋予谓词的结构，

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

由于 ℙ 中使用的水平量化，这是一个错误的结构。当我使用 S, P 作为模块的参数时一切正常，但我希望它们是记录，以便我可以在它们上形成构造并提供它们的实例。

我已经尝试了一些其他的事情，例如通过存在性将 ℙ 的级别 b 移动到定义中，但这导致了元变量问题。我还尝试更改 P 的类型，

P : ℙ {a} S → Set c

但是我不能再要求空集具有以下属性:

P-⊥ : P(λ _ → ⊥)

由于 Set != Set a，这不是很好的类型——我必须承认，我尝试在这里使用 Level.lift，但没有成功。更一般地说，这也不允许我表达闭包属性，例如 P 在任意联合下被关闭——这才是我真正感兴趣的。

我知道我可以避免级别多态性，

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

然后是简单的项目，例如最大的子集，

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

甚至不会进行类型检查!

也许我没有适本地意识到子集作为谓词的概念——任何建议都将不胜感激。谢谢!

Answer 1

你需要像这样从 P 中取出 b

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

是的，这很丑陋和烦人，但这就是它在 Agda 中的做法(来自标准库的 an example:_>>=_ 不是正确的宇宙多态)。 Lift 有时会有帮助，但速度很快 gets out of hand .

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

您的定义是正确的，但还有另一个定义，请参阅 Conor McBride 的 lecture notes 中的 4.8.3 .