From dce672a815616efd5d3a8b8eef85b1cb997ece2b Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 30 Apr 2015 23:26:55 -0400
Subject: [PATCH] fix(hott.md): mention arity.hlean

---
 hott/hott.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/hott/hott.md b/hott/hott.md
index ec0780893..e9548f8c0 100644
--- a/hott/hott.md
+++ b/hott/hott.md
@@ -9,6 +9,7 @@ modules and directories:
 * [hit](hit/hit.md): higher inductive types
 * [algebra](algebra/algebra.md) : algebraic structures
 * [cubical](cubical/cubical.md) : implementation of ideas from cubical type theory
+* [arity](arity.hlean) : a file containing theorems about functions with arity 2 or higher
 
 Lean's homotopy type theory kernel is a version of Martin-Löf Type Theory with: