From e8e41ed745235f5e0773ab6c7727b6d22917ca7e Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 30 Apr 2015 12:31:22 -0400 Subject: [PATCH] fix(types.md): add all files, add some explanation --- hott/types/types.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) 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)