module Imports.Test where

open import Common.Level

record Foo (ℓ : Level) : Set ℓ where