将类型升级到更高级的Universe

Question

在我正在进行的一项正式工作中，我需要将Agda标准库中的单元类型从Universe Set上定义为多态，如Set a。

我该怎么做？我知道，我可以只定义了另一种类型的，像这样的：

record Unit {l} : Set l where 
    constructor unit 

这是宇宙的多态性。但是，我相信这个问题应该有更习惯的解决方案。有人可以提供给我一个解决方案，或者如果没有办法向我解释理由吗？

Answer 1

其实找了一下标准库，我找到了需要的工具Level模块。该解决方案是使用类型Lift：

record Lift {a ℓ} (A : Set a) : Set (a ⊔ ℓ) where 
    constructor lift 
    field lower : A 

单位类型

record ⊤ : Set where 
    constructor tt 

可以解除使用Lift ⊤更高宇宙水平。我发现解决方案读取以下answer的一部分。