diff --git a/src/Mugen/Algebra/Displacement/Instances/Endomorphism.agda b/src/Mugen/Algebra/Displacement/Instances/Endomorphism.agda
index 09fd74f..c8307b5 100644
--- a/src/Mugen/Algebra/Displacement/Instances/Endomorphism.agda
+++ b/src/Mugen/Algebra/Displacement/Instances/Endomorphism.agda
@@ -12,7 +12,7 @@ open import Mugen.Prelude
 
 open import Mugen.Algebra.Displacement
 open import Mugen.Cat.Monad
-open import Mugen.Cat.StrictOrders
+open import Mugen.Cat.Instances.StrictOrders
 open import Mugen.Order.StrictOrder
 open import Mugen.Order.Instances.Endomorphism
   renaming (Endomorphism to Endomorphism-poset)
diff --git a/src/Mugen/Cat/HierarchyTheory.agda b/src/Mugen/Cat/HierarchyTheory.agda
index b04746c..ec0fb6f 100644
--- a/src/Mugen/Cat/HierarchyTheory.agda
+++ b/src/Mugen/Cat/HierarchyTheory.agda
@@ -4,7 +4,7 @@ open import Cat.Diagram.Monad
 import Cat.Reasoning as Cat
 
 open import Mugen.Prelude
-open import Mugen.Cat.StrictOrders
+open import Mugen.Cat.Instances.StrictOrders
 open import Mugen.Order.StrictOrder
 
 --------------------------------------------------------------------------------
diff --git a/src/Mugen/Cat/HierarchyTheory/McBride.agda b/src/Mugen/Cat/HierarchyTheory/McBride.agda
index 1b7576d..0be9c29 100644
--- a/src/Mugen/Cat/HierarchyTheory/McBride.agda
+++ b/src/Mugen/Cat/HierarchyTheory/McBride.agda
@@ -6,7 +6,7 @@ open import Mugen.Prelude
 open import Mugen.Algebra.Displacement
 open import Mugen.Order.Instances.LeftInvariantRightCentered
 open import Mugen.Order.StrictOrder
-open import Mugen.Cat.StrictOrders
+open import Mugen.Cat.Instances.StrictOrders
 open import Mugen.Cat.HierarchyTheory
 
 import Mugen.Order.Reasoning
diff --git a/src/Mugen/Cat/HierarchyTheory/Universality.agda b/src/Mugen/Cat/HierarchyTheory/Universality.agda
index 682e1c8..0843c41 100644
--- a/src/Mugen/Cat/HierarchyTheory/Universality.agda
+++ b/src/Mugen/Cat/HierarchyTheory/Universality.agda
@@ -16,19 +16,13 @@ open import Mugen.Prelude
 open import Mugen.Algebra.Displacement
 open import Mugen.Algebra.Displacement.Instances.Endomorphism
 
-open import Mugen.Cat.Endomorphisms
-open import Mugen.Cat.Indexed
-open import Mugen.Cat.StrictOrders
+open import Mugen.Cat.Instances.Endomorphisms
+open import Mugen.Cat.Instances.Indexed
+open import Mugen.Cat.Instances.StrictOrders
 open import Mugen.Cat.Monad
 open import Mugen.Cat.HierarchyTheory
 open import Mugen.Cat.HierarchyTheory.McBride
 
-open import Mugen.Order.StrictOrder
-open import Mugen.Order.Instances.Endomorphism renaming (Endomorphism to Endomorphism-poset)
-open import Mugen.Order.Instances.LeftInvariantRightCentered
-open import Mugen.Order.Instances.Lift
-open import Mugen.Order.Instances.Singleton
-
 import Mugen.Order.Reasoning as Reasoning
 
 --------------------------------------------------------------------------------
@@ -53,7 +47,6 @@ module Mugen.Cat.HierarchyTheory.Universality {o o' r}
   -- Notation
 
   private
-    open Strictly-monotone
     open Algebra-hom
     module H = Monad H
 
diff --git a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda
index 70df921..2a58d6d 100644
--- a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda
+++ b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda
@@ -14,8 +14,8 @@ open import Mugen.Prelude
 open import Mugen.Algebra.Displacement
 open import Mugen.Algebra.Displacement.Instances.Endomorphism
 
-open import Mugen.Cat.Endomorphisms
-open import Mugen.Cat.StrictOrders
+open import Mugen.Cat.Instances.Endomorphisms
+open import Mugen.Cat.Instances.StrictOrders
 open import Mugen.Cat.Monad
 open import Mugen.Cat.HierarchyTheory
 open import Mugen.Cat.HierarchyTheory.McBride
diff --git a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbeddingNaturality.agda b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbeddingNaturality.agda
index 2d0c131..4ce7445 100644
--- a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbeddingNaturality.agda
+++ b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbeddingNaturality.agda
@@ -15,8 +15,8 @@ open import Mugen.Prelude
 open import Mugen.Algebra.Displacement
 open import Mugen.Algebra.Displacement.Instances.Endomorphism
 
-open import Mugen.Cat.Endomorphisms
-open import Mugen.Cat.StrictOrders
+open import Mugen.Cat.Instances.Endomorphisms
+open import Mugen.Cat.Instances.StrictOrders
 open import Mugen.Cat.Monad
 open import Mugen.Cat.HierarchyTheory
 open import Mugen.Cat.HierarchyTheory.McBride
diff --git a/src/Mugen/Cat/HierarchyTheory/Universality/SubcategoryEmbedding.agda b/src/Mugen/Cat/HierarchyTheory/Universality/SubcategoryEmbedding.agda
index d7d36d3..7ac7d53 100644
--- a/src/Mugen/Cat/HierarchyTheory/Universality/SubcategoryEmbedding.agda
+++ b/src/Mugen/Cat/HierarchyTheory/Universality/SubcategoryEmbedding.agda
@@ -1,5 +1,6 @@
 -- vim: nowrap
 open import Data.Nat
+
 open import Order.Instances.Discrete
 open import Order.Instances.Disjoint
 
@@ -12,15 +13,14 @@ import Cat.Reasoning as Cat
 
 open import Mugen.Prelude
 
-open import Mugen.Cat.Endomorphisms
-open import Mugen.Cat.Indexed
-open import Mugen.Cat.StrictOrders
+open import Mugen.Cat.Instances.Endomorphisms
+open import Mugen.Cat.Instances.Indexed
+open import Mugen.Cat.Instances.StrictOrders
 open import Mugen.Cat.Monad
 open import Mugen.Cat.HierarchyTheory
 
 open import Mugen.Order.StrictOrder
 open import Mugen.Order.Instances.Copower
-open import Mugen.Order.Instances.Singleton
 
 import Mugen.Order.Reasoning as Reasoning
 
diff --git a/src/Mugen/Cat/Endomorphisms.agda b/src/Mugen/Cat/Instances/Endomorphisms.agda
similarity index 85%
rename from src/Mugen/Cat/Endomorphisms.agda
rename to src/Mugen/Cat/Instances/Endomorphisms.agda
index dd25d1a..48b0eaa 100644
--- a/src/Mugen/Cat/Endomorphisms.agda
+++ b/src/Mugen/Cat/Instances/Endomorphisms.agda
@@ -1,6 +1,6 @@
 open import Cat.Prelude
 
-module Mugen.Cat.Endomorphisms {o ℓ} where
+module Mugen.Cat.Instances.Endomorphisms {o ℓ} where
 
 --------------------------------------------------------------------------------
 -- The category of endomorphisms on an object.
@@ -8,7 +8,7 @@ module Mugen.Cat.Endomorphisms {o ℓ} where
 -- /Technically/ this is a monoid, but it's easier to work with
 -- in this form w/o having to introduce a delooping.
 
-open import Mugen.Cat.Indexed
+open import Mugen.Cat.Instances.Indexed
 
 Endos : (𝒞 : Precategory o ℓ) (X : 𝒞 .Precategory.Ob) → Precategory lzero ℓ
 Endos 𝒞 X = Indexed {I = ⊤} 𝒞 λ _ → X
diff --git a/src/Mugen/Cat/Indexed.agda b/src/Mugen/Cat/Instances/Indexed.agda
similarity index 92%
rename from src/Mugen/Cat/Indexed.agda
rename to src/Mugen/Cat/Instances/Indexed.agda
index ab65093..d11f3e2 100644
--- a/src/Mugen/Cat/Indexed.agda
+++ b/src/Mugen/Cat/Instances/Indexed.agda
@@ -1,6 +1,6 @@
 open import Cat.Prelude
 
-module Mugen.Cat.Indexed {o o' ℓ} {I : Type o'} where
+module Mugen.Cat.Instances.Indexed {o o' ℓ} {I : Type o'} where
 
 import Cat.Reasoning as Cat
 
diff --git a/src/Mugen/Cat/StrictOrders.agda b/src/Mugen/Cat/Instances/StrictOrders.agda
similarity index 96%
rename from src/Mugen/Cat/StrictOrders.agda
rename to src/Mugen/Cat/Instances/StrictOrders.agda
index 541c823..9f82af0 100644
--- a/src/Mugen/Cat/StrictOrders.agda
+++ b/src/Mugen/Cat/Instances/StrictOrders.agda
@@ -1,4 +1,4 @@
-module Mugen.Cat.StrictOrders where
+module Mugen.Cat.Instances.StrictOrders where
 
 open import Mugen.Prelude
 open import Mugen.Order.StrictOrder
diff --git a/src/Mugen/Everything.agda b/src/Mugen/Everything.agda
index c97393f..13e2574 100644
--- a/src/Mugen/Everything.agda
+++ b/src/Mugen/Everything.agda
@@ -20,16 +20,16 @@ import Mugen.Algebra.Displacement.Instances.Product
 import Mugen.Algebra.Displacement.Instances.Support
 import Mugen.Algebra.Displacement.Subalgebra
 import Mugen.Algebra.OrderedMonoid
-import Mugen.Cat.Endomorphisms
 import Mugen.Cat.HierarchyTheory
 import Mugen.Cat.HierarchyTheory.McBride
 import Mugen.Cat.HierarchyTheory.Universality
 import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding
 import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality
 import Mugen.Cat.HierarchyTheory.Universality.SubcategoryEmbedding
-import Mugen.Cat.Indexed
+import Mugen.Cat.Instances.Endomorphisms
+import Mugen.Cat.Instances.Indexed
+import Mugen.Cat.Instances.StrictOrders
 import Mugen.Cat.Monad
-import Mugen.Cat.StrictOrders
 import Mugen.Data.List
 import Mugen.Data.NonEmpty
 import Mugen.Order.Instances.BasedSupport
diff --git a/src/Mugen/Order/Instances/Endomorphism.agda b/src/Mugen/Order/Instances/Endomorphism.agda
index a476083..9f96af2 100644
--- a/src/Mugen/Order/Instances/Endomorphism.agda
+++ b/src/Mugen/Order/Instances/Endomorphism.agda
@@ -6,8 +6,8 @@ import Cat.Reasoning as Cat
 open import Mugen.Prelude
 
 open import Mugen.Order.StrictOrder
-open import Mugen.Cat.StrictOrders
 open import Mugen.Cat.Monad
+open import Mugen.Cat.Instances.StrictOrders
 
 import Mugen.Order.Reasoning as Reasoning