在 Agda 中，有两种不同的相等概念：Pointwise Equality 和 Propositional Equality。 Pointwise Equality 是指两个对象在每个点上都相等，即函数在每个输入上产生相同的输出。 Propositional Equality 是指两个对象在全局上相等，即它们可以互换使用而不会影响程序的正确性。

通过以下代码示例可以更好地理解两者之间的区别：

-- Pointwise Equality f : ℕ → ℕ f x = x + 1

g : ℕ → ℕ g x = 2 * x

-- 两个函数在每个输入上都相等 h : ∀ (x : ℕ) → f x ≗ g x h x = refl

-- Propositional Equality data Vec (A : Set) : ℕ → Set where Nil : Vec A zero Cons : (x : A) → (xs : Vec A n) → Vec A (succ n)

-- 定义两个相同的向量 exampleVec1 : Vec ℕ 2 exampleVec1 = Cons 1 (Cons 2 Nil)

exampleVec2 : Vec ℕ 2 exampleVec2 = Cons 1 (Cons 2 Nil)

-- 这两个向量是全局相等的 example : exampleVec1 ≡ exampleVec2 example = refl