阿格达语中这两种平等定义有什么区别？

问：

我安装了 Agda 并开始玩。我试图定义一个相等类型，并提出了以下解决方案：

data _≡_ {A : Set} : A -> A -> Set where
  refl : {x : A} -> x ≡ x

但是，在 Ulf Norell 和 James Chapman 的教程中，他们是这样定义的：

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

与我的版本有什么区别（除了选择不同的角色）？推荐哪一个？