将一个类型提升到更高的宇宙

Question

在我正在处理的形式化中，我需要将 Unit 类型从在 UniverseSet上定义的 Agda 标准库提升为像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 ?。我找到了阅读以下答案部分的解决方案。