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