fix: rename Prefix to LexicalList

Author: favonia

README.md

@@ -23,7 +23,7 @@ This is a formalization of the displacement algebras, their properties, and part
 | Indexed products                      | 3.3.5           | [IndexedProduct](src/Mugen/Algebra/Displacement/Instances/IndexedProduct.agda) | _(not implementable)_                                                                                                                                               |
 | Nearly constant infinite products     | 3.3.5           | [NearlyConstant](src/Mugen/Algebra/Displacement/Instances/NearlyConstant.agda) | [NearlyConstant](https://redprl.org/mugen/mugen/Mugen/Shift/NearlyConstant) and [NearlyConstant](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/NearlyConstant) |
 | Infinite products with finite support | 3.3.5           | [FiniteSupport](src/Mugen/Algebra/Displacement/Instances/FiniteSupport.agda)   | [FiniteSupport](https://redprl.org/mugen/mugen/Mugen/Shift/FiniteSupport) and [FiniteSupport](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/FiniteSupport)     |
-| Prefix order                          | 3.3.6           | [Prefix](src/Mugen/Algebra/Displacement/Instances/Prefix.agda)                 | [Prefix](https://redprl.org/mugen/mugen/Mugen/Shift/Prefix)                                                                                                         |
+| Lexical lists                         | 3.3.6           | [LexicalList](src/Mugen/Algebra/Displacement/Instances/LexicalList.agda)       | [Lexicographic](https://redprl.org/mugen/mugen/Mugen/Shift/Lexicographic)                                                                                          |
 | Opposite displacements                | 3.3.8           | [Opposite](src/Mugen/Algebra/Displacement/Instances/Opposite.agda)             | [Opposite](https://redprl.org/mugen/mugen/Mugen/Shift/Opposite)                                                                                                     |
 | Endomorphisms                         | 3.4 (Lemma 3.7) | [Endomorphism](src/Mugen/Algebra/Displacement/Instances/Endomorphism.agda)     | _(not implementable)_                                                                                                                                               |
 

…gebra/Displacement/Instances/Prefix.agda …/Displacement/Instances/LexicalList.agdasrc/Mugen/Algebra/Displacement/Instances/Prefix.agda renamed to src/Mugen/Algebra/Displacement/Instances/LexicalList.agda src/Mugen/Algebra/Displacement/Instances/Prefix.agda renamed to src/Mugen/Algebra/Displacement/Instances/LexicalList.agda

@@ -14,12 +14,12 @@ import Mugen.Order.Reasoning as Reasoning
 import Mugen.Order.Instances.LexicalList as LexicalList
 
 --------------------------------------------------------------------------------
--- Prefix Displacements
+-- Lexical List Displacements
 -- Section 3.3.6
 --
 -- Given a poset 'A', we can define a displacement algebra on lexicographical lists over 'A'.
 
-module Mugen.Algebra.Displacement.Instances.Prefix {o r} (A : Poset o r) where
+module Mugen.Algebra.Displacement.Instances.LexicalList {o r} (A : Poset o r) where
 
 private
   module A = Reasoning A
@@ -34,9 +34,9 @@ private
   ++-left-invariant [] ys zs ys≤zs = ys≤zs
   ++-left-invariant (x ∷ xs) ys zs ys≤zs = A.≤-refl L.∷≤ (λ _ → ++-left-invariant xs ys zs ys≤zs)
 
--- Most of the order theoretic properties come from 'Mugen.Order.Instances.Prefix'.
-Prefix : Displacement-on L.poset
-Prefix = to-displacement-on displacement where
+-- Most of the order theoretic properties come from 'Mugen.Order.Instances.LexicalList'.
+LexicalList : Displacement-on L.poset
+LexicalList = to-displacement-on displacement where
   displacement : make-displacement L.poset
   displacement .make-displacement.ε = []
   displacement .make-displacement._⊗_ = _++_

src/Mugen/Everything.agda

@@ -9,12 +9,12 @@ import Mugen.Algebra.Displacement.Instances.Constant
 import Mugen.Algebra.Displacement.Instances.Endomorphism
 import Mugen.Algebra.Displacement.Instances.IndexedProduct
 import Mugen.Algebra.Displacement.Instances.Int
+import Mugen.Algebra.Displacement.Instances.LexicalList
 import Mugen.Algebra.Displacement.Instances.LexicalProduct
 import Mugen.Algebra.Displacement.Instances.Nat
 import Mugen.Algebra.Displacement.Instances.NearlyConstant
 import Mugen.Algebra.Displacement.Instances.NonPositive
 import Mugen.Algebra.Displacement.Instances.Opposite
-import Mugen.Algebra.Displacement.Instances.Prefix
 import Mugen.Algebra.Displacement.Instances.Product
 import Mugen.Algebra.Displacement.Instances.Support
 import Mugen.Algebra.Displacement.Subalgebra