{-

Absolute basics:
  ∙ universe levels for the ambient type theory;
  ∙ definition of equality (with axiom K provided by the --with-K flag).

-}
module basic.prelude where

open import Agda.Primitive public renaming (Set to Type)

data _≡_ {ℓ} {A : Type ℓ} (a : A) : A → Type ℓ where
  instance
    refl : a ≡ a

infix  _≡_

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REWRITE _≡_ #-}