From 7787a8f0be55e3fbf50036251e7fcc83944c6d62 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:52:14 +0100
Subject: [PATCH] Indentation

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

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 6c3172e..cec311d 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -102,9 +102,9 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
   open Univalence ℂ public
   field
     isAssociative : IsAssociative
-    isIdentity : IsIdentity 𝟙
+    isIdentity    : IsIdentity 𝟙
     arrowsAreSets : ArrowsAreSets
-    univalent : Univalent isIdentity
+    univalent     : Univalent isIdentity
 
 -- `IsCategory` is a mere proposition.
 module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where