agda - Set₀ でのシステム F のパラメトリック多形性のモデル化

Question

システム F では、ポリモーフィック型の種類は*(とにかくシステム F ではそれが唯一の種類であるため...)、たとえば次の閉じた型の場合:

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

Agda で System F を表現し*たいと考えていSetます。のようなもの

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 に組み込むことはできませんか?