polished

UrsSchreiber · Nov 21, 2011 · 70ff9f2 · 70ff9f2
1 parent 17d2dc8
commit 70ff9f2
Showing 1 changed file with 2 additions and 4 deletions.
diff --git a/README b/README
@@ -9,15 +9,13 @@ the internal language of infinity-toposes
 
 The directory "Hott/Coq" contains Coq code
 
-  htt://ncatlab.org/nlab/show/Coq
+  http://ncatlab.org/nlab/show/Coq
 
 for Martin-L�f type theory
 
   http://ncatlab.org/nlab/Martin-L�f+type+theory .
 
-that sets up the basic notions of homotopy type theory
-
-  http://ncatlab.org/nlab/show/homotopy+type+theory ,
+that sets up the basic notions of homotopy type theory.
 
 The subdirectory "HoTT/Coq/HIT" contains code that sets up
 higher inductive types