From 78462d66f168f0b5809c329fda71584f0d640a25 Mon Sep 17 00:00:00 2001 From: favonia Date: Fri, 31 May 2024 08:49:07 -0500 Subject: [PATCH] refactor: minor tweaks --- .../Displacement/Instances/Endomorphism.agda | 2 +- src/Mugen/Cat/HierarchyTheory.agda | 2 +- src/Mugen/Cat/HierarchyTheory/McBride.agda | 2 +- src/Mugen/Cat/HierarchyTheory/Universality.agda | 13 +++---------- .../Universality/EndomorphismEmbedding.agda | 4 ++-- .../EndomorphismEmbeddingNaturality.agda | 4 ++-- .../Universality/SubcategoryEmbedding.agda | 8 ++++---- src/Mugen/Cat/{ => Instances}/Endomorphisms.agda | 4 ++-- src/Mugen/Cat/{ => Instances}/Indexed.agda | 2 +- src/Mugen/Cat/{ => Instances}/StrictOrders.agda | 2 +- src/Mugen/Everything.agda | 6 +++--- src/Mugen/Order/Instances/Endomorphism.agda | 2 +- 12 files changed, 22 insertions(+), 29 deletions(-) rename src/Mugen/Cat/{ => Instances}/Endomorphisms.agda (85%) rename src/Mugen/Cat/{ => Instances}/Indexed.agda (92%) rename src/Mugen/Cat/{ => Instances}/StrictOrders.agda (96%) 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