diff --git a/README.md b/README.md index bf41216..1c7844d 100644 --- a/README.md +++ b/README.md @@ -12,27 +12,25 @@ This is a formalization of the displacement algebras, their properties, and part 🚧 The links are currently broken. -| Displacements | Paper Section | Agda Module | OCaml Module(s) | -| :------------------------------------ | :-------------- | :----------------------------------------------------------------------------- | :------------------------------------------------------------------------------------------------------------------------------------------------------------------ | -| Natural numbers | 3.3.1 | [Nat](src/Mugen/Algebra/Displacement/Instances/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/Instances/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/Instances/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/Instances/Constant.agda) | [Constant](https://redprl.org/mugen/mugen/Mugen/Shift/Constant) | -| Binary products | 3.3.3 | [Product](src/Mugen/Algebra/Displacement/Instances/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/Instances/Lexicographic.agda) | [Lexicographic](https://redprl.org/mugen/mugen/Mugen/Shift/Lexicographic) and [Lexicographic](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Lexicographic) | -| 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) | -| Fractal displacements | 3.3.7 | [Fractal](src/Mugen/Algebra/Displacement/Instances/Fractal.agda) | [Fractal](https://redprl.org/mugen/mugen/Mugen/Shift/Fractal) | -| Opposite displacements | 3.3.8 | [Opposite](src/Mugen/Algebra/Displacement/Instances/Opposite.agda) | [Opposite](https://redprl.org/mugen/mugen/Mugen/Shift/Opposite) | -| Weird frarctal displacements | 3.3.9 | [WeirdFractal](src/Mugen/Algebra/Displacement/Instances/WeirdFractal.agda) | [Fractal](https://redprl.org/mugen/mugen/Mugen/Shift/Fractal) | -| Endomorphisms | 3.4 (Lemma 3.7) | [Endomorphism](src/Mugen/Algebra/Displacement/Instances/Endomorphism.agda) | _(not implementable)_ | +| Displacements | Paper Section | Agda Module | OCaml Module(s) | +| :------------------------------------ | :------------------ | :----------------------------------------------------------------------------- | :------------------------------------------------------------------------------------------------------------------------------------------------------------------ | +| Natural numbers | 3.3.1 | [Nat](src/Mugen/Algebra/Displacement/Instances/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/Instances/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/Instances/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/Instances/Constant.agda) | [Constant](https://redprl.org/mugen/mugen/Mugen/Shift/Constant) | +| Binary products | 3.3.3 | [Product](src/Mugen/Algebra/Displacement/Instances/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/Instances/Lexicographic.agda) | [Lexicographic](https://redprl.org/mugen/mugen/Mugen/Shift/Lexicographic) and [Lexicographic](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Lexicographic) | +| 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) | +| Fractal displacements | 3.3.7 | [Fractal](src/Mugen/Algebra/Displacement/Instances/Fractal.agda) | [Fractal](https://redprl.org/mugen/mugen/Mugen/Shift/Fractal) | +| Opposite displacements | 3.3.8 | [Opposite](src/Mugen/Algebra/Displacement/Instances/Opposite.agda) | [Opposite](https://redprl.org/mugen/mugen/Mugen/Shift/Opposite) | +| Weird fractal displacements | 3.3.9 (not in POPL) | [WeirdFractal](src/Mugen/Algebra/Displacement/Instances/WeirdFractal.agda) | [Fractal](https://redprl.org/mugen/mugen/Mugen/Shift/Fractal) | +| Endomorphisms | 3.4 (Lemma 3.7) | [Endomorphism](src/Mugen/Algebra/Displacement/Instances/Endomorphism.agda) | _(not implementable)_ | ### Other Theorems -🚧 The links are currently broken. - | Theorems | Paper Section | Agda Module | | :------------------------------------ | :----------------- | :----------------------------------------------------------------------------------------------- | | Validity of McBride monads | 3.1 | [McBride](./src/Mugen/Cat/HierarchyTheory/McBride.agda) |