From 65c93b180d89e1fa503405727a4ef21487142dda Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 9 Dec 2015 00:17:42 -0500
Subject: [PATCH] fix(types.md): add num

---
 hott/types/types.md | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/hott/types/types.md b/hott/types/types.md
index b6243d8ce6..88490a378f 100644
--- a/hott/types/types.md
+++ b/hott/types/types.md
@@ -1,10 +1,11 @@
 hott.types
 ==========
 
-Types (not necessarily HoTT-related):
+Types in Martin-Lӧf Type Theory:
 
 * [unit](unit.hlean)
 * [bool](bool.hlean)
+* [num[(num.hlean) (natural numbers written in binary form)
 * [nat](nat/nat.md) (subfolder)
 * [int](int/int.md) (subfolder)
 * [prod](prod.hlean)
@@ -17,7 +18,9 @@ Types (not necessarily HoTT-related):
 * [lift](lift.hlean)
 * [list](list.hlean)
 
-HoTT types
+The number systems (num, nat, int, ...) are for a large part ported from the standard libary.
+
+Specific HoTT types
 
 * [eq](eq.hlean): show that functions related to the identity type are equivalences
 * [pointed](pointed.hlean): pointed types, maps, homotopies, and equivalences