从agda获得第二个参数？

Question

在下面的数据类型，

data _≡_ {A : Set} (x : A) : A → Set where 
    refl : x ≡ x 

我想明白这一点，如：

如果A是Set型的，是隐含的x是第一个参数和A类型，那么这将构建类型为A → Set的数据。

请解释一下。我没有得到第二个x，在构造函数refl。

Answer 1

关键这里的区别是参数（在这种情况下A和x）和指数（在A → Set的A）之间。

参数位于数据声明中冒号的左侧。他们在范围内的范围内，可能不会有所不同（因此他们的名字）。这是什么让你将数据写入宣言，如List其中包含在这些List元素的类型声明一劳永逸：

data List (A : Set) : Set where 
    nil : List A 
    cons : A → List A → List A 

，而不是用∀ A →提到它在每一个构造函数：

data List : Set → Set1 where 
    nil : ∀ A → List A 
    cons : ∀ A → A → List A → List A 

的指数位于在数据声明冒号的右边。它们可以是由构造函数引入的新变量，也可以是与其他术语相同的约束。

如果用自然数的工作就可以了，例如，建立一个谓语，指出了一些不zero就像这样：

open import Data.Nat 
data NotZero : (n : ℕ) → Set where 
    indeed1 : NotZero (suc zero) 
    indeed2+ : ∀ p → NotZero (suc (suc p)) 

这里n数据声明的类型签名提到的是指数。它受到不同构造函数的不同约束：indeed1表示n是1而indeed2+表示n的形状为suc (suc p)。

要回到你在你的问题引用的声明，我们可以在一个完全明确的等价形式重新制定它：

data Eq (A : Set) (x : A) : (y : A) → Set where 
    refl : Eq A x x 

这里我们看到Eq有两个参数（A是一组与x是一个元素A）和一个索引y这是我们要声称等于x。 refl指出，建立两个东西x和y相等的证明的唯一方法是如果它们完全相同;它将y约束为x。