From cc1ddaac9f3cadbcc5f86e9a969d23de7664cdb7 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 10:35:42 +0100
Subject: [PATCH] Add new type-synonym

---
 src/Cat/Category.agda | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 686ae76..536f0b7 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -49,6 +49,9 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   IsIdentity id = {A B : Object} {f : Arrow A B}
     → f ∘ id ≡ f × id ∘ f ≡ f
 
+  ArrowsAreSets : Set (ℓa ⊔ ℓb)
+  ArrowsAreSets = ∀ {A B : Object} → isSet (Arrow A B)
+
   IsInverseOf : ∀ {A B} → (Arrow A B) → (Arrow B A) → Set ℓb
   IsInverseOf = λ f g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙
 
@@ -100,7 +103,7 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
   field
     assoc : IsAssociative
     ident : IsIdentity 𝟙
-    arrowIsSet : ∀ {A B : Object} → isSet (Arrow A B)
+    arrowIsSet : ArrowsAreSets
     univalent : Univalent ident
 
 -- `IsCategory` is a mere proposition.
@@ -162,8 +165,13 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
       ident : (λ _ → IsIdentity 𝟙) [ X.ident ≡ Y.ident ]
       ident = propIsIdentity x X.ident Y.ident
       done : x ≡ y
-      U : ∀ {a : IsIdentity 𝟙} → (λ _ → IsIdentity 𝟙) [ X.ident ≡ a ] → (b : Univalent a) → Set _
-      U eqwal bbb = (λ i → Univalent (eqwal i)) [ X.univalent ≡ bbb ]
+      U : ∀ {a : IsIdentity 𝟙}
+        → (λ _ → IsIdentity 𝟙) [ X.ident ≡ a ]
+        → (b : Univalent a)
+        → Set _
+      U eqwal bbb =
+        (λ i → Univalent (eqwal i))
+        [ X.univalent ≡ bbb ]
       P : (y : IsIdentity 𝟙)
         → (λ _ → IsIdentity 𝟙) [ X.ident ≡ y ] → Set _
       P y eq = ∀ (b' : Univalent y) → U eq b'