style: reorganize Cat.HierarchyTheory and update documentation (#42)

RedPRL · Nov 28, 2023 · f134d5c · f134d5c
1 parent b884ba9
commit f134d5c
Show file tree

Hide file tree

Showing 4 changed files with 149 additions and 126 deletions.
diff --git a/README.md b/README.md
@@ -8,28 +8,28 @@ This is a formalization of the displacement algebras, their properties, and part
 
 ### Displacement Algebras
 
-| Displacements                         | Paper Section | Agda Module                                                            | OCaml Module(s)                                                                                                                                                     |
-| :------------------------------------ | :------------ | :--------------------------------------------------------------------- | :------------------------------------------------------------------------------------------------------------------------------------------------------------------ |
-| Natural numbers                       | 3.3.1         | [Nat](src/Mugen/Algebra/Displacement/Nat.agda)                         | [Nat](https://redprl.org/mugen/mugen/Mugen/Shift/Nat) and [Nat](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Nat)                                             |
-| Integers                              | 3.3.1         | [Int](src/Mugen/Algebra/Displacement/Int.agda)                         | [Int](https://redprl.org/mugen/mugen/Mugen/Shift/Int) and [Int](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Int)                                             |
-| Non-positive integers                 | 3.3.1         | [NonPositive](src/Mugen/Algebra/Displacement/NonPositive.agda)         | [NonPositive](https://redprl.org/mugen/mugen/Mugen/Shift/NonPositive) and [NonPositive](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/NonPositive)             |
-| Constant displacements                | 3.3.2         | [Constant](src/Mugen/Algebra/Displacement/Constant.agda)               | [Constant](https://redprl.org/mugen/mugen/Mugen/Shift/Constant)                                                                                                     |
-| Binary products                       | 3.3.3         | [Product](src/Mugen/Algebra/Displacement/Product.agda)                 | [Product](https://redprl.org/mugen/mugen/Mugen/Shift/Product) and [Product](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Product)                             |
-| Lexicographic binary products         | 3.3.4         | [Lexicographic](src/Mugen/Algebra/Displacement/Lexicographic.agda)     | [Lexicographic](https://redprl.org/mugen/mugen/Mugen/Shift/Lexicographic) and [Lexicographic](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Lexicographic)     |
-| Infinite products                     | 3.3.5         | [InfiniteProduct](src/Mugen/Algebra/Displacement/InfiniteProduct.agda) | _(not implementable)_                                                                                                                                               |
-| Nearly constant infinite products     | 3.3.5         | [NearlyConstant](src/Mugen/Algebra/Displacement/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/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/Prefix.agda)                   | [Prefix](https://redprl.org/mugen/mugen/Mugen/Shift/Prefix)                                                                                                         |
-| Fractal displacements                 | 3.3.7         | [Fractal](src/Mugen/Algebra/Displacement/Fractal.agda)                 | [Fractal](https://redprl.org/mugen/mugen/Mugen/Shift/Fractal)                                                                                                       |
-| Opposite displacements                | 3.3.8         | [Opposite](src/Mugen/Algebra/Displacement/Opposite.agda)               | [Opposite](https://redprl.org/mugen/mugen/Mugen/Shift/Opposite)                                                                                                     |
-| Endomorphisms                         | 3.4           | [Endomorphism](src/Mugen/Algebra/Displacement/Endomorphism.agda)       | _(not implementable)_                                                                                                                                               |
+| Displacements                         | Paper Section | Agda Module                                                                         | OCaml Module(s)                                                                                                                                                     |
+| :------------------------------------ | :------------ | :---------------------------------------------------------------------------------- | :------------------------------------------------------------------------------------------------------------------------------------------------------------------ |
+| Natural numbers                       | 3.3.1         | [Nat](src/Mugen/Algebra/Displacement/Nat.agda)                                      | [Nat](https://redprl.org/mugen/mugen/Mugen/Shift/Nat) and [Nat](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Nat)                                             |
+| Integers                              | 3.3.1         | [Int](src/Mugen/Algebra/Displacement/Int.agda)                                      | [Int](https://redprl.org/mugen/mugen/Mugen/Shift/Int) and [Int](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Int)                                             |
+| Non-positive integers                 | 3.3.1         | [NonPositive](src/Mugen/Algebra/Displacement/NonPositive.agda)                      | [NonPositive](https://redprl.org/mugen/mugen/Mugen/Shift/NonPositive) and [NonPositive](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/NonPositive)             |
+| Constant displacements                | 3.3.2         | [Constant](src/Mugen/Algebra/Displacement/Constant.agda)                            | [Constant](https://redprl.org/mugen/mugen/Mugen/Shift/Constant)                                                                                                     |
+| Binary products                       | 3.3.3         | [Product](src/Mugen/Algebra/Displacement/Product.agda)                              | [Product](https://redprl.org/mugen/mugen/Mugen/Shift/Product) and [Product](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Product)                             |
+| Lexicographic binary products         | 3.3.4         | [Lexicographic](src/Mugen/Algebra/Displacement/Lexicographic.agda)                  | [Lexicographic](https://redprl.org/mugen/mugen/Mugen/Shift/Lexicographic) and [Lexicographic](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Lexicographic)     |
+| Infinite products                     | 3.3.5         | Generalized to [IndexedProduct](src/Mugen/Algebra/Displacement/IndexedProduct.agda) | _(not implementable)_                                                                                                                                               |
+| Nearly constant infinite products     | 3.3.5         | [NearlyConstant](src/Mugen/Algebra/Displacement/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/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/Prefix.agda)                                | [Prefix](https://redprl.org/mugen/mugen/Mugen/Shift/Prefix)                                                                                                         |
+| Fractal displacements                 | 3.3.7         | [Fractal](src/Mugen/Algebra/Displacement/Fractal.agda)                              | [Fractal](https://redprl.org/mugen/mugen/Mugen/Shift/Fractal)                                                                                                       |
+| Opposite displacements                | 3.3.8         | [Opposite](src/Mugen/Algebra/Displacement/Opposite.agda)                            | [Opposite](https://redprl.org/mugen/mugen/Mugen/Shift/Opposite)                                                                                                     |
+| Endomorphisms                         | 3.4           | [Endomorphism](src/Mugen/Algebra/Displacement/Endomorphism.agda)                    | _(not implementable)_                                                                                                                                               |
 
 ### Other Theorems
 
-| Theorems                   | Paper Section | Agda Module                                                                             |
-| :------------------------- | :------------ | :-------------------------------------------------------------------------------------- |
-| Validity of McBride monads | 3.1           | [Mugen.Cat.HierarchyTheory](./src/Mugen/Cat/HierarchyTheory.agda)                       |
-| Embedding of endomorphisms | 3.4           | [Mugen.Cat.HierarchyTheory.Properties](./src/Mugen/Cat/HierarchyTheory/Properties.agda) |
+| Theorems                   | Paper Section | Agda Module                                                                                                     |
+| :------------------------- | :------------ | :-------------------------------------------------------------------------------------------------------------- |
+| Validity of McBride monads | 3.1           | [Mugen.Cat.HierarchyTheory](./src/Mugen/Cat/HierarchyTheory/McBride.agda)                                       |
+| Embedding of endomorphisms | 3.4           | [Mugen.Cat.HierarchyTheory.Properties](./src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda) |
 
 ## Building
 

diff --git a/src/Mugen/Cat/McBrideMonad.agda → src/Mugen/Cat/HierarchyTheory/McBride.agda b/src/Mugen/Cat/McBrideMonad.agda → src/Mugen/Cat/HierarchyTheory/McBride.agda
@@ -1,4 +1,4 @@
-module Mugen.Cat.McBrideMonad where
+module Mugen.Cat.HierarchyTheory.McBride where
 
 open import Cat.Diagram.Monad