diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index a881c71..8ccad7e 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -22,8 +22,6 @@ open import Cubical
 
 syntax ∃!-syntax (λ x → B) = ∃![ x ] B
 
-postulate undefined : {ℓ : Level} → {A : Set ℓ} → A
-
 record IsCategory {ℓ ℓ' : Level}
   (Object : Set ℓ)
   (Arrow  : Object → Object → Set ℓ')