From 85ff9dc7c527d2df302b925c703c9d503af147d0 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Sun, 2 Jun 2024 06:43:55 -0500
Subject: [PATCH] feat: define the category of displacement algebras

---
 src/Mugen/Algebra/Displacement.agda           | 20 +++++++++++--
 .../Algebra/Displacement/Subalgebra.agda      | 10 +++----
 src/Mugen/Algebra/OrderedMonoid.agda          | 30 +++----------------
 src/Mugen/Cat/Instances/Displacements.agda    | 24 +++++++++++++++
 src/Mugen/Everything.agda                     |  1 +
 src/Mugen/Order/StrictOrder.agda              |  6 ++--
 6 files changed, 54 insertions(+), 37 deletions(-)
 create mode 100644 src/Mugen/Cat/Instances/Displacements.agda

diff --git a/src/Mugen/Algebra/Displacement.agda b/src/Mugen/Algebra/Displacement.agda
index 329494a..aabcc09 100644
--- a/src/Mugen/Algebra/Displacement.agda
+++ b/src/Mugen/Algebra/Displacement.agda
@@ -89,16 +89,30 @@ module _
       Π-is-hlevel' 1 λ _ → Π-is-hlevel' 1 λ _ → B.Ob-is-set _ _
       where unquoteDecl eqv = declare-record-iso eqv (quote is-displacement-hom)
 
-displacement-hom-∘
+abstract instance
+  H-Level-is-displacement : ∀ {n}
+    {A : Poset o r} {B : Poset o' r'}
+    {X : Displacement-on A} {Y : Displacement-on B}
+    {f : Strictly-monotone A B} →
+    H-Level (is-displacement-hom X Y f) (suc n)
+  H-Level-is-displacement {X = X} {Y} {f} = prop-instance (is-displacement-hom-is-prop X Y f)
+
+id-is-displacement-hom
+  : {A : Poset o r} (X : Displacement-on A)
+  → is-displacement-hom X X strictly-monotone-id
+id-is-displacement-hom X .is-displacement-hom.pres-ε = refl
+id-is-displacement-hom X .is-displacement-hom.pres-⊗ = refl
+
+∘-is-displacement-hom
   : {A : Poset o r} {B : Poset o' r'} {C : Poset o'' r''}
   {X : Displacement-on A} {Y : Displacement-on B} {Z : Displacement-on C}
   {f : Strictly-monotone B C} {g : Strictly-monotone A B}
   → is-displacement-hom Y Z f
   → is-displacement-hom X Y g
   → is-displacement-hom X Z (strictly-monotone-∘ f g)
-displacement-hom-∘ {f = f} f-disp g-disp .is-displacement-hom.pres-ε =
+∘-is-displacement-hom {f = f} f-disp g-disp .is-displacement-hom.pres-ε =
   ap# f (g-disp .is-displacement-hom.pres-ε) ∙ f-disp .is-displacement-hom.pres-ε
-displacement-hom-∘ {f = f} {g = g} f-disp g-disp .is-displacement-hom.pres-⊗ {x} {y} =
+∘-is-displacement-hom {f = f} {g = g} f-disp g-disp .is-displacement-hom.pres-⊗ {x} {y} =
   ap# f (g-disp .is-displacement-hom.pres-⊗ {x} {y}) ∙ f-disp .is-displacement-hom.pres-⊗ {g # x} {g # y}
 
 --------------------------------------------------------------------------------
diff --git a/src/Mugen/Algebra/Displacement/Subalgebra.agda b/src/Mugen/Algebra/Displacement/Subalgebra.agda
index 1ec2be0..0130067 100644
--- a/src/Mugen/Algebra/Displacement/Subalgebra.agda
+++ b/src/Mugen/Algebra/Displacement/Subalgebra.agda
@@ -33,15 +33,15 @@ module _
   where
   open is-full-subdisplacement
 
-  full-subdisplacement-∘
+  ∘-is-full-subdisplacement
     : {f : Strictly-monotone B C} {g : Strictly-monotone A B}
     → is-full-subdisplacement Y Z f
     → is-full-subdisplacement X Y g
     → is-full-subdisplacement X Z (strictly-monotone-∘ f g)
-  full-subdisplacement-∘ {f = f} {g = g} f-sub g-sub .has-is-full-subposet =
-    full-subposet-∘ (f-sub .has-is-full-subposet) (g-sub .has-is-full-subposet)
-  full-subdisplacement-∘ {f = f} {g = g} f-sub g-sub .has-is-displacement-hom =
-    displacement-hom-∘ (f-sub .has-is-displacement-hom) (g-sub .has-is-displacement-hom)
+  ∘-is-full-subdisplacement {f = f} {g = g} f-sub g-sub .has-is-full-subposet =
+    ∘-is-full-subposet (f-sub .has-is-full-subposet) (g-sub .has-is-full-subposet)
+  ∘-is-full-subdisplacement {f = f} {g = g} f-sub g-sub .has-is-displacement-hom =
+    ∘-is-displacement-hom (f-sub .has-is-displacement-hom) (g-sub .has-is-displacement-hom)
 
 --------------------------------------------------------------------------------
 -- Builders for Subalgebras
diff --git a/src/Mugen/Algebra/OrderedMonoid.agda b/src/Mugen/Algebra/OrderedMonoid.agda
index 856a803..bea5e88 100644
--- a/src/Mugen/Algebra/OrderedMonoid.agda
+++ b/src/Mugen/Algebra/OrderedMonoid.agda
@@ -40,41 +40,19 @@ record Ordered-monoid-on {o r : Level} (A : Poset o r) : Type (o ⊔ lsuc r) whe
 
   open is-ordered-monoid has-ordered-monoid public
 
-record Ordered-monoid (o r : Level) : Type (lsuc (o ⊔ r)) where
-  field
-    poset : Poset o r
-    ordered-monoid : Ordered-monoid-on poset
-
-  open Poset poset public
-  open Ordered-monoid-on ordered-monoid hiding (has-is-set) public
-
-instance
-  Underlying-ordered-monoid : ∀ {o r} → Underlying (Ordered-monoid o r)
-  Underlying-ordered-monoid .Underlying.ℓ-underlying = _
-  Underlying.⌞ Underlying-ordered-monoid ⌟ M = ⌞ Ordered-monoid.poset M ⌟
-
 --------------------------------------------------------------------------------
 -- Ordered Monoid Actions
 
 record is-right-ordered-monoid-action
-  {o r o′ r′} (A : Poset o r) (B : Ordered-monoid o′ r′)
+  {o r o′ r′} (A : Poset o r) {B : Poset o′ r′} (M : Ordered-monoid-on B)
   (α : ⌞ A ⌟ → ⌞ B ⌟ → ⌞ A ⌟)
   : Type (o ⊔ r ⊔ o′ ⊔ r′)
   where
   no-eta-equality
   private
     module A = Poset A
-    module B = Ordered-monoid B
+    module M = Ordered-monoid-on M
   field
-    identity : ∀ (a : ⌞ A ⌟) → α a B.ε ≡ a
-    compat : ∀ (a : ⌞ A ⌟) (x y : ⌞ B ⌟) → α (α a x) y ≡ α a (x B.⊗ y)
+    identity : ∀ (a : ⌞ A ⌟) → α a M.ε ≡ a
+    compat : ∀ (a : ⌞ A ⌟) (x y : ⌞ B ⌟) → α (α a x) y ≡ α a (x M.⊗ y)
     invariant : ∀ (a b : ⌞ A ⌟) (x : ⌞ B ⌟) → a A.≤ b → α a x A.≤ α b x
-
-record Right-ordered-monoid-action
-  {o o' r r'} (A : Poset o r) (B : Ordered-monoid o' r')
-  : Type (o ⊔ o' ⊔ r ⊔ r')
-  where
-  no-eta-equality
-  field
-    hom : ⌞ A ⌟ → ⌞ B ⌟ → ⌞ A ⌟
-    has-is-action : is-right-ordered-monoid-action A B hom
diff --git a/src/Mugen/Cat/Instances/Displacements.agda b/src/Mugen/Cat/Instances/Displacements.agda
new file mode 100644
index 0000000..ab78c05
--- /dev/null
+++ b/src/Mugen/Cat/Instances/Displacements.agda
@@ -0,0 +1,24 @@
+module Mugen.Cat.Instances.Displacements where
+
+open import Cat.Displayed.Base
+open import Cat.Displayed.Total
+
+open import Mugen.Prelude
+open import Mugen.Algebra.Displacement
+open import Mugen.Cat.Instances.StrictOrders
+
+--------------------------------------------------------------------------------
+-- The Category of Displacement Algebras
+
+Displacements-over : ∀ (o r : Level) → Displayed (Strict-orders o r) (o ⊔ lsuc r) o
+Displacements-over o r .Displayed.Ob[_] A = Displacement-on A
+Displacements-over o r .Displayed.Hom[_] f X Y = is-displacement-hom X Y f
+Displacements-over o r .Displayed.Hom[_]-set f X Y = hlevel 2
+Displacements-over o r .Displayed.id' = id-is-displacement-hom _
+Displacements-over o r .Displayed._∘'_ = ∘-is-displacement-hom
+Displacements-over o r .Displayed.idr' _ = prop!
+Displacements-over o r .Displayed.idl' _ = prop!
+Displacements-over o r .Displayed.assoc' _ _ _ = prop!
+
+Displacements : ∀ o r → Precategory (lsuc o ⊔ lsuc r) (o ⊔ r)
+Displacements o r = ∫ (Displacements-over o r)
diff --git a/src/Mugen/Everything.agda b/src/Mugen/Everything.agda
index 1d5434b..a750b07 100644
--- a/src/Mugen/Everything.agda
+++ b/src/Mugen/Everything.agda
@@ -27,6 +27,7 @@ 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.Instances.Displacements
 import Mugen.Cat.Instances.Endomorphisms
 import Mugen.Cat.Instances.Indexed
 import Mugen.Cat.Instances.StrictOrders
diff --git a/src/Mugen/Order/StrictOrder.agda b/src/Mugen/Order/StrictOrder.agda
index 348c77c..2e01995 100644
--- a/src/Mugen/Order/StrictOrder.agda
+++ b/src/Mugen/Order/StrictOrder.agda
@@ -106,14 +106,14 @@ module _
   where
   open is-full-subposet
 
-  full-subposet-∘
+  ∘-is-full-subposet
     : {f : Strictly-monotone B C} {g : Strictly-monotone A B}
     → is-full-subposet f
     → is-full-subposet g
     → is-full-subposet (strictly-monotone-∘ f g)
-  full-subposet-∘ {f = f} {g = g} f-sub g-sub .is-full-subposet.injective =
+  ∘-is-full-subposet {f = f} {g = g} f-sub g-sub .is-full-subposet.injective =
     g-sub .is-full-subposet.injective ⊙ f-sub .is-full-subposet.injective
-  full-subposet-∘ {f = f} {g = g} f-sub g-sub .is-full-subposet.full =
+  ∘-is-full-subposet {f = f} {g = g} f-sub g-sub .is-full-subposet.full =
     g-sub .is-full-subposet.full ⊙ f-sub .is-full-subposet.full
 
 --------------------------------------------------------------------------------