diff --git a/src/Category.agda b/src/Category.agda
index ef5c2c4..d1aa814 100644
--- a/src/Category.agda
+++ b/src/Category.agda
@@ -6,6 +6,7 @@ open import Agda.Primitive
 open import Data.Unit.Base
 open import Data.Product
 open import Cubical.PathPrelude
+open import Data.Empty
 
 postulate undefined : {ℓ : Level} → {A : Set ℓ} → A
 
@@ -115,8 +116,6 @@ module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} { A B : Object ℂ } w
   iso-is-epi-mono : ∀ {X} (f : ℂ.Arrow A B ) → Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
   iso-is-epi-mono f iso = iso-is-epi f iso , iso-is-mono f iso
 
-data ⊥ : Set where
-
 ¬_ : {ℓ : Level} → Set ℓ → Set ℓ
 ¬ A = A → ⊥