为什么 Agda 拒绝 Set₁ → Set₁？答案

【问题标题】：Why is Agda refusing Set₁ → Set₁?为什么 Agda 拒绝 Set₁ → Set₁？
【发布时间】：2021-02-28 16:13:15
【问题描述】：

代码如下：

Continuation : Set → Set₁ → Set₁
Continuation R X = (X → R) → R

Selection : Set → Set₁ → Set₁
Selection R X = (X → R) → X

dagger : {R : Set} → Selection R → Continuation R
dagger S X k = k (S k)

出于其他原因，我需要继续和选择以使用更高的宇宙。但是接下来dagger的定义就报错了：

(Set₁ → Set₁) 应该是一种排序，但在检查应用程序的推断类型时不是设置₁ → 设置₁ 匹配预期类型_16

【问题讨论】：

标签： agda

【解决方案1】：

在 Agda 中，_→_ 是函数空间，不是任何类别，而是类型和职能。我的猜测是您想要以下内容：

dagger : {R : Set} → ∀ X → Selection R X → Continuation R X
dagger X S k = k (S k)

即索引类型和索引保留函数的函数空间。

或者，您可以使用标准库的 Relation.Unary 态射概念并写：

open import Relation.Unary

dagger : {R : Set} → Selection R ⊆ Continuation R
dagger S k = k (S k)

【讨论】：

谢谢！所以我理解更正，但我不明白你对第一句话的意思。
第一句可以忽略。我假设您来自类别理论，因为您试图以这种方式编写代码。如果不是这种情况，那么该解释将无济于事。只要你得到修复，这才是最重要的。
是的，你的猜测是正确的。所以也许我发现我试图做的事情不适合我想做的事情。我仍然不明白这个错误，可能是因为我不知道_16 应该是什么类型。写一个从Set1到Set1的函数不是可以接受吗？
当 Agda 对一个类型进行排序检查时，它不知道期望什么排序。我希望_16 是未知排序的内部元变量。当这些事情泄漏到面向用户的诊断程序中时，它有点粗糙，但我还有三个手指，指向我。