From e7c174719b8eebc41a05a8c5957a3f282067fcef Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Thu, 2 Mar 2017 17:08:00 -0500
Subject: [PATCH] fix typo

---
 algebra/is_short_exact.hlean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/algebra/is_short_exact.hlean b/algebra/is_short_exact.hlean
index e7422fc..3f94ced 100644
--- a/algebra/is_short_exact.hlean
+++ b/algebra/is_short_exact.hlean
@@ -19,4 +19,4 @@ structure is_short_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C)
   (is_emb    : is_embedding f)
   (im_in_ker : Π(a:A), g (f a) = pt)
   (ker_in_im : Π(b:B), (g b = pt) → fiber f b)
-   is_surj   : is_split_surjective g)
+  (is_surj   : is_split_surjective g)