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