Chuangjie Xu & Martin Escardo, 2014

\begin{code}

module Preliminaries where

open import Agda.Primitive using (Level ; lzero ; lsuc ; _⊔_)

data [] {i : Level} : Set i where
 ⋆ : []

record Σ {i j : Level}{A : Set i}(B : A → Set j) : Set(i ⊔ j) where
 constructor _,_
 field
  pr₁ : A
  pr₂ : B pr₁

open Σ public

data _≡_ {i : Level}{A : Set i} : A → A → Set i where
 refl : {a : A} → a ≡ a

\end{code}