1{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
2 --no-subtyping #-}
3
4module Agda.Builtin.Equality where
5
6infix 4 _≡_
7data _≡_ {a} {A : Set a} (x : A) : A → Set a where
8 instance refl : x ≡ x
9
10{-# BUILTIN EQUALITY _≡_ #-}
11