From 4a98b2aa3d6db03840f37cac4eeb5626b14eb61d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 12 Dec 2017 12:39:58 +0100
Subject: [PATCH] Leftovers...

---
 src/Category.agda | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/Category.agda b/src/Category.agda
index 7504bd1..b1f7c88 100644
--- a/src/Category.agda
+++ b/src/Category.agda
@@ -4,9 +4,11 @@ module Category where
 
 open import Agda.Primitive
 open import Data.Unit.Base
-open import Data.Product
-open import Cubical.PathPrelude
+open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
 open import Data.Empty
+open import Function
+
+open import Cubical
 
 postulate undefined : {ℓ : Level} → {A : Set ℓ} → A
 
@@ -216,7 +218,7 @@ module _ {ℓ ℓ' : Level} where
       ident-l : identity ⊛ f ≡ f
       ident-l = {!!}
 
-  CatCat : Category {ℓ-suc (ℓ ⊔ ℓ')} {ℓ ⊔ ℓ'}
+  CatCat : Category {lsuc (ℓ ⊔ ℓ')} {ℓ ⊔ ℓ'}
   CatCat =
     record
       { Object = Category {ℓ} {ℓ'}