From caddf83a097d7fb9eba022bf4a0751c7001179d0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 25 Feb 2018 14:37:28 +0100
Subject: [PATCH] Let `IsCategory` reexport RawCategory

---
 src/Cat/Categories/Free.agda | 2 --
 src/Cat/Category.agda        | 5 ++---
 2 files changed, 2 insertions(+), 5 deletions(-)

diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda
index 5441abc..9a0c891 100644
--- a/src/Cat/Categories/Free.agda
+++ b/src/Cat/Categories/Free.agda
@@ -7,8 +7,6 @@ open import Data.Product
 
 open import Cat.Category
 
-open IsCategory
-
 data Path {ℓ ℓ' : Level} {A : Set ℓ} (R : A → A → Set ℓ') : (a b : A) → Set (ℓ ⊔ ℓ') where
   empty : {a : A} → Path R a a
   cons : {a b c : A} → R b c → Path R a b → Path R a c
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 31b7cdd..dba717a 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -100,7 +100,7 @@ module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
     Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
 
 record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
-  open RawCategory ℂ
+  open RawCategory ℂ public
   open Univalence ℂ public
   field
     isAssociative : IsAssociative
@@ -112,7 +112,7 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
 module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
   open RawCategory C
   module _ (ℂ : IsCategory C) where
-    open IsCategory ℂ
+    open IsCategory ℂ using (isAssociative ; arrowsAreSets ; isIdentity ; Univalent)
     open import Cubical.NType
     open import Cubical.NType.Properties
 
@@ -196,7 +196,6 @@ record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     raw : RawCategory ℓa ℓb
     {{isCategory}} : IsCategory raw
 
-  open RawCategory raw public
   open IsCategory isCategory public
 
 module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where