data _@$\equiv$@_ {a} {A : Set a} (x : A) : A @$\rightarrow$@ Set a where
  refl : x @$\equiv$@ x