Add some required algebraic types.

1 files changed, 15 insertions, 0 deletions

diff --git a/Everything.agda b/Everything.agda
index 5f0a173..1acafde 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -8,6 +8,21 @@
 
 module Everything where
 
+-- Definitions for more algebraic structures
+import Helium.Algebra.Bundles
+
+-- Relations between properties of functions when the underlying relation is a setoid
+import Helium.Algebra.Consequences.Setoid
+
+-- More core algebraic definitions
+import Helium.Algebra.Core
+
+-- More properties of functions
+import Helium.Algebra.Definitions
+
+-- Some more algebraic structures
+import Helium.Algebra.Structures
+
 -- Definition of types and operations used by the Armv8-M pseudocode.
 import Helium.Data.Pseudocode