Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: formalize the "Traditional" universe polymorphism #55

Merged
merged 2 commits into from
Jun 9, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 17 additions & 16 deletions README.md
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
66 changes: 66 additions & 0 deletions src/Mugen/Cat/HierarchyTheory/Traditional.agda
Original file line number Diff line number Diff line change
@@ -0,0 +1,66 @@
module Mugen.Cat.HierarchyTheory.Traditional where

open import Cat.Diagram.Monad

open import Order.Instances.Nat
open import Order.Instances.Coproduct

open import Mugen.Prelude
open import Mugen.Algebra.Displacement
open import Mugen.Order.Instances.LeftInvariantRightCentered
open import Mugen.Order.StrictOrder
open import Mugen.Cat.Instances.StrictOrders
open import Mugen.Cat.HierarchyTheory

import Mugen.Order.Reasoning

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

module _ {o : Level} where
open Strictly-monotone
open Functor
open _=>_

Traditional : Hierarchy-theory o o
Traditional = ht where
M : Functor (Strict-orders o o) (Strict-orders o o)
M .F₀ L = Nat-poset ⊎ᵖ L
M .F₁ f .hom (inl n) = inl n
M .F₁ f .hom (inr l) = inr (f .hom l)
M .F₁ {L} {N} f .pres-≤[]-equal {inl n1} {inl n2} n1≤n2 = n1≤n2 , ap inl ⊙ inl-inj
M .F₁ {L} {N} f .pres-≤[]-equal {inr l1} {inr l2} (lift l1≤l2) =
lift {ℓ = lzero} (Strictly-monotone.pres-≤ f l1≤l2) ,
λ eq → ap inr $ Strictly-monotone.injective-on-related f l1≤l2 $ inr-inj eq
M .F-id = ext λ where
(inl n) → refl
(inr l) → refl
M .F-∘ f g = ext λ where
(inl n) → refl
(inr l) → refl

unit : Id => M
unit .η L .hom l = inr l
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 .η = 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
ht .Monad.unit = unit
ht .Monad.mult = mult
ht .Monad.left-ident = ext λ { (inl n) → refl ; (inr l) → refl }
ht .Monad.right-ident = ext λ { (inl n) → refl ; (inr l) → refl }
ht .Monad.mult-assoc = ext λ { (inl n) → refl ; (inr l) → refl }
1 change: 1 addition & 0 deletions src/Mugen/Everything.agda
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ import Mugen.Algebra.Displacement.Subalgebra
import Mugen.Algebra.OrderedMonoid
import Mugen.Cat.HierarchyTheory
import Mugen.Cat.HierarchyTheory.McBride
import Mugen.Cat.HierarchyTheory.Traditional
import Mugen.Cat.HierarchyTheory.Universality
import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding
import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality
Expand Down