Update HIT_README.txt. Address issue #26.

HoTT · May 9, 2017 · 479457c · 479457c
1 parent 7278ce7
commit 479457c
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/core/lib/types/HIT_README.txt b/core/lib/types/HIT_README.txt
@@ -5,6 +5,15 @@
 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 
 
+Note
+====
+
+This document is kept as a historical record. The higher inductive types have
+since been implemented using the new Agda feature---rewriting rules---which are
+cleaner and potentially more reliable than the hacks (described in this document)
+to guard the abstraction. See core/lib/types/Pushout.agda for an example.
+
+
 Introduction
 ============