Skip to content

Commit

Permalink
feat: the traditional hierarchy theory
Browse files Browse the repository at this point in the history
  • Loading branch information
@favonia
favonia committed Jun 9, 2024
1 parent 78d8251 commit 8f640c3
Show file tree
Hide file tree
Showing 2 changed files with 28 additions and 24 deletions.
33 changes: 17 additions & 16 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,27 +12,28 @@ 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 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)_ |
| 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 (JFP only) | [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

| Theorems | Paper Section | Agda Module |
| :------------------------------------ | :----------------- | :----------------------------------------------------------------------------------------------- |
| Traditional level polymorphism | 2.2 | [Traditional](./src/Mugen/Cat/HierarchyTheory/Traditional.agda) |
| Validity of McBride monads | 3.1 | [McBride](./src/Mugen/Cat/HierarchyTheory/McBride.agda) |
| Embedding of endomorphisms | 3.4 (Lemma 3.8) | [EndomorphismEmbedding](./src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda) |
| Embedding of small hierarchy theories | 3.4 (Lemma 3.9) | [SubcategoryEmbedding](./src/Mugen/Cat/HierarchyTheory/Universality/SubcategoryEmbedding.agda) |
Expand Down
19 changes: 11 additions & 8 deletions src/Mugen/Cat/HierarchyTheory/Traditional.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,9 +14,6 @@ open import Mugen.Cat.HierarchyTheory

import Mugen.Order.Reasoning

private variable
o o' r r' : Level

--------------------------------------------------------------------------------
-- The Traditional Hierarchy Theory

Expand Down Expand Up @@ -47,12 +44,18 @@ module _ {o : Level} where
unit .η L .pres-≤[]-equal l1≤l2 = lift {ℓ = lzero} l1≤l2 , inr-inj
unit .is-natural L L' f = ext λ _ → refl

mult-hom : ∀ (L : Poset o o) → Strictly-monotone (Nat-poset ⊎ᵖ (Nat-poset ⊎ᵖ L)) (Nat-poset ⊎ᵖ L)
mult-hom L .hom (inl n) = inl n
mult-hom L .hom (inr l) = l
mult-hom L .pres-≤[]-equal {inl n1} {inl n2} n1≤n2 = n1≤n2 , ap inl ⊙ inl-inj
mult-hom L .pres-≤[]-equal {inr l1} {inr l2} (lift l1≤l2) = l1≤l2 , ap inr

mult : M F∘ M => M
mult .η L .hom (inl n) = inl n
mult .η L .hom (inr l) = l
mult .η L .pres-≤[]-equal {inl n1} {inl n2} n1≤n2 = n1≤n2 , ap inl ⊙ inl-inj
mult .η L .pres-≤[]-equal {inr l1} {inr l2} (lift l1≤l2) = l1≤l2 , ap inr
mult .is-natural L L' f = ext λ { (inl n) → {! refl !} ; (inr (inl l)) → refl ; (inr (inr _)) → {! refl !} }
mult .η = mult-hom
mult .is-natural L L' f = ext λ where
(inl n) → refl
(inr (inl l)) → refl
(inr (inr _)) → refl

ht : Hierarchy-theory o o
ht .Monad.M = M
Expand Down

0 comments on commit 8f640c3

Please sign in to comment.