From a4f8a37e365e01701f40a8cb83379074a9ee02d2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 20 Feb 2018 18:01:26 +0100
Subject: [PATCH] Proove that `IsCategory` is a mere proposition!

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

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 224e279..df9e67f 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -165,7 +165,7 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
       P y eq = ∀ (b' : Univ y) → U eq b'
       helper : ∀ (b' : Univ X.ident)
         → (λ _ → Univ X.ident) [ X.univalent ≡ b' ]
-      helper univ = {!!}
+      helper univ = propUnivalent x X.univalent univ
       foo = pathJ P helper Y.ident ident
       eqUni : U ident Y.univalent
       eqUni = foo Y.univalent