From f640cb65e9106be5674f8f13d9594d12966d823a Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Sun, 16 Jan 2022 16:59:55 +0000
Subject: Define ordered algebraic structures.

---
 Everything.agda | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'Everything.agda')

diff --git a/Everything.agda b/Everything.agda
index 80dd812..e1a82ae 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -23,6 +23,17 @@ import Helium.Algebra.Core
 -- More properties of functions
 import Helium.Algebra.Definitions
 
+-- Ordering properties of functions
+import Helium.Algebra.Ordered.Definitions
+
+-- Definitions of ordered algebraic structures like monoids and rings
+-- (packed in records together with sets, operations, etc.)
+import Helium.Algebra.Ordered.StrictTotal.Bundles
+
+-- Some ordered algebraic structures (not packed up with sets,
+-- operations, etc.)
+import Helium.Algebra.Ordered.StrictTotal.Structures
+
 -- Some more algebraic structures
 import Helium.Algebra.Structures
 
-- 
cgit v1.2.3