{-# OPTIONS --universe-polymorphism #-}

open import Level

module Equality where

infix  _≡_

data _≡_ {l : Level} {A : Set l} (a : A) : A → Set l where
    refl : a ≡ a

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}