agda - 在 Set₀ 建模 System F 的参数多态性

Question

在 System F 中，多态类型的类型是*（因为这是 System F 中唯一的类型......），例如对于以下封闭类型：

[] ⊢ (forall α : *. α → α) : *

我想在 Agda 中表示 System F，因为一切都在 中*，我想我会将类型（如上）解释为 Agda Sets; 所以像

evalTy : RepresentationOfAWellKindedClosedType → Set

但是，Agda 没有多态类型，因此在 Agda 中，上述类型需要是（大！）Π 类型：

idType = (α : Set) → α → α

这意味着它不在 Set₀ 中：

idType : Set
idType = (α : Set) → α → α

poly-level.agda:4,12-29
Set₁ != Set
when checking that the expression (α : Set) → α → α has type Set

有没有办法解决这个问题，或者 System F 在这个意义上不能嵌入到 Agda 中？

Answer 1