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: