diff --git a/hott/types/types.md b/hott/types/types.md
index 77efad375..9e7cc9cf1 100644
--- a/hott/types/types.md
+++ b/hott/types/types.md
@@ -12,7 +12,6 @@ Various datatypes.
 * [hprop_trunc](hprop_trunc.hlean): in this file we prove that `is_trunc n A` is a mere proposition. We separate this from [trunc](trunc.hlean) to avoid circularity in imports.
 * [equiv](equiv.hlean)
 * [pointed](pointed.hlean)
-
-* [trunc](trunc.hlean)
-
-* [W](W.hlean) (not loaded by default)
\ No newline at end of file
+* [function](function.hlean): embeddings, (split) surjections, retractions
+* [trunc](trunc.hlean): truncation levels, n-Types, truncation
+* [W](W.hlean): W-types (not loaded by default)