From b5f89322ac3c4992598d1915bb9c714eb44bdcb7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Thu, 5 Apr 2018 15:13:59 +0200
Subject: [PATCH] Add notion of strict category

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

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index b182e02..fcae234 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -319,6 +319,14 @@ record PreCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     isPreCategory  : IsPreCategory raw
   open IsPreCategory isPreCategory public
 
+-- Definition 9.6.1 in [HoTT]
+record StrictCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
+  field
+    preCategory : PreCategory ℓa ℓb
+  open PreCategory preCategory
+  field
+    objectsAreSets : isSet Object
+
 record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
   field
     isPreCategory : IsPreCategory ℂ