From 74824078a8c7b31364fa690b236aadd448cec7b9 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Thu, 19 Mar 2015 10:48:15 -0400
Subject: [PATCH] fix(hott/algebra) fix previous commit by importing 'arity'

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

diff --git a/hott/algebra/precategory/basic.hlean b/hott/algebra/precategory/basic.hlean
index 5ef15adcd5..a664ca0cd7 100644
--- a/hott/algebra/precategory/basic.hlean
+++ b/hott/algebra/precategory/basic.hlean
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: algebra.precategory.basic
 Authors: Floris van Doorn
 -/
-import types.trunc types.pi
+import types.trunc types.pi arity
 
 open eq is_trunc pi