diff --git a/hott/hit/hit.md b/hott/hit/hit.md
new file mode 100644
index 000000000..8ccdd43ec
--- /dev/null
+++ b/hott/hit/hit.md
@@ -0,0 +1,17 @@
+hit
+===
+
+Declaration and theorems of higher inductive types in Lean. We take two higher inductive types (hits) as primitive notions in Lean. We define all other hits in terms of these two hits. The hits which are primitive are n-truncation and type quotients. These are defined in [init.hit](../init.hit.hlean) and they have definitional computation rules on the point constructors.
+
+Files in this folder:
+
+* [type_quotient](type_quotient.hlean) (Type quotients, primitive)
+* [trunc](trunc.hlean) (truncation, primitive)
+* [colimit](colimit.hlean) (Colimits of arbitrary diagrams and sequential colimits, defined using type quotients)
+* [pushout](pushout.hlean) (Pushouts, defined using type quotients)
+* [coeq](coeq.hlean) (Co-equalizers, defined using type quotients)
+* [cylinder](cylinder.hlean) (Mapping cylinders, defined using type quotients)
+* [quotient](quotient.hlean) (Set-quotients, defined using type quotients and set-truncation)
+* [suspension](suspension.hlean) (Suspensions, defined using pushouts)
+* [sphere](sphere.hlean) (Higher spheres, defined recursively using suspensions)
+* [circle](circle.hlean)
\ No newline at end of file
diff --git a/hott/hott.md b/hott/hott.md
index 69b975cf8..6fa314b9c 100644
--- a/hott/hott.md
+++ b/hott/hott.md
@@ -6,12 +6,14 @@ modules and directories:
 
 * [init](init/init.md) : constants and theorems needed for low-level system operations
 * [types](types/types.md) : concrete datatypes and type constructors
+* [hit](hit/hit.md): higher inductive types
 * [algebra](algebra/algebra.md) : algebraic structures
 
+
 Lean's homotopy type theory kernel is a version of Martin-Löf Type Theory with:
 
 * universe polymorphism
-* a non-cumulative hierarchy of universes, `Type 0`, `Type 1`, ... 
+* a non-cumulative hierarchy of universes, `Type 0`, `Type 1`, ...
 * inductively defined types
 
 Note that there is no proof-irrelevant or impredicative universe.
@@ -19,4 +21,3 @@ Note that there is no proof-irrelevant or impredicative universe.
 By default, the univalence axiom is declared on initialization.
 
 See also the [standard library](../library/library.md).
-