在 Agda 中，点对点相等性意味着两个函数在每个输入都产生相同的结果。换句话说，对于函数 f 和 g，如果 f x ≗ g x，则对于任意 x，f 和 g 在 x 上是相等的。

命题相等性则表示两个类型或表达式是完全相同的，并可以用等同符号 ≡ 进行判定。在 Agda 中，使用 J 预定义类型来证明类型或表达式之间的命题相等性。

下面的示例展示了如何在 Agda 中使用命题相等性和点对点相等性：

data Vec (A : Set) : Nat -> Set where
  []    : Vec A zero
  _::_  : {n : Nat} -> A -> Vec A n -> Vec A (succ n)

v1 : Vec ℕ 2
v1 = 1 :: 2 :: []

v2 : Vec ℕ 2
v2 = 1 :: suc 1 :: []

v3 : Vec ℕ 2
v3 = 3 :: 4 :: []

-- 此处使用点对点相等性来判断两个 Vec 是否相等
-- 因为只有在相同的索引处元素相等才有意义
eqVec : {n : Nat} -> Vec ℕ n -> Vec ℕ n -> Bool
eqVec [] []         = true
eqVec (x :: xs) (y :: ys) = (x ≟ y) && (eqVec xs ys)
eqVec _ _           = false

-- 此处使用命题相等性来判断两个 Vec 是否相等
-- 因为 Vec 的结构是完全相同的，只是元素不同
eqVecP : {n : Nat} -> Vec ℕ n -> Vec ℕ n -> Set
eqVecP [] []         = Set
eqVecP (x :: xs