From a57f45d93f53b672ca61b34c7657e705831576d5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 23 Feb 2018 12:33:20 +0100
Subject: [PATCH] Remove yet another postulate

---
 src/Cat/Categories/Cat.agda | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 6623936..02f4838 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -86,8 +86,9 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
 
       module C = Category ℂ
       module D = Category 𝔻
-      postulate
-        issSet : {A B : RawCategory.Object :rawProduct:} → isSet (Arrow A B)
+      open import Cubical.Sigma
+      issSet : {A B : RawCategory.Object :rawProduct:} → isSet (Arrow A B)
+      issSet = setSig {sA = C.arrowIsSet} {sB = λ x → D.arrowIsSet}
       ident' : IsIdentity :𝟙:
       ident'
         = Σ≡ (fst C.ident) (fst D.ident)