From 1d040e5391d71f27869d6c33c698ce4ca49a42a1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 15 Nov 2017 22:56:04 +0100
Subject: [PATCH] Use bot from stdlib

---
 src/Category.agda | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

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 → ⊥