diff --git a/FiniteSets/FSets.v b/FiniteSets/FSets.v
new file mode 100644
index 0000000..8b1d63c
--- /dev/null
+++ b/FiniteSets/FSets.v
@@ -0,0 +1,7 @@
+Require Export HoTT HitTactics.
+Require Export representations.definition.
+From fsets Require Export
+     monad
+     extensionality
+     properties
+     properties_decidable.
\ No newline at end of file
diff --git a/FiniteSets/_CoqProject b/FiniteSets/_CoqProject
index ce39aff..aa0f7e5 100644
--- a/FiniteSets/_CoqProject
+++ b/FiniteSets/_CoqProject
@@ -2,16 +2,17 @@
 -R ../prelude ""
 lattice.v
 disjunction.v
-bad.v
-definition.v
-operations.v
-properties.v
-operations_decidable.v
-extensionality.v
-properties_decidable.v
-monad.v
-cons_repr.v
-lists.v
-enumerated.v
+representations/bad.v
+representations/definition.v
+fsets/operations.v
+fsets/properties.v
+fsets/operations_decidable.v
+fsets/extensionality.v
+fsets/properties_decidable.v
+fsets/monad.v
+FSets.v
+representations/cons_repr.v
+implementations/lists.v
+variations/enumerated.v
 #empty_set.v
 #ordered.v
diff --git a/FiniteSets/extensionality.v b/FiniteSets/fsets/extensionality.v
similarity index 96%
rename from FiniteSets/extensionality.v
rename to FiniteSets/fsets/extensionality.v
index 89237a3..838afb9 100644
--- a/FiniteSets/extensionality.v
+++ b/FiniteSets/fsets/extensionality.v
@@ -1,6 +1,7 @@
 (** Extensionality of the FSets *)
 Require Import HoTT HitTactics.
-Require Import definition operations properties.
+From representations Require Import definition.
+From fsets Require Import operations properties.
 
 Section ext.
 Context {A : Type}.
diff --git a/FiniteSets/monad.v b/FiniteSets/fsets/monad.v
similarity index 96%
rename from FiniteSets/monad.v
rename to FiniteSets/fsets/monad.v
index 0a06e5a..fce9a8e 100644
--- a/FiniteSets/monad.v
+++ b/FiniteSets/fsets/monad.v
@@ -1,6 +1,6 @@
 (* [FSet] is a (strong and stable) finite powerset monad *)
 Require Import HoTT HitTactics.
-Require Export definition properties.
+Require Export representations.definition fsets.properties.
 
 Definition ffmap {A B : Type} : (A -> B) -> FSet A -> FSet B.
 Proof.
diff --git a/FiniteSets/operations.v b/FiniteSets/fsets/operations.v
similarity index 93%
rename from FiniteSets/operations.v
rename to FiniteSets/fsets/operations.v
index 838a9e6..0a20230 100644
--- a/FiniteSets/operations.v
+++ b/FiniteSets/fsets/operations.v
@@ -1,6 +1,6 @@
 (* Operations on the [FSet A] for an arbitrary [A] *)
 Require Import HoTT HitTactics.
-Require Import definition disjunction lattice.
+Require Import representations.definition disjunction lattice.
 
 Section operations.
 Context {A : Type}.
diff --git a/FiniteSets/operations_decidable.v b/FiniteSets/fsets/operations_decidable.v
similarity index 93%
rename from FiniteSets/operations_decidable.v
rename to FiniteSets/fsets/operations_decidable.v
index bdc6e70..650d8b1 100644
--- a/FiniteSets/operations_decidable.v
+++ b/FiniteSets/fsets/operations_decidable.v
@@ -1,6 +1,6 @@
 (* Operations on [FSet A] when [A] has decidable equality *)
 Require Import HoTT HitTactics.
-Require Export definition operations.
+Require Export representations.definition fsets.operations.
 
 Section decidable_A.
   Context {A : Type}.
diff --git a/FiniteSets/properties.v b/FiniteSets/fsets/properties.v
similarity index 97%
rename from FiniteSets/properties.v
rename to FiniteSets/fsets/properties.v
index 6aa679f..c5fd21e 100644
--- a/FiniteSets/properties.v
+++ b/FiniteSets/fsets/properties.v
@@ -1,5 +1,5 @@
 Require Import HoTT HitTactics.
-Require Export definition operations disjunction.
+Require Export representations.definition disjunction fsets.operations.
 
 (* Lemmas relating operations to the membership predicate *)
 Section operations_isIn.
diff --git a/FiniteSets/properties_decidable.v b/FiniteSets/fsets/properties_decidable.v
similarity index 98%
rename from FiniteSets/properties_decidable.v
rename to FiniteSets/fsets/properties_decidable.v
index ffdd3ba..3080817 100644
--- a/FiniteSets/properties_decidable.v
+++ b/FiniteSets/fsets/properties_decidable.v
@@ -1,6 +1,7 @@
 (* Properties of [FSet A] where [A] has decidable equality *)
 Require Import HoTT HitTactics.
-Require Export properties extensionality lattice operations_decidable.
+From fsets Require Export properties extensionality operations_decidable.
+Require Export lattice.
 
 (* Lemmas relating operations to the membership predicate *)
 Section operations_isIn.
diff --git a/FiniteSets/lists.v b/FiniteSets/implementations/lists.v
similarity index 97%
rename from FiniteSets/lists.v
rename to FiniteSets/implementations/lists.v
index b331126..cb96c89 100644
--- a/FiniteSets/lists.v
+++ b/FiniteSets/implementations/lists.v
@@ -1,5 +1,5 @@
 Require Import HoTT HitTactics.
-Require Import cons_repr operations_decidable properties_decidable definition.
+Require Import representations.cons_repr FSets.
 
 Section Operations.
   Variable A : Type.
diff --git a/FiniteSets/bad.v b/FiniteSets/representations/bad.v
similarity index 100%
rename from FiniteSets/bad.v
rename to FiniteSets/representations/bad.v
diff --git a/FiniteSets/cons_repr.v b/FiniteSets/representations/cons_repr.v
similarity index 98%
rename from FiniteSets/cons_repr.v
rename to FiniteSets/representations/cons_repr.v
index d3fec87..87b592e 100644
--- a/FiniteSets/cons_repr.v
+++ b/FiniteSets/representations/cons_repr.v
@@ -1,5 +1,6 @@
 Require Import HoTT HitTactics.
-Require Import definition operations_decidable properties_decidable.
+Require Import representations.definition.
+From fsets Require Import operations_decidable properties_decidable.
 
 Module Export FSetC.
  
diff --git a/FiniteSets/definition.v b/FiniteSets/representations/definition.v
similarity index 100%
rename from FiniteSets/definition.v
rename to FiniteSets/representations/definition.v
diff --git a/FiniteSets/enumerated.v b/FiniteSets/variations/enumerated.v
similarity index 100%
rename from FiniteSets/enumerated.v
rename to FiniteSets/variations/enumerated.v