set - 适当使用宇宙多态性

Question

我已经在一个 Agda 项目上工作了几个星期，尽我所能地忽略关卡多态性。不幸的是（或者也许幸运的是）我似乎已经到了需要开始理解它的地步。

到目前为止，我只在需要它们作为第二个参数Rel（或第三个参数REL）时才使用级别变量。否则我就省略了，直接使用Set。现在我有一些客户端代码可以显式量化各个级别a，并尝试将某些类型的表单传递Set a给我现有的代码，这些代码现在不够多态。在下面的示例中，quibble代表客户端代码，并且_[_]×[_]_是≈-List我现有代码的典型代表，它仅使用Set.

module Temp where

open import Data.List
open import Data.Product
open import Level
open import Relation.Binary

-- Direct product of binary relations.
_[_]×[_]_ : {ℓ₁ ℓ₂ : Level} {A B C D : Set} → A × B → REL A C ℓ₁ → REL B D ℓ₂ → C × D → Set (ℓ₁ ⊔ ℓ₂)
(a , b) [ _R_ ]×[ _S_ ] (c , d) = a R c × b S d

-- Extend a setoid (A, ≈) to List A.
data ≈-List {ℓ : Level} {A : Set} (_≈_ : Rel A ℓ) : Rel (List A) ℓ where
   [] : ≈-List _≈_ [] []
   _∷_ : {x y : A} {xs ys : List A} → (x≈y : x ≈ y) → (xs≈ys : ≈-List _≈_ xs ys) → ≈-List _≈_ (x ∷ xs) (y ∷ ys)

quibble : {a ℓ : Level} {A : Set a} → Rel A ℓ → Rel (List (A × A)) ℓ
quibble _≈_ = ≈-List (λ x y → x [ _≈_ ]×[ _≈_ ] y)

≈-List在这里，我可以使用额外的级别参数扩展 的归纳定义，a以便它可以采用 type 的类型参数Set a，但是我不清楚输入和输出关系的宇宙应该如何变化。然后问题蔓延到更复杂的定义，例如_[_]×[_]_我更不确定如何进行。

我应该如何概括给出的示例中的签名，以便quibble编译？有没有我可以遵循的一般规则？我读过这个。

Answer 1