From 316de7e4f9a6a88963dd09dcaa71a3c79af9ce96 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 21 Jan 2018 14:32:27 +0100
Subject: [PATCH] Remove `undefined`

---
 src/Cat/Category.agda | 2 --
 1 file changed, 2 deletions(-)

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 ℓ')