refactor: minor tweaks

RedPRL · May 31, 2024 · 78462d6 · 78462d6
1 parent dbe60b7
commit 78462d6
Show file tree

Hide file tree

Showing 12 changed files with 22 additions and 29 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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 → src/Mugen/Cat/Instances/Endomorphisms.agda b/src/Mugen/Cat/Endomorphisms.agda → src/Mugen/Cat/Instances/Endomorphisms.agda
@@ -1,14 +1,14 @@
 open import Cat.Prelude
 
-module Mugen.Cat.Endomorphisms {o ℓ} where
+module Mugen.Cat.Instances.Endomorphisms {o ℓ} where
 
 --------------------------------------------------------------------------------
 -- The category of endomorphisms on an object.
 --
 -- /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 → src/Mugen/Cat/Instances/Indexed.agda b/src/Mugen/Cat/Indexed.agda → 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 → src/Mugen/Cat/Instances/StrictOrders.agda b/src/Mugen/Cat/StrictOrders.agda → 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
@@ -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
@@ -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