update README.md

martinescardo · Sep 5, 2023 · 123e4fb · 123e4fb
1 parent cd2f11a
commit 123e4fb
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 2 deletions.
diff --git a/README.md b/README.md
@@ -26,8 +26,18 @@ You can use the following BibTeX entry to cite `TypeTopology`:
 If you are citing only your own files, then create a different bibtex file
 with only your name as author.
 
+## Root of the development
+
+ * [source/index.lagda](source/index.lagda] (only `--safe` modules`)
+
+ * [source/AllModules.lagda](source/AllModules.lagda) (including "unsafe" ones)
+
+ * Each subdirectory has its own index file.
+
 ## Current contributors in alphabetical order of first name
 
+Please add yourself the first time you contribute.
+
 * Alice Laroche
 * Andrew Sneap
 * Ayberk Tosun

diff --git a/source/Fin/Dedekind.lagda b/source/Fin/Dedekind.lagda
@@ -37,8 +37,8 @@ open import Various.HiggsInvolutionTheorem
 
 \end{code}
 
-Example. A weakly connected type (a type that is connected if it is
-inhabited), is Dedekind finite, so, for instance, the circle S¹ is
+Example. A weakly connected type (a type that is (1-)connected if it
+is inhabited), is Dedekind finite, so, for instance, the circle S¹ is
 Dedekind finite.
 
 \begin{code}