{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
 
module Agda.Builtin.Equality where
 
infix  _≡_
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  instance refl : x ≡ x
 
{-# BUILTIN EQUALITY _≡_ #-}