{-# OPTIONS --without-K #-} module pointed where open import pointed.core public open import pointed.equality public