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

Question

代码如下：

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₁)应为排序，但在检查应用程序集₁→Set₁的推断类型是否与预期类型匹配时不是

_

16

Answer 1

在Agda中

不是任何类别的函数空间，而是类型和函数的函数空间。我的猜测是您需要以下内容：

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

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

或者，您可以通过使用stdlib的

态射和write的概念：

open import Relation.Unary

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