diff --git a/.travis.yml b/.travis.yml
index bc104d3..4df3276 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -9,7 +9,7 @@ before_install:
 - docker pull scottfleischman/agda:2.5.2
 
 env:
-- AGDA_FILE="src/API/Laws.agda"
+- AGDA_FILE="src/API/Theorems.agda"
 
 script:
 - docker run -v $TRAVIS_BUILD_DIR:/opt/agda-build scottfleischman/agda:2.5.2 /bin/sh -c 'cd /opt/agda-build; agda '$AGDA_FILE
diff --git a/src/API.agda b/src/API.agda
index 3f09bbf..ea7afe7 100644
--- a/src/API.agda
+++ b/src/API.agda
@@ -1,6 +1,6 @@
 module API where
 
-open import Graph
+open import Algebra
 open import Prelude
 
 empty : ∀ {A} -> Graph A
diff --git a/src/API/Laws.agda b/src/API/Theorems.agda
similarity index 80%
rename from src/API/Laws.agda
rename to src/API/Theorems.agda
index cad8e69..3328d5d 100644
--- a/src/API/Laws.agda
+++ b/src/API/Theorems.agda
@@ -1,10 +1,10 @@
-module API.Laws where
+module API.Theorems where
 
+open import Algebra
+open import Algebra.Theorems
 open import API
-open import Graph
 open import Prelude
 open import Reasoning
-open import Theorems
 
 -- vertices [x] == vertex x
 vertices-vertex : ∀ {A} {x : A} -> vertices (x :: []) ≡ vertex x
@@ -18,4 +18,4 @@ vertices-clique {a} {_ :: t} = ⊆transitivity (⊆right-monotony (vertices-cliq
 -- clique (xs ++ ys) == connect (clique xs) (clique ys)
 connect-clique : ∀ {A} {xs ys : List A} -> clique (xs ++ ys) ≡ connect (clique xs) (clique ys)
 connect-clique {_} {[]}     = symmetry *left-identity
-connect-clique {a} {h :: t} = R (connect-clique {a} {t}) >> *associativity
+connect-clique {a} {_ :: t} = R (connect-clique {a} {t}) >> *associativity
diff --git a/src/Graph.agda b/src/Algebra.agda
similarity index 98%
rename from src/Graph.agda
rename to src/Algebra.agda
index 520e6c8..231a436 100644
--- a/src/Graph.agda
+++ b/src/Algebra.agda
@@ -1,4 +1,4 @@
-module Graph where
+module Algebra where
 
 -- Core graph construction primitives
 data Graph (A : Set) : Set where
diff --git a/src/Theorems.agda b/src/Algebra/Theorems.agda
similarity index 99%
rename from src/Theorems.agda
rename to src/Algebra/Theorems.agda
index e86a529..1dbdaea 100644
--- a/src/Theorems.agda
+++ b/src/Algebra/Theorems.agda
@@ -1,6 +1,6 @@
-module Theorems where
+module Algebra.Theorems where
 
-open import Graph
+open import Algebra
 open import Reasoning
 
 +pre-idempotence : ∀ {A} {x : Graph A} -> x + x + ε ≡ x
diff --git a/src/Prelude.agda b/src/Prelude.agda
index f51ab55..ba30d2c 100644
--- a/src/Prelude.agda
+++ b/src/Prelude.agda
@@ -18,6 +18,10 @@ data List (A : Set) : Set where
 
 infixr 20 _::_
 
+_++_ : ∀ {A} -> List A -> List A -> List A
+[] ++ l = l
+(x :: xs) ++ l = x :: (xs ++ l)
+
 foldr : ∀ {A B : Set} -> (A -> B -> B) -> B -> List A -> B
 foldr f b [] = b
 foldr f b (x :: xs) = f x (foldr f b xs)
@@ -25,7 +29,3 @@ foldr f b (x :: xs) = f x (foldr f b xs)
 map : ∀ {A B} -> (A -> B) -> List A -> List B
 map f [] = []
 map f (x :: xs) = f x :: map f xs
-
-_++_ : ∀ {A} -> List A -> List A -> List A
-[] ++ l = l
-(x :: xs) ++ l = x :: (xs ++ l)
diff --git a/src/Reasoning.agda b/src/Reasoning.agda
index 015ed80..5a051d2 100644
--- a/src/Reasoning.agda
+++ b/src/Reasoning.agda
@@ -1,6 +1,6 @@
 module Reasoning where
 
-open import Graph
+open import Algebra
 
 -- Standard syntax sugar for writing equational proofs
 infix 4 _≈_