Add to the index and add a new section on the DiscreteLocale directory

martinescardo · Sep 17, 2024 · 989bcdc · 989bcdc
1 parent 9db6bc7
commit 989bcdc
Showing 1 changed file with 18 additions and 5 deletions.
diff --git a/source/Locales/index.lagda b/source/Locales/index.lagda
@@ -48,6 +48,24 @@ import Locales.Compactness.Properties
 
 \end{code}
 
+\section{The discrete locale}
+
+The `DiscreteLocale` directory contains
+
+  1. Definition of the discrete locale over a set.
+  2. Construction of a directed basis for the discrete locale.
+  3. The discrete locale on the type of Booleans.
+  4. Properties of the discrete locale on the type of Booleans.
+
+\begin{code}
+
+import Locales.DiscreteLocale.Basis
+import Locales.DiscreteLocale.Definition
+import Locales.DiscreteLocale.Two
+import Locales.DiscreteLocale.Two-Properties
+
+\end{code}
+
 \begin{code}
 
 import Locales.AdjointFunctorTheoremForFrames    -- (1)
@@ -154,11 +172,6 @@ import Locales.Point.SpectralPoint-Definition
 
 import Locales.TerminalLocale.Properties
 
-import Locales.DiscreteLocale.Definition
-
-import Locales.DiscreteLocale.Two
-import Locales.DiscreteLocale.Two-Properties
-
 import Locales.SIP.FrameSIP
 import Locales.SIP.DistributiveLatticeSIP