diff --git a/Dockerfile b/Dockerfile index 2e52a31..4650bf7 100644 --- a/Dockerfile +++ b/Dockerfile @@ -31,7 +31,7 @@ FROM alpine AS onelab RUN apk add --no-cache git WORKDIR /dist/1lab -ARG ONELAB_VERSION=ab2c18bb879a9944dac6e0ba61c662197a7f1965 +ARG ONELAB_VERSION=497ac8cf0c2a5c44b355c0d4de58dffa5b919ae2 RUN \ git init && \ git remote add origin https://github.com/plt-amy/1lab && \ diff --git a/src/Mugen/Algebra/Displacement.agda b/src/Mugen/Algebra/Displacement.agda index 61271ff..329494a 100644 --- a/src/Mugen/Algebra/Displacement.agda +++ b/src/Mugen/Algebra/Displacement.agda @@ -6,14 +6,12 @@ open import Algebra.Semigroup open import Mugen.Prelude open import Mugen.Algebra.OrderedMonoid -open import Mugen.Order.Poset - -import Mugen.Data.Nat as Nat +open import Mugen.Order.StrictOrder +import Mugen.Order.Reasoning as Reasoning private variable - o r o' r' : Level - A : Type o + o o' o'' r r' r'' : Level -------------------------------------------------------------------------------- -- Displacement Algebras @@ -21,13 +19,13 @@ private variable -- Like ordered monoids, we view displacement algebras as structures -- over an order. -record is-displacement-algebra - {o r} (A : Poset o r) +record is-displacement + (A : Poset o r) (ε : ⌞ A ⌟) (_⊗_ : ⌞ A ⌟ → ⌞ A ⌟ → ⌞ A ⌟) : Type (o ⊔ r) where no-eta-equality - open Poset A + open Reasoning A field has-is-monoid : is-monoid ε _⊗_ @@ -41,406 +39,125 @@ record is-displacement-algebra -- -- Note: we did not /prove/ that the naive formulation is not -- constructively working. - left-strict-invariant : ∀ {x y z} → y ≤ z - → ((x ⊗ y) ≤ (x ⊗ z)) × ((x ⊗ y) ≡ (x ⊗ z) → y ≡ z) + left-strict-invariant : ∀ {x y z} → y ≤ z → (x ⊗ y) ≤[ y ≡ z ] (x ⊗ z) abstract left-invariant : ∀ {x y z} → y ≤ z → (x ⊗ y) ≤ (x ⊗ z) - left-invariant y≤z = fst $ left-strict-invariant y≤z + left-invariant y≤z = left-strict-invariant y≤z .fst - injr-on-related : ∀ {x y z} → y ≤ z → (x ⊗ y) ≡ (x ⊗ z) → y ≡ z - injr-on-related y≤z = snd $ left-strict-invariant y≤z + injectiver-on-related : ∀ {x y z} → y ≤ z → (x ⊗ y) ≡ (x ⊗ z) → y ≡ z + injectiver-on-related y≤z = left-strict-invariant y≤z .snd open is-monoid has-is-monoid hiding (has-is-set) public -record Displacement-algebra-on - {o r : Level} (A : Poset o r) - : Type (o ⊔ lsuc r) - where +record Displacement-on (A : Poset o r) : Type (o ⊔ lsuc r) where field ε : ⌞ A ⌟ _⊗_ : ⌞ A ⌟ → ⌞ A ⌟ → ⌞ A ⌟ - has-is-displacement-algebra : is-displacement-algebra A ε _⊗_ - - open is-displacement-algebra has-is-displacement-algebra public - -record Displacement-algebra (o r : Level) : Type (lsuc (o ⊔ r)) where - no-eta-equality - field - poset : Poset o r - displacement-algebra-on : Displacement-algebra-on poset + has-is-displacement : is-displacement A ε _⊗_ - open Poset poset public - open Displacement-algebra-on displacement-algebra-on public - -instance - Underlying-displacement-algebra : ∀ {o r} → Underlying (Displacement-algebra o r) - Underlying-displacement-algebra .Underlying.ℓ-underlying = _ - Underlying.⌞ Underlying-displacement-algebra ⌟ D = ⌞ Displacement-algebra.poset D ⌟ - -private - variable - X Y Z : Displacement-algebra o r + open is-displacement has-is-displacement public -------------------------------------------------------------------------------- -- Homomorphisms of Displacement Algebras module _ - {o o' r r'} - (X : Displacement-algebra o r) (Y : Displacement-algebra o' r') + {A : Poset o r} {B : Poset o' r'} + (X : Displacement-on A) (Y : Displacement-on B) where + private - module X = Displacement-algebra X - module Y = Displacement-algebra Y + module A = Reasoning A + module B = Reasoning B + module X = Displacement-on X + module Y = Displacement-on Y - record is-displacement-algebra-hom - (f : Strictly-monotone X.poset Y.poset) - : Type (o ⊔ o') - where + record is-displacement-hom (f : Strictly-monotone A B) : Type (o ⊔ o') where no-eta-equality open Strictly-monotone f field pres-ε : hom X.ε ≡ Y.ε - pres-⊗ : ∀ (x y : ⌞ X ⌟) → hom (x X.⊗ y) ≡ (hom x Y.⊗ hom y) - - is-displacement-algebra-hom-is-prop - : (f : Strictly-monotone X.poset Y.poset) - → is-prop (is-displacement-algebra-hom f) - is-displacement-algebra-hom-is-prop f = - Iso→is-hlevel 1 eqv $ - Σ-is-hlevel 1 (Y.has-is-set _ _) λ _ → - Π-is-hlevel² 1 λ _ _ → Y.has-is-set _ _ - where unquoteDecl eqv = declare-record-iso eqv (quote is-displacement-algebra-hom) - - record Displacement-algebra-hom : Type (o ⊔ o' ⊔ r ⊔ r') where - no-eta-equality - field - strict-hom : Strictly-monotone X.poset Y.poset - has-is-displacement-hom : is-displacement-algebra-hom strict-hom - - open Strictly-monotone strict-hom public - open is-displacement-algebra-hom has-is-displacement-hom public + pres-⊗ : ∀ {x y : ⌞ A ⌟} → hom (x X.⊗ y) ≡ (hom x Y.⊗ hom y) -Displacement-algebra-hom-path - : ∀ {o r o' r'} - → {X : Displacement-algebra o r} {Y : Displacement-algebra o' r'} - → (f g : Displacement-algebra-hom X Y) - → f .Displacement-algebra-hom.strict-hom ≡ g .Displacement-algebra-hom.strict-hom - → f ≡ g -Displacement-algebra-hom-path f g p i .Displacement-algebra-hom.strict-hom = p i -Displacement-algebra-hom-path {X = X} {Y = Y} f g p i .Displacement-algebra-hom.has-is-displacement-hom = - is-prop→pathp - (λ i → is-displacement-algebra-hom-is-prop X Y (p i)) - (f .Displacement-algebra-hom.has-is-displacement-hom) - (g .Displacement-algebra-hom.has-is-displacement-hom) i - -instance - Funlike-displacement-algebra-hom - : ∀ {o r o' r'} - → Funlike (Displacement-algebra-hom {o} {r} {o'} {r'}) - Funlike-displacement-algebra-hom .Funlike.au = Underlying-displacement-algebra - Funlike-displacement-algebra-hom .Funlike.bu = Underlying-displacement-algebra - Funlike-displacement-algebra-hom .Funlike._#_ f x = f .Displacement-algebra-hom.strict-hom # x - -module _ {o r o' r' ℓ} {X : Displacement-algebra o r} {Y : Displacement-algebra o' r'} where - private - module X = Displacement-algebra X - module Y = Displacement-algebra Y - - Extensional-Displacement-algebra-hom - : ∀ ⦃ sa : Extensional (Strictly-monotone X.poset Y.poset) ℓ ⦄ - → Extensional (Displacement-algebra-hom X Y) ℓ - Extensional-Displacement-algebra-hom ⦃ sa ⦄ = - injection→extensional! {f = Displacement-algebra-hom.strict-hom} (Displacement-algebra-hom-path _ _) sa - - instance - extensionality-displacement-algebra-hom : Extensionality (Displacement-algebra-hom X Y) - extensionality-displacement-algebra-hom = record { lemma = quote Extensional-Displacement-algebra-hom } + abstract + is-displacement-hom-is-prop + : (f : Strictly-monotone A B) + → is-prop (is-displacement-hom f) + is-displacement-hom-is-prop f = + Iso→is-hlevel 1 eqv $ + Σ-is-hlevel 1 (B.Ob-is-set _ _) λ _ → + Π-is-hlevel' 1 λ _ → Π-is-hlevel' 1 λ _ → B.Ob-is-set _ _ + where unquoteDecl eqv = declare-record-iso eqv (quote is-displacement-hom) displacement-hom-∘ - : Displacement-algebra-hom Y Z - → Displacement-algebra-hom X Y - → Displacement-algebra-hom X Z -displacement-hom-∘ f g .Displacement-algebra-hom.strict-hom = - strictly-monotone-∘ (f .Displacement-algebra-hom.strict-hom) (g .Displacement-algebra-hom.strict-hom) -displacement-hom-∘ f g .Displacement-algebra-hom.has-is-displacement-hom .is-displacement-algebra-hom.pres-ε = - ap (f #_) (g .Displacement-algebra-hom.pres-ε) ∙ f .Displacement-algebra-hom.pres-ε -displacement-hom-∘ f g .Displacement-algebra-hom.has-is-displacement-hom .is-displacement-algebra-hom.pres-⊗ x y = - ap (f #_) (g .Displacement-algebra-hom.pres-⊗ x y) ∙ f .Displacement-algebra-hom.pres-⊗ (g # x) (g # y) - --------------------------------------------------------------------------------- --- Subalgebras of Displacement Algebras - -record is-displacement-subalgebra - {o r o' r'} - (X : Displacement-algebra o r) - (Y : Displacement-algebra o' r') - : Type (o ⊔ o' ⊔ r ⊔ r') - where - no-eta-equality - field - into : Displacement-algebra-hom X Y - inj : ∀ {x y : ⌞ X ⌟} → into # x ≡ into # y → x ≡ y - - open Displacement-algebra-hom into public - -module _ where - open is-displacement-subalgebra - - is-displacement-subalgebra-trans - : ∀ {o r o' r' o'' r''} - {X : Displacement-algebra o r} - {Y : Displacement-algebra o' r'} - {Z : Displacement-algebra o'' r''} - → is-displacement-subalgebra X Y - → is-displacement-subalgebra Y Z - → is-displacement-subalgebra X Z - is-displacement-subalgebra-trans f g .into = displacement-hom-∘ (g .into) (f .into) - is-displacement-subalgebra-trans f g .is-displacement-subalgebra.inj p = f .inj (g .inj p) + : {A : Poset o r} {B : Poset o' r'} {C : Poset o'' r''} + {X : Displacement-on A} {Y : Displacement-on B} {Z : Displacement-on C} + {f : Strictly-monotone B C} {g : Strictly-monotone A B} + → is-displacement-hom Y Z f + → is-displacement-hom X Y g + → is-displacement-hom X Z (strictly-monotone-∘ f g) +displacement-hom-∘ {f = f} f-disp g-disp .is-displacement-hom.pres-ε = + ap# f (g-disp .is-displacement-hom.pres-ε) ∙ f-disp .is-displacement-hom.pres-ε +displacement-hom-∘ {f = f} {g = g} f-disp g-disp .is-displacement-hom.pres-⊗ {x} {y} = + ap# f (g-disp .is-displacement-hom.pres-⊗ {x} {y}) ∙ f-disp .is-displacement-hom.pres-⊗ {g # x} {g # y} -------------------------------------------------------------------------------- -- Some Properties of Displacement Algebras module _ - {o r} (A : Poset o r) + (A : Poset o r) {ε : ⌞ A ⌟} {_⊗_ : ⌞ A ⌟ → ⌞ A ⌟ → ⌞ A ⌟} - (D : is-displacement-algebra A ε _⊗_) + (𝒟 : is-displacement A ε _⊗_) where private module A = Poset A - open A using (_≤_) - module D = is-displacement-algebra D + module 𝒟 = is-displacement 𝒟 - is-right-invariant-displacement-algebra→is-ordered-monoid - : (∀ {x y z} → x ≤ y → (x ⊗ z) ≤ (y ⊗ z)) + is-right-invariant-displacement→is-ordered-monoid + : (∀ {x y z} → x A.≤ y → (x ⊗ z) A.≤ (y ⊗ z)) → is-ordered-monoid A ε _⊗_ - is-right-invariant-displacement-algebra→is-ordered-monoid ≤-invariantr = om where + is-right-invariant-displacement→is-ordered-monoid right-invariant = om where om : is-ordered-monoid A ε _⊗_ - om .is-ordered-monoid.has-is-monoid = D.has-is-monoid + om .is-ordered-monoid.has-is-monoid = 𝒟.has-is-monoid om .is-ordered-monoid.invariant w≤y x≤z = - A.≤-trans (≤-invariantr w≤y) (D.left-invariant x≤z) - --------------------------------------------------------------------------------- --- Augmentations of Displacement Algebras - -module _ {o r} (𝒟 : Displacement-algebra o r) where + A.≤-trans (right-invariant w≤y) (𝒟.left-invariant x≤z) - open Displacement-algebra 𝒟 +module _ {A : Poset o r} (𝒟 : Displacement-on A) where + open Reasoning A + open Displacement-on 𝒟 -- Ordered Monoids has-ordered-monoid : Type (o ⊔ r) - has-ordered-monoid = is-ordered-monoid poset ε _⊗_ + has-ordered-monoid = is-ordered-monoid A ε _⊗_ right-invariant→has-ordered-monoid : (∀ {x y z} → x ≤ y → (x ⊗ z) ≤ (y ⊗ z)) → has-ordered-monoid right-invariant→has-ordered-monoid = - is-right-invariant-displacement-algebra→is-ordered-monoid - poset - has-is-displacement-algebra - - -- Joins - record has-joins : Type (o ⊔ r) where - field - join : ⌞ 𝒟 ⌟ → ⌞ 𝒟 ⌟ → ⌞ 𝒟 ⌟ - joinl : ∀ {x y} → x ≤ join x y - joinr : ∀ {x y} → y ≤ join x y - universal : ∀ {x y z} → x ≤ z → y ≤ z → join x y ≤ z - - -- Bottoms - record has-bottom : Type (o ⊔ r) where - field - bot : ⌞ 𝒟 ⌟ - is-bottom : ∀ x → bot ≤ x - --------------------------------------------------------------------------------- --- Subalgebras of Augmented Displacement Algebras - -preserves-joins - : (X-joins : has-joins X) (Y-joins : has-joins Y) - → (f : Displacement-algebra-hom X Y) - → Type _ -preserves-joins {X = X} ⋁X ⋁Y f = - ∀ (x y : ⌞ X ⌟) → f # (⋁X .join x y) ≡ ⋁Y .join (f # x) (f # y) - where - open has-joins - -preserves-bottom - : (X-bot : has-bottom X) (Y-bot : has-bottom Y) - → (f : Displacement-algebra-hom X Y) - → Type _ -preserves-bottom X⊥ Y⊥ f = f # X⊥ .bot ≡ Y⊥ .bot - where - open has-bottom - -record is-displacement-subsemilattice - {X : Displacement-algebra o r} {Y : Displacement-algebra o' r'} - (X-joins : has-joins X) (Y-joins : has-joins Y) - : Type (o ⊔ o' ⊔ r' ⊔ r) - where - field - has-displacement-subalgebra : is-displacement-subalgebra X Y - - open is-displacement-subalgebra has-displacement-subalgebra public - field - pres-joins : preserves-joins X-joins Y-joins into - -record is-bounded-displacement-subalgebra - {X : Displacement-algebra o r} {Y : Displacement-algebra o' r'} - (X-bottom : has-bottom X) (Y-bottom : has-bottom Y) - : Type (o ⊔ o' ⊔ r ⊔ r') where - field - has-displacement-subalgebra : is-displacement-subalgebra X Y - open is-displacement-subalgebra has-displacement-subalgebra public - field - pres-bottom : preserves-bottom X-bottom Y-bottom into - --------------------------------------------------------------------------------- --- Displacement Actions - -module _ - {o r o′ r′} - (A : Poset o r) (B : Displacement-algebra o′ r′) - where - private - module A = Poset A - module B = Displacement-algebra B - - record is-right-displacement-action - (α : ⌞ A ⌟ → ⌞ B ⌟ → ⌞ A ⌟) - : Type (o ⊔ r ⊔ o′ ⊔ r′) - where - no-eta-equality - field - identity : ∀ (a : ⌞ A ⌟) → α a B.ε ≡ a - compat : ∀ (a : ⌞ A ⌟) (x y : ⌞ B ⌟) → α (α a x) y ≡ α a (x B.⊗ y) - strict-invariant : ∀ (a : ⌞ A ⌟) (x y : ⌞ B ⌟) → x B.≤ y → (α a x A.≤ α a y) × (α a x ≡ α a y → x ≡ y) - - abstract - invariant : ∀ (a : ⌞ A ⌟) (x y : ⌞ B ⌟) → x B.≤ y → α a x A.≤ α a y - invariant a x y x≤y = strict-invariant a x y x≤y .fst - - injr-on-related : ∀ (a : ⌞ A ⌟) (x y : ⌞ B ⌟) → x B.≤ y → α a x ≡ α a y → x ≡ y - injr-on-related a x y x≤y = strict-invariant a x y x≤y .snd - - abstract - is-right-displacement-action-is-prop - : (α : ⌞ A ⌟ → ⌞ B ⌟ → ⌞ A ⌟) - → is-prop (is-right-displacement-action α) - is-right-displacement-action-is-prop α = - Iso→is-hlevel 1 eqv $ - Σ-is-hlevel 1 (Π-is-hlevel 1 λ _ → A.has-is-set _ _) λ _ → - Σ-is-hlevel 1 (Π-is-hlevel³ 1 λ _ _ _ → A.has-is-set _ _) λ _ → - Π-is-hlevel³ 1 λ _ _ _ → Π-is-hlevel 1 λ _ → ×-is-hlevel 1 A.≤-thin $ - Π-is-hlevel 1 λ _ → B.has-is-set _ _ - where unquoteDecl eqv = declare-record-iso eqv (quote is-right-displacement-action) - -record Right-displacement-action - {o r o′ r′} - (A : Poset o r) (B : Displacement-algebra o′ r′) - : Type (o ⊔ r ⊔ o′ ⊔ r′) - where - field - hom : ⌞ A ⌟ → ⌞ B ⌟ → ⌞ A ⌟ - has-is-action : is-right-displacement-action A B hom - - open is-right-displacement-action has-is-action public - -module _ where - open Right-displacement-action - - Right-displacement-action-path - : ∀ {o r o′ r′} - → {A : Poset o r} {B : Displacement-algebra o′ r′} - → (α β : Right-displacement-action A B) - → (∀ a b → α .hom a b ≡ β .hom a b) - → α ≡ β - Right-displacement-action-path α β p i .hom a b = p a b i - Right-displacement-action-path α β p i .has-is-action = - is-prop→pathp (λ i → is-right-displacement-action-is-prop _ _ (λ a b → p a b i)) - (α .has-is-action) - (β .has-is-action) i - -instance - Right-actionlike-displacement-action - : ∀ {o r o' r'} - → Right-actionlike (Right-displacement-action {o} {r} {o'} {r'}) - Right-actionlike.⟦ Right-actionlike-displacement-action ⟧ʳ = - Right-displacement-action.hom - Right-actionlike-displacement-action .Right-actionlike.extʳ = - Right-displacement-action-path _ _ + is-right-invariant-displacement→is-ordered-monoid A has-is-displacement -------------------------------------------------------------------------------- -- Builders -record make-displacement-algebra - {o r} (A : Poset o r) - : Type (o ⊔ r) - where +record make-displacement (A : Poset o r) : Type (o ⊔ r) where no-eta-equality - open Poset A + open Reasoning A field ε : ⌞ A ⌟ _⊗_ : ⌞ A ⌟ → ⌞ A ⌟ → ⌞ A ⌟ idl : ∀ {x} → ε ⊗ x ≡ x idr : ∀ {x} → x ⊗ ε ≡ x associative : ∀ {x y z} → x ⊗ (y ⊗ z) ≡ (x ⊗ y) ⊗ z - left-strict-invariant : ∀ {x y z} → y ≤ z - → ((x ⊗ y) ≤ (x ⊗ z)) × ((x ⊗ y) ≡ (x ⊗ z) → y ≡ z) - -module _ where - open Displacement-algebra - open Displacement-algebra-on - open is-displacement-algebra - open make-displacement-algebra - - to-displacement-algebra - : ∀ {o r} {A : Poset o r} - → make-displacement-algebra A - → Displacement-algebra o r - to-displacement-algebra {A = A} mk .poset = A - to-displacement-algebra {A = A} mk .displacement-algebra-on .ε = mk .ε - to-displacement-algebra {A = A} mk .displacement-algebra-on ._⊗_ = mk ._⊗_ - to-displacement-algebra {A = A} mk .displacement-algebra-on .has-is-displacement-algebra .has-is-monoid .has-is-semigroup .has-is-magma .is-magma.has-is-set = Poset.has-is-set A - to-displacement-algebra {A = A} mk .displacement-algebra-on .has-is-displacement-algebra .has-is-monoid .has-is-semigroup .associative = mk .associative - to-displacement-algebra {A = A} mk .displacement-algebra-on .has-is-displacement-algebra .has-is-monoid .idl = mk .idl - to-displacement-algebra {A = A} mk .displacement-algebra-on .has-is-displacement-algebra .has-is-monoid .idr = mk .idr - to-displacement-algebra {A = A} mk .displacement-algebra-on .has-is-displacement-algebra .left-strict-invariant = mk .left-strict-invariant - -record make-displacement-subalgebra - {o r o' r'} - (X : Displacement-algebra o r) - (Y : Displacement-algebra o' r') - : Type (o ⊔ o' ⊔ r ⊔ r') - where - no-eta-equality - private - module X = Displacement-algebra X - module Y = Displacement-algebra Y - field - into : ⌞ X ⌟ → ⌞ Y ⌟ - pres-ε : into X.ε ≡ Y.ε - pres-⊗ : ∀ x y → into (x X.⊗ y) ≡ into x Y.⊗ into y - mono : ∀ x y → x X.≤ y → into x Y.≤ into y - inj : ∀ {x y} → into x ≡ into y → x ≡ y - - strict-mono : ∀ x y → x X.≤ y → (into x Y.≤ into y) × (into x ≡ into y → x ≡ y) - strict-mono x y x≤y = mono x y x≤y , inj - - -module _ where - open is-displacement-algebra-hom - open is-displacement-subalgebra - open make-displacement-subalgebra - open Displacement-algebra-hom - - to-displacement-subalgebra - : ∀ {o r o' r'} - → {X : Displacement-algebra o r} - → {Y : Displacement-algebra o' r'} - → make-displacement-subalgebra X Y - → is-displacement-subalgebra X Y - to-displacement-subalgebra mk .into .strict-hom .Strictly-monotone.hom = mk .into - to-displacement-subalgebra mk .into .strict-hom .Strictly-monotone.strict-mono = - make-displacement-subalgebra.strict-mono mk _ _ - to-displacement-subalgebra mk .into .has-is-displacement-hom .pres-ε = mk .pres-ε - to-displacement-subalgebra mk .into .has-is-displacement-hom .pres-⊗ = mk .pres-⊗ - to-displacement-subalgebra mk .inj = mk .inj + left-strict-invariant : ∀ {x y z} → y ≤ z → (x ⊗ y) ≤[ y ≡ z ] (x ⊗ z) + +module _ {A : Poset o r} where + open Displacement-on + open is-displacement + open make-displacement + + to-displacement-on : make-displacement A → Displacement-on A + to-displacement-on mk .ε = mk .ε + to-displacement-on mk ._⊗_ = mk ._⊗_ + to-displacement-on mk .has-is-displacement .has-is-monoid .has-is-semigroup .has-is-magma .is-magma.has-is-set = Poset.Ob-is-set A + to-displacement-on mk .has-is-displacement .has-is-monoid .has-is-semigroup .associative = mk .associative + to-displacement-on mk .has-is-displacement .has-is-monoid .idl = mk .idl + to-displacement-on mk .has-is-displacement .has-is-monoid .idr = mk .idr + to-displacement-on mk .has-is-displacement .left-strict-invariant = mk .left-strict-invariant diff --git a/src/Mugen/Algebra/Displacement/Action.agda b/src/Mugen/Algebra/Displacement/Action.agda new file mode 100644 index 0000000..c769e90 --- /dev/null +++ b/src/Mugen/Algebra/Displacement/Action.agda @@ -0,0 +1,65 @@ +module Mugen.Algebra.Displacement.Action where + +open import Mugen.Prelude +open import Mugen.Algebra.Displacement + +import Mugen.Order.Reasoning as Reasoning + +-------------------------------------------------------------------------------- +-- Right Displacement Actions + +record Right-displacement-action + {o r o' r'} (A : Poset o r) {B : Poset o' r'} (Y : Displacement-on B) + : Type (o ⊔ r ⊔ o' ⊔ r') + where + private + module A = Reasoning A + module B = Reasoning B + module Y = Displacement-on Y + field + _⋆_ : ⌞ A ⌟ → ⌞ B.Ob ⌟ → ⌞ A ⌟ + identity : ∀ {a} → a ⋆ Y.ε ≡ a + compatible : ∀ {a x y} → a ⋆ (x Y.⊗ y) ≡ (a ⋆ x) ⋆ y + strict-invariant : ∀ {a x y} → x B.≤ y → (a ⋆ x) A.≤[ x ≡ y ] (a ⋆ y) + + abstract + invariant : ∀ {a x y} → x B.≤ y → (a ⋆ x) A.≤ (a ⋆ y) + invariant {a} {x} {y} x≤y = strict-invariant {a} {x} {y} x≤y .fst + + injectiver-on-related : ∀ {a} {x} {y} → x B.≤ y → (a ⋆ x) ≡ (a ⋆ y) → x ≡ y + injectiver-on-related {a} {x} {y} x≤y = strict-invariant {a} {x} {y} x≤y .snd + +module _ where + open Right-displacement-action + + opaque + Right-displacement-action-path + : ∀ {o r o' r'} + → {A : Poset o r} {B : Poset o' r'} {Y : Displacement-on B} + → (α β : Right-displacement-action A Y) + → (∀ {a b} → (α ._⋆_ a b) ≡ (β ._⋆_ a b)) + → α ≡ β + Right-displacement-action-path α β p i ._⋆_ a b = p {a} {b} i + Right-displacement-action-path {A = A} {Y = Y} α β p i .identity {a} = + is-prop→pathp + (λ i → Poset.Ob-is-set A (p {a} {Y .Displacement-on.ε} i) _) + (α .identity {a}) (β .identity {a}) i + Right-displacement-action-path {A = A} {Y = Y} α β p i .compatible {a} {x} {y} = + is-prop→pathp + (λ i → Poset.Ob-is-set A + (p {a} {Y .Displacement-on._⊗_ x y} i) + (p {p {a} {x} i} {y} i)) + (α .compatible {a} {x} {y}) (β .compatible {a} {x} {y}) i + Right-displacement-action-path {A = A} {B = B} α β p i .strict-invariant {a} {x} {y} q = + is-prop→pathp + (λ i → Reasoning.≤[]-is-hlevel A {x = p {a} {x} i} {y = p {a} {y} i} 0 (Poset.Ob-is-set B _ _)) + (α .strict-invariant {a} {x} {y} q) (β .strict-invariant {a} {x} {y} q) i + +instance + Right-actionlike-displacement-action + : ∀ {o r o' r'} + → Right-actionlike (λ A (B : Σ _ Displacement-on) → Right-displacement-action {o} {r} {o'} {r'} A (B .snd)) + Right-actionlike.⟦ Right-actionlike-displacement-action ⟧ʳ = + Right-displacement-action._⋆_ + Right-actionlike-displacement-action .Right-actionlike.extʳ = + Right-displacement-action-path _ _ diff --git a/src/Mugen/Algebra/Displacement/Constant.agda b/src/Mugen/Algebra/Displacement/Constant.agda deleted file mode 100644 index 3326050..0000000 --- a/src/Mugen/Algebra/Displacement/Constant.agda +++ /dev/null @@ -1,126 +0,0 @@ -module Mugen.Algebra.Displacement.Constant where - -open import Algebra.Magma -open import Algebra.Monoid -open import Algebra.Semigroup - -open import Mugen.Prelude hiding (Const) -open import Mugen.Order.Poset -open import Mugen.Order.Coproduct - -open import Mugen.Algebra.Displacement -open import Mugen.Algebra.OrderedMonoid - --------------------------------------------------------------------------------- --- Constant Displacements --- Section 3.3.2 --- --- Given a strict order 'A', a displacement algebra 'B', and a right displacement --- action 'α : A → B → A', we can construct a displacement algebra whose carrier --- is 'A ⊎ B'. Multiplication of an 'inl a' and 'inr b' uses the 'α' to have --- 'b' act upon 'a'. - -module Constant - {o r} {A : Poset o r} {B : Displacement-algebra o r} - (α : Right-displacement-action A B) where - private - module A = Poset A - module B = Displacement-algebra B - module α = Right-displacement-action α - open Poset-coproduct A B.poset - - _⊗α_ : ⌞ A ⌟ ⊎ ⌞ B ⌟ → ⌞ A ⌟ ⊎ ⌞ B ⌟ → ⌞ A ⌟ ⊎ ⌞ B ⌟ - _ ⊗α inl a = inl a - inl a ⊗α inr x = inl (⟦ α ⟧ʳ a x) - inr x ⊗α inr y = inr (x B.⊗ y) - - εα : ⌞ A ⌟ ⊎ ⌞ B ⌟ - εα = inr B.ε - - ⊗α-associative : ∀ (x y z : ⌞ A ⌟ ⊎ ⌞ B ⌟) → (x ⊗α (y ⊗α z)) ≡ ((x ⊗α y) ⊗α z) - ⊗α-associative _ _ (inl _) = refl - ⊗α-associative _ (inl _) (inr _) = refl - ⊗α-associative (inl a) (inr y) (inr z) = ap inl (sym (α.compat a y z)) - ⊗α-associative (inr x) (inr y) (inr z) = ap inr B.associative - - ⊗α-idl : ∀ (x : ⌞ A ⌟ ⊎ ⌞ B ⌟) → (εα ⊗α x) ≡ x - ⊗α-idl (inl x) = refl - ⊗α-idl (inr x) = ap inr B.idl - - ⊗α-idr : ∀ (x : ⌞ A ⌟ ⊎ ⌞ B ⌟) → (x ⊗α εα) ≡ x - ⊗α-idr (inl x) = ap inl (α.identity x) - ⊗α-idr (inr x) = ap inr B.idr - - -------------------------------------------------------------------------------- - -- Ordering - -- - -- This uses the coproduct of strict orders, so we can re-use proofs from there. - - _≤α_ : ⌞ A ⌟ ⊎ ⌞ B ⌟ → ⌞ A ⌟ ⊎ ⌞ B ⌟ → Type r - x ≤α y = x ⊕≤ y - - _<α_ : ⌞ A ⌟ ⊎ ⌞ B ⌟ → ⌞ A ⌟ ⊎ ⌞ B ⌟ → Type (o ⊔ r) - _<α_ = strict _≤α_ - - -------------------------------------------------------------------------------- - -- Left Invariance - - ⊗α-left-invariant : ∀ (x y z : ⌞ A ⌟ ⊎ ⌞ B ⌟) → y ≤α z → (x ⊗α y) ≤α (x ⊗α z) - ⊗α-left-invariant _ (inl y) (inl z) y≤z = y≤z - ⊗α-left-invariant (inl x) (inr y) (inr z) y≤z = α.invariant x y z y≤z - ⊗α-left-invariant (inr x) (inr y) (inr z) y≤z = B.left-invariant y≤z - - ⊗α-injr-on-≤α : ∀ (x y z : ⌞ A ⌟ ⊎ ⌞ B ⌟) → y ≤α z → (x ⊗α y) ≡ (x ⊗α z) → y ≡ z - ⊗α-injr-on-≤α _ (inl y) (inl z) _ p = p - ⊗α-injr-on-≤α (inl x) (inr y) (inr z) y≤z p = - ap inr $ α.injr-on-related x y z y≤z (inl-inj p) - ⊗α-injr-on-≤α (inr x) (inr y) (inr z) y≤z p = - ap inr $ B.injr-on-related y≤z (inr-inj p) - -Const - : ∀ {o r} {A : Poset o r} {B : Displacement-algebra o r} - → Right-displacement-action A B - → Displacement-algebra o r -Const {A = A} {B = B} α = to-displacement-algebra mk where - module A = Poset A - module B = Displacement-algebra B - open Constant α - open make-displacement-algebra - - mk : make-displacement-algebra (A ⊕ B.poset) - mk .ε = εα - mk ._⊗_ = _⊗α_ - mk .idl {x} = ⊗α-idl x - mk .idr {x} = ⊗α-idr x - mk .associative {x} {y} {z} = ⊗α-associative x y z - mk .left-strict-invariant {x} {y} {z} p = - ⊗α-left-invariant x y z p , ⊗α-injr-on-≤α x y z p - -module ConstantProperties - {o r} - {A : Poset o r} {B : Displacement-algebra o r} - (α : Right-displacement-action A B) where - private - module A = Poset A - module B = Displacement-algebra B - open Poset-coproduct A B.poset - open B using (ε; _⊗_) - - -------------------------------------------------------------------------------- - -- Ordered Monoid - - ⊗α-is-ordered-monoid - : has-ordered-monoid B - → (∀ {x y : ⌞ A ⌟} {z : ⌞ B ⌟} → x A.≤ y → ⟦ α ⟧ʳ x z A.≤ ⟦ α ⟧ʳ y z) - → has-ordered-monoid (Const α) - ⊗α-is-ordered-monoid B-ordered-monoid α-right-invariant = - right-invariant→has-ordered-monoid (Const α) λ {x} {y} {z} x≤y → - ≤α-right-invariant x y z x≤y - where - open Constant α - module B-ordered-monoid = is-ordered-monoid (B-ordered-monoid) - - ≤α-right-invariant : ∀ x y z → x ≤α y → (x ⊗α z) ≤α (y ⊗α z) - ≤α-right-invariant x y (inl z) x≤y = ⊕≤-refl (inl z) - ≤α-right-invariant (inl x) (inl y) (inr z) x≤y = α-right-invariant x≤y - ≤α-right-invariant (inr x) (inr y) (inr z) x≤y = B-ordered-monoid.right-invariant x≤y diff --git a/src/Mugen/Algebra/Displacement/Endomorphism.agda b/src/Mugen/Algebra/Displacement/Endomorphism.agda deleted file mode 100644 index 4555dae..0000000 --- a/src/Mugen/Algebra/Displacement/Endomorphism.agda +++ /dev/null @@ -1,126 +0,0 @@ --- vim: nowrap -module Mugen.Algebra.Displacement.Endomorphism where - -open import Algebra.Magma -open import Algebra.Monoid renaming (idl to ⊗-idl; idr to ⊗-idr) -open import Algebra.Semigroup - -open import Cat.Diagram.Monad -import Cat.Reasoning as Cat - -open import Mugen.Prelude -open import Mugen.Data.NonEmpty - -open import Mugen.Algebra.Displacement -open import Mugen.Order.Poset -open import Mugen.Cat.StrictOrders -open import Mugen.Cat.Monad - --------------------------------------------------------------------------------- --- Endomorphism Displacements --- Section 3.4 --- --- Given a Monad 'H' on the category of strict orders, we can construct a displacement --- algebra whose carrier set is the set of endomorphisms 'Free H Δ → Free H Δ' between --- free H-algebras in the Eilenberg-Moore category. -open Algebra-hom - -instance - Funlike-algebra-hom - : ∀ {o ℓ} {C : Precategory o ℓ} - → {M : Monad C} - → (let module C = Precategory C) - → ⦃ fl : Funlike C.Hom ⦄ - → Funlike (Algebra-hom C M) - Funlike-algebra-hom ⦃ fl ⦄ .Funlike.au = Underlying-Σ ⦃ ua = Funlike.au fl ⦄ - Funlike-algebra-hom ⦃ fl ⦄ .Funlike.bu = Underlying-Σ ⦃ ua = Funlike.bu fl ⦄ - Funlike-algebra-hom ⦃ fl ⦄ .Funlike._#_ f x = f .morphism # x - -module _ {o r} (H : Monad (Strict-orders o r)) (Δ : Poset o r) where - - open Monad H renaming (M₀ to H₀; M₁ to H₁) - open Cat (Eilenberg-Moore (Strict-orders o r) H) - - private - module H⟨Δ⟩ = Poset (H₀ Δ) - Fᴴ⟨Δ⟩ : Algebra (Strict-orders o r) H - Fᴴ⟨Δ⟩ = Functor.F₀ (Free (Strict-orders o r) H) Δ - {-# INLINE Fᴴ⟨Δ⟩ #-} - - Endomorphism : Type (lsuc o ⊔ lsuc r) - Endomorphism = Hom Fᴴ⟨Δ⟩ Fᴴ⟨Δ⟩ - {-# INLINE Endomorphism #-} - - - -------------------------------------------------------------------------------- - -- Algebra - - endo-is-magma : is-magma _∘_ - endo-is-magma .has-is-set = Hom-set Fᴴ⟨Δ⟩ Fᴴ⟨Δ⟩ - - endo-is-semigroup : is-semigroup _∘_ - endo-is-semigroup .has-is-magma = endo-is-magma - endo-is-semigroup .associative {f} {g} {h} = assoc f g h - - endo-is-monoid : is-monoid id _∘_ - endo-is-monoid .has-is-semigroup = endo-is-semigroup - endo-is-monoid .⊗-idl {f} = idl f - endo-is-monoid .⊗-idr {f} = idr f - - -------------------------------------------------------------------------------- - -- Order - - -- Favonia: the following "HACK" note was left when we were using records - -- to define 'endo[_≤_]'. The accuracy of the note should be checked again. - -- > HACK: We could make this live in a lower universe level, - -- > but then we can't construct a hierarchy theory from it without an annoying lift. - endo[_≤_] : ∀ (σ δ : Endomorphism) → Type (lsuc o ⊔ lsuc r) - endo[_≤_] σ δ = Lift _ ((α : ⌞ Δ ⌟) → σ # (unit.η Δ # α) H⟨Δ⟩.≤ δ # (unit.η Δ # α)) - - endo[_<_] : ∀ (σ δ : Endomorphism) → Type (lsuc o ⊔ lsuc r) - endo[_<_] = strict endo[_≤_] - - endo≤-thin : ∀ σ δ → is-prop endo[ σ ≤ δ ] - endo≤-thin σ δ = hlevel! - - endo≤-refl : ∀ σ → endo[ σ ≤ σ ] - endo≤-refl σ = lift λ _ → H⟨Δ⟩.≤-refl - - endo≤-trans : ∀ σ δ τ → endo[ σ ≤ δ ] → endo[ δ ≤ τ ] → endo[ σ ≤ τ ] - endo≤-trans σ δ τ (lift σ≤δ) (lift δ≤τ) = lift λ α → H⟨Δ⟩.≤-trans (σ≤δ α) (δ≤τ α) - - endo≤-antisym : ∀ σ δ → endo[ σ ≤ δ ] → endo[ δ ≤ σ ] → σ ≡ δ - endo≤-antisym σ δ (lift σ≤δ) (lift δ≤σ) = free-algebra-hom-path H $ ext λ α → - H⟨Δ⟩.≤-antisym (σ≤δ α) (δ≤σ α) - - -------------------------------------------------------------------------------- - -- Left Invariance - - ∘-left-strict-invariant : ∀ (σ δ τ : Endomorphism) → endo[ δ ≤ τ ] → endo[ σ ∘ δ ≤ σ ∘ τ ] × (σ ∘ δ ≡ σ ∘ τ → δ ≡ τ) - ∘-left-strict-invariant σ δ τ (lift δ≤τ) = - (lift λ α → Strictly-monotone.mono (σ .morphism) (δ≤τ α)) , - λ p → free-algebra-hom-path H $ ext λ α → - Strictly-monotone.inj-on-related (σ .morphism) (δ≤τ α) (p #ₚ (unit.η Δ # α)) - - -------------------------------------------------------------------------------- - -- Bundles - -- - -- We do this with copatterns for performance reasons. - - Endo≤ : Poset (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) - Endo≤ .Poset.Ob = Endomorphism - Endo≤ .Poset.poset-on .Poset-on._≤_ = endo[_≤_] - Endo≤ .Poset.poset-on .Poset-on.has-is-poset .is-partial-order.≤-thin {σ} {δ} = endo≤-thin σ δ - Endo≤ .Poset.poset-on .Poset-on.has-is-poset .is-partial-order.≤-refl {σ} = endo≤-refl σ - Endo≤ .Poset.poset-on .Poset-on.has-is-poset .is-partial-order.≤-trans {σ} {δ} {τ} = endo≤-trans σ δ τ - Endo≤ .Poset.poset-on .Poset-on.has-is-poset .is-partial-order.≤-antisym {σ} {δ} = endo≤-antisym σ δ - - Endo∘ : Displacement-algebra (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) - Endo∘ .Displacement-algebra.poset = Endo≤ - Endo∘ .Displacement-algebra.displacement-algebra-on .Displacement-algebra-on.ε = id - Endo∘ .Displacement-algebra.displacement-algebra-on .Displacement-algebra-on._⊗_ = _∘_ - Endo∘ .Displacement-algebra.displacement-algebra-on .Displacement-algebra-on.has-is-displacement-algebra .is-displacement-algebra.has-is-monoid .has-is-semigroup .has-is-magma .has-is-set = hlevel! - Endo∘ .Displacement-algebra.displacement-algebra-on .Displacement-algebra-on.has-is-displacement-algebra .is-displacement-algebra.has-is-monoid .has-is-semigroup .associative = assoc _ _ _ - Endo∘ .Displacement-algebra.displacement-algebra-on .Displacement-algebra-on.has-is-displacement-algebra .is-displacement-algebra.has-is-monoid .⊗-idl = idl _ - Endo∘ .Displacement-algebra.displacement-algebra-on .Displacement-algebra-on.has-is-displacement-algebra .is-displacement-algebra.has-is-monoid .⊗-idr = idr _ - Endo∘ .Displacement-algebra.displacement-algebra-on .Displacement-algebra-on.has-is-displacement-algebra .is-displacement-algebra.left-strict-invariant {σ} {δ} {τ} = ∘-left-strict-invariant σ δ τ diff --git a/src/Mugen/Algebra/Displacement/FiniteSupport.agda b/src/Mugen/Algebra/Displacement/FiniteSupport.agda deleted file mode 100644 index e1ec094..0000000 --- a/src/Mugen/Algebra/Displacement/FiniteSupport.agda +++ /dev/null @@ -1,174 +0,0 @@ -module Mugen.Algebra.Displacement.FiniteSupport where - -open import 1Lab.Reflection.Record - -open import Algebra.Magma -open import Algebra.Monoid -open import Algebra.Semigroup - -open import Mugen.Prelude -open import Mugen.Order.Poset -open import Mugen.Algebra.Displacement -open import Mugen.Algebra.Displacement.IndexedProduct -open import Mugen.Algebra.Displacement.NearlyConstant -open import Mugen.Algebra.OrderedMonoid - - --------------------------------------------------------------------------------- --- Finitely Supported Functions --- Section 3.3.5 --- --- Finitely supported functions over some displacement algebra '𝒟' are --- functions 'f : Nat → 𝒟' that differ from the unit 'ε' in only a finite number of positions. --- These are a special case of the Nearly Constant functions where the base is always ε --- and are implemented as such. - -module FinSupport {o r} (𝒟 : Displacement-algebra o r) ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄ where - private - module 𝒟 = Displacement-algebra 𝒟 - open NearlyConst 𝒟 - - -------------------------------------------------------------------------------- - -- Finite Support Lists - -- - -- As noted above, these are defined to be SupportLists of nearly constant functions, - -- with the constraint that the base is 'ε'. - - record FinSupportList : Type o where - no-eta-equality - field - support : SupportList - - open SupportList support public - - field - is-ε : base ≡ 𝒟.ε - - open FinSupportList - - -- Paths between finitely supportd functions are purely determined by their elements. - fin-support-list-path : ∀ {xs ys} → xs .support ≡ ys .support → xs ≡ ys - fin-support-list-path p i .support = p i - fin-support-list-path {xs = xs} {ys = ys} p i .is-ε = - is-set→squarep (λ _ _ → 𝒟.has-is-set) (ap SupportList.base p) (xs .is-ε) (ys .is-ε) refl i - - private unquoteDecl eqv = declare-record-iso eqv (quote FinSupportList) - - FinSupportList-is-set : is-set FinSupportList - FinSupportList-is-set = - is-hlevel≃ 2 (Iso→Equiv eqv) $ - Σ-is-hlevel 2 SupportList-is-set λ support → - is-hlevel-suc 2 𝒟.has-is-set (SupportList.base support) 𝒟.ε - - merge-fin : FinSupportList → FinSupportList → FinSupportList - merge-fin xs ys .FinSupportList.support = merge (xs .support) (ys .support) - merge-fin xs ys .FinSupportList.is-ε = - base-merge (xs .support) (ys .support) ∙ ap₂ 𝒟._⊗_ (xs .is-ε) (ys .is-ε) ∙ 𝒟.idl - - empty-fin : FinSupportList - empty-fin .support = empty - empty-fin .is-ε = refl - - -------------------------------------------------------------------------------- - -- Order - - _≤_ : FinSupportList → FinSupportList → Type r - _≤_ xs ys = (xs .support) supp≤ (ys .support) - --------------------------------------------------------------------------------- --- Displacement Algebra - -module _ {o r} (𝒟 : Displacement-algebra o r) ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄ where - open FinSupport 𝒟 - open FinSupportList - private module 𝒩 = Displacement-algebra (NearlyConstant 𝒟) - - FiniteSupport : Displacement-algebra o r - FiniteSupport = to-displacement-algebra mk where - mk-strict : make-poset r FinSupportList - mk-strict .make-poset._≤_ = _≤_ - mk-strict .make-poset.≤-refl {xs} = - 𝒩.≤-refl {xs .support} - mk-strict .make-poset.≤-thin {xs} {ys} = - 𝒩.≤-thin {xs .support} {ys .support} - mk-strict .make-poset.≤-trans {xs} {ys} {zs} = - 𝒩.≤-trans {xs .support} {ys .support} {zs .support} - mk-strict .make-poset.≤-antisym {xs} {ys} p q = - fin-support-list-path $ 𝒩.≤-antisym {xs .support} {ys .support} p q - - mk : make-displacement-algebra (to-poset mk-strict) - mk .make-displacement-algebra.ε = empty-fin - mk .make-displacement-algebra._⊗_ = merge-fin - mk .make-displacement-algebra.idl = fin-support-list-path 𝒩.idl - mk .make-displacement-algebra.idr = fin-support-list-path 𝒩.idr - mk .make-displacement-algebra.associative = fin-support-list-path 𝒩.associative - mk .make-displacement-algebra.left-strict-invariant {xs} {ys} {zs} p = - 𝒩.left-invariant {xs .support} {ys .support} {zs .support} p , - (fin-support-list-path ⊙ 𝒩.injr-on-related {xs .support} {ys .support} p ⊙ ap support) - --------------------------------------------------------------------------------- --- Subalgebra Structure - -module _ - {o r} - {𝒟 : Displacement-algebra o r} - (let module 𝒟 = Displacement-algebra 𝒟) - ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄ - where - open FinSupport 𝒟 - - FinSupport⊆NearlyConstant : is-displacement-subalgebra (FiniteSupport 𝒟) (NearlyConstant 𝒟) - FinSupport⊆NearlyConstant = to-displacement-subalgebra mk where - mk : make-displacement-subalgebra _ _ - mk .make-displacement-subalgebra.into = FinSupportList.support - mk .make-displacement-subalgebra.pres-ε = refl - mk .make-displacement-subalgebra.pres-⊗ _ _ = refl - mk .make-displacement-subalgebra.mono _ _ xs λ n → if n = 1 then 2 else if n = 3 then 1 else 5 +-- +-- will be represented as a pair (5, [5,2,5,3]). We will call the +-- first element of this pair "the base" of the function, and the +-- prefix list "the support". +-- +-- However, there is a problem: there can be multiple representations +-- for the same function. The above function can also be represented +-- as (5, [5,2,5,3,5,5,5,5,5,5]), with trailing base elements. +-- To resolve this, we say that a list is compact relative +-- to some 'base : 𝒟' if it does not have any trailing base's. +-- We then only work with compact lists. + +-------------------------------------------------------------------------------- +-- Displacement + +module _ + {A : Poset o r} + ⦃ _ : Discrete ⌞ A ⌟ ⦄ + (𝒟 : Displacement-on A) + where + private + module 𝒟 = Displacement-on 𝒟 + + rep : represents-full-subdisplacement (IndexedProduct Nat (λ _ → 𝒟)) (BasedSupport→Pointwise-is-full-subposet A) + rep .represents-full-subdisplacement.ε = based-support-list (raw [] 𝒟.ε) (lift tt) + rep .represents-full-subdisplacement._⊗_ = merge-with 𝒟._⊗_ + rep .represents-full-subdisplacement.pres-ε = refl + rep .represents-full-subdisplacement.pres-⊗ {xs} {ys} = index-merge-with 𝒟._⊗_ xs ys + module rep = represents-full-subdisplacement rep + + NearlyConstant : Displacement-on (BasedSupport A) + NearlyConstant = rep.displacement-on + + NearlyConstant→Pointwise-is-full-subdisplacement : + is-full-subdisplacement NearlyConstant (IndexedProduct Nat (λ _ → 𝒟)) (BasedSupport→Pointwise A) + NearlyConstant→Pointwise-is-full-subdisplacement = rep.has-is-full-subdisplacement + +-------------------------------------------------------------------------------- +-- Ordered Monoid + +module _ + {A : Poset o r} + ⦃ _ : Discrete ⌞ A ⌟ ⦄ + (𝒟 : Displacement-on A) + (𝒟-ordered-monoid : has-ordered-monoid 𝒟) + where + private + module 𝒟 = Displacement-on 𝒟 + module B = Reasoning (BasedSupport A) + module N = Displacement-on (NearlyConstant 𝒟) + module P = Reasoning (Pointwise Nat λ _ → A) + module I-is-ordered-monoid = + is-ordered-monoid (IndexedProduct-has-ordered-monoid Nat (λ _ → 𝒟) λ _ → 𝒟-ordered-monoid) + + right-invariant : ∀ {xs ys zs} → xs B.≤ ys → (xs N.⊗ zs) B.≤ (ys N.⊗ zs) + right-invariant {xs} {ys} {zs} xs≤ys = + coe1→0 (λ i → index-merge-with 𝒟._⊗_ xs zs i P.≤ index-merge-with 𝒟._⊗_ ys zs i) $ + I-is-ordered-monoid.right-invariant xs≤ys + + NearlyConstant-has-ordered-monoid : has-ordered-monoid (NearlyConstant 𝒟) + NearlyConstant-has-ordered-monoid = + right-invariant→has-ordered-monoid (NearlyConstant 𝒟) λ {xs} {ys} {zs} → + right-invariant {xs} {ys} {zs} diff --git a/src/Mugen/Algebra/Displacement/Instances/NonPositive.agda b/src/Mugen/Algebra/Displacement/Instances/NonPositive.agda new file mode 100644 index 0000000..cb446e9 --- /dev/null +++ b/src/Mugen/Algebra/Displacement/Instances/NonPositive.agda @@ -0,0 +1,36 @@ +module Mugen.Algebra.Displacement.Instances.NonPositive where + +open import Mugen.Prelude +open import Mugen.Algebra.Displacement +open import Mugen.Algebra.Displacement.Subalgebra +open import Mugen.Algebra.Displacement.Instances.Int +open import Mugen.Algebra.Displacement.Instances.Nat +open import Mugen.Algebra.Displacement.Instances.Opposite + +open import Mugen.Order.Instances.NonPositive + renaming (NonPositive to NonPositive-poset) + +open import Mugen.Data.Int + +-------------------------------------------------------------------------------- +-- The Non-Positive Integers +-- Section 3.3.1 +-- +-- These have a terse definition as the opposite order of Nat+, +-- so we just use that. + +NonPositive : Displacement-on NonPositive-poset +NonPositive = Opposite Nat-displacement + +-------------------------------------------------------------------------------- +-- Inclusion into Int + +NonPositive→Int-is-full-subdisplacement + : is-full-subdisplacement NonPositive Int-displacement NonPositive→Int +NonPositive→Int-is-full-subdisplacement = to-full-subdisplacement subalg where + subalg : make-full-subdisplacement NonPositive Int-displacement NonPositive→Int + subalg .make-full-subdisplacement.pres-ε = refl + subalg .make-full-subdisplacement.pres-⊗ {x} {y} = +ℤ-negate x y + subalg .make-full-subdisplacement.pres-≤ {x} {y} = negate-anti-mono y x + subalg .make-full-subdisplacement.injective = negate-injective _ _ + subalg .make-full-subdisplacement.full {x} {y} = negate-anti-full y x diff --git a/src/Mugen/Algebra/Displacement/Instances/Opposite.agda b/src/Mugen/Algebra/Displacement/Instances/Opposite.agda new file mode 100644 index 0000000..8ea9257 --- /dev/null +++ b/src/Mugen/Algebra/Displacement/Instances/Opposite.agda @@ -0,0 +1,42 @@ +module Mugen.Algebra.Displacement.Instances.Opposite where + +open import Mugen.Prelude +open import Mugen.Order.Instances.Opposite renaming (Opposite to Opposite-poset) +open import Mugen.Algebra.Displacement +open import Mugen.Algebra.OrderedMonoid + +private variable + o r : Level + +-------------------------------------------------------------------------------- +-- The Opposite Displacement Algebra +-- Section 3.3.8 +-- +-- Given a displacement algebra '𝒟', we can define another displacement +-- algebra with the same monoid structure, but with a reverse order. + +Opposite : ∀ {A : Poset o r} + → Displacement-on A → Displacement-on (Opposite-poset A) +Opposite {A = A} 𝒟 = to-displacement-on displacement where + open Displacement-on 𝒟 + + displacement : make-displacement (Opposite-poset A) + displacement .make-displacement.ε = ε + displacement .make-displacement._⊗_ = _⊗_ + displacement .make-displacement.idl = idl + displacement .make-displacement.idr = idr + displacement .make-displacement.associative = associative + displacement .make-displacement.left-strict-invariant p = + left-invariant p , λ q → sym $ injectiver-on-related p (sym q) + +module OpProperties {A : Poset o r} {𝒟 : Displacement-on A} where + open Displacement-on 𝒟 + + -------------------------------------------------------------------------------- + -- Ordered Monoid + + Opposite-has-ordered-monoid : has-ordered-monoid 𝒟 → has-ordered-monoid (Opposite 𝒟) + Opposite-has-ordered-monoid 𝒟-ordered-monoid = + right-invariant→has-ordered-monoid (Opposite 𝒟) right-invariant + where + open is-ordered-monoid 𝒟-ordered-monoid diff --git a/src/Mugen/Algebra/Displacement/Instances/Prefix.agda b/src/Mugen/Algebra/Displacement/Instances/Prefix.agda new file mode 100644 index 0000000..3431407 --- /dev/null +++ b/src/Mugen/Algebra/Displacement/Instances/Prefix.agda @@ -0,0 +1,42 @@ +module Mugen.Algebra.Displacement.Instances.Prefix where + +open import Algebra.Magma +open import Algebra.Monoid +open import Algebra.Semigroup + +open import Mugen.Prelude +open import Mugen.Data.List +open import Mugen.Order.StrictOrder +open import Mugen.Order.Lattice +open import Mugen.Order.Instances.Prefix renaming (Prefix to Prefix-poset) +open import Mugen.Algebra.Displacement + +private variable + o r : Level + +-------------------------------------------------------------------------------- +-- Prefix Displacements +-- Section 3.3.6 +-- +-- Given a set 'A', we can define a displacement algebra on 'List A', +-- where 'xs ≤ ys' if 'xs' is a prefix of 'ys'. + +private + -------------------------------------------------------------------------------- + -- Left Invariance + + ++-left-invariant : ∀ {ℓ} {A : Type ℓ} (xs ys zs : List A) → Prefix[ ys ≤ zs ] → Prefix[ (xs ++ ys) ≤ (xs ++ zs) ] + ++-left-invariant [] ys zs ys≤zs = ys≤zs + ++-left-invariant (x ∷ xs) ys zs ys λ n → if n = 1 then 2 else if n = 3 then 1 else 5 --- --- will be represented as a pair (5, [5,2,5,3]). We will call the --- first element of this pair "the base" of the function, and the --- prefix list "the support". --- --- However, there is a slight problem here when we go to show that --- this is a subalgebra of 'IdxProd': it's not injective! The problem --- occurs when you have trailing base elements, meaning 2 lists can --- denote the same function! --- --- To resolve this, we say that a list is compact relative --- to some 'base : 𝒟' if it does not have any trailing base's. --- We then only work with compact lists in our displacement algebra. - -module NearlyConst - {o r} - (𝒟 : Displacement-algebra o r) - ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄ - where - private module 𝒟 = Displacement-algebra 𝒟 - open Idx Nat (λ _ → 𝒟) - module idx𝒟 = Displacement-algebra (IdxProd Nat (λ _ → 𝒟)) - - -------------------------------------------------------------------------------- - -- Raw Support Lists - -- - - record RawList : Type o where - constructor raw - field - elts : List ⌞ 𝒟 ⌟ - base : ⌞ 𝒟 ⌟ - - open RawList - - raw-path : ∀ {xs ys : RawList} - → xs .elts ≡ ys .elts - → xs .base ≡ ys .base - → xs ≡ ys - raw-path p q i .elts = p i - raw-path p q i .base = q i - - private unquoteDecl raw-eqv = declare-record-iso raw-eqv (quote RawList) - - RawList-is-set : is-set RawList - RawList-is-set = - is-hlevel≃ 2 (Iso→Equiv raw-eqv) $ - ×-is-hlevel 2 (ListPath.List-is-hlevel 0 𝒟.has-is-set) (hlevel 2) - - -- Operations and properties for raw support lists - module Raw where - _raw∷_ : ⌞ 𝒟 ⌟ → RawList → RawList - x raw∷ (raw xs b) = raw (x ∷ xs) b - - -- Indexing function that turns a list into a map 'Nat → ⌞ 𝒟 ⌟' - index : RawList → (Nat → ⌞ 𝒟 ⌟) - index (raw [] b) n = b - index (raw (x ∷ xs) b) zero = x - index (raw (x ∷ xs) b) (suc n) = index (raw xs b) n - - -------------------------------------------------------------------------------- - -- Compact Support Lists - -- - -- These will be the actual elements of our displacement algebra. - -- A SupportList consists of a choice of base, and a compact list - -- relative to that base. - - is-compact : RawList → Type o - is-compact (raw [] b) = Lift o ⊤ - is-compact (raw (x ∷ []) b) = ¬ (x ≡ b) - is-compact (raw (_ ∷ y ∷ ys) b) = is-compact (raw (y ∷ ys) b) - - abstract - is-compact-is-prop : ∀ xs → is-prop (is-compact xs) - is-compact-is-prop (raw [] _) = hlevel 1 - is-compact-is-prop (raw (_ ∷ []) _) = hlevel 1 - is-compact-is-prop (raw (_ ∷ y ∷ ys) _) = is-compact-is-prop (raw (y ∷ ys) _) - - module _ (b : ⌞ 𝒟 ⌟) where - compact-list-step : ⌞ 𝒟 ⌟ → List ⌞ 𝒟 ⌟ → List ⌞ 𝒟 ⌟ - compact-list-step x [] with x ≡? b - ... | yes _ = [] - ... | no _ = x ∷ [] - compact-list-step x (y ∷ ys) = x ∷ y ∷ ys - - compact-list : List ⌞ 𝒟 ⌟ → List ⌞ 𝒟 ⌟ - compact-list [] = [] - compact-list (x ∷ xs) = compact-list-step x (compact-list xs) - - compact-step : ⌞ 𝒟 ⌟ → RawList → RawList - compact-step x (raw xs b) = raw (compact-list-step b x xs) b - - compact : RawList → RawList - compact (raw xs b) = raw (compact-list b xs) b - - -- compact preserves 'base' - abstract - base-compact : ∀ xs → compact xs .base ≡ xs .base - base-compact _ = refl - - abstract - compact-compacted : ∀ {xs} → is-compact xs → compact xs ≡ xs - compact-compacted {xs = raw [] _} _ = refl - compact-compacted {xs = raw (x ∷ []) b} x≠b with x ≡? b - ... | yes x=b = absurd (x≠b x=b) - ... | no _ = refl - compact-compacted {xs = raw (x ∷ y ∷ ys) b} is-compact = - ap (compact-step x) $ compact-compacted {xs = raw (y ∷ ys) b} is-compact - - abstract - tail-is-compact : ∀ x xs → is-compact (x raw∷ xs) → is-compact xs - tail-is-compact x (raw [] _) _ = lift tt - tail-is-compact x (raw (y ∷ ys) _) compact = compact - - -- the result of 'compact' is a compact list - abstract - private - compact-step-is-compact : ∀ x xs - → is-compact xs - → is-compact (compact-step x xs) - compact-step-is-compact x (raw [] b) _ with x ≡? b - ... | yes _ = lift tt - ... | no x≠b = x≠b - compact-step-is-compact x (raw (y ∷ ys) b) is-compact = is-compact - - compact-is-compact : ∀ xs → is-compact (compact xs) - compact-is-compact (raw [] _) = lift tt - compact-is-compact (raw (x ∷ xs) b) = - compact-step-is-compact x (compact (raw xs b)) (compact-is-compact (raw xs b)) - - -- 'compact' does not change the result of 'index' - abstract - private - index-compact-step-zero : ∀ x xs - → index (compact-step x xs) zero ≡ x - index-compact-step-zero x (raw [] b) with x ≡? b - ... | yes x=b = sym x=b - ... | no _ = refl - index-compact-step-zero x (raw (_ ∷ _) _) = refl - - index-compact-step-suc : ∀ x xs n - → index (compact-step x xs) (suc n) ≡ index xs n - index-compact-step-suc x (raw [] b) n with x ≡? b - ... | yes _ = refl - ... | no _ = refl - index-compact-step-suc x (raw (_ ∷ _) _) n = refl - - -- Indexing a compacted list is the same as indexing the uncompacted list. - abstract - index-compact : ∀ xs n → index (compact xs) n ≡ index xs n - index-compact (raw [] _) n = refl - index-compact (raw (x ∷ xs) b) zero = - index-compact-step-zero x (compact (raw xs b)) - index-compact (raw (x ∷ xs) b) (suc n) = - index (compact-step x (compact (raw xs b))) (suc n) - ≡⟨ index-compact-step-suc x (compact (raw xs b)) n ⟩ - index (compact (raw xs b)) n - ≡⟨ index-compact (raw xs b) n ⟩ - index (raw xs b) n - ∎ - - -------------------------------------------------------------------------------- - -- Merging Lists - - merge-list-with : (⌞ 𝒟 ⌟ → ⌞ 𝒟 ⌟ → ⌞ 𝒟 ⌟) → RawList → RawList → List ⌞ 𝒟 ⌟ - merge-list-with _⊚_ (raw [] b1) (raw [] b2) = [] - merge-list-with _⊚_ (raw [] b1) (raw (y ∷ ys) b2) = (b1 ⊚ y) ∷ merge-list-with _⊚_ (raw [] b1) (raw ys b2) - merge-list-with _⊚_ (raw (x ∷ xs) b1) (raw [] b2) = (x ⊚ b2) ∷ merge-list-with _⊚_ (raw xs b1) (raw [] b2) - merge-list-with _⊚_ (raw (x ∷ xs) b1) (raw (y ∷ ys) b2) = (x ⊚ y) ∷ merge-list-with _⊚_ (raw xs b1) (raw ys b2) - - merge-with : (⌞ 𝒟 ⌟ → ⌞ 𝒟 ⌟ → ⌞ 𝒟 ⌟) → RawList → RawList → RawList - merge-with _⊚_ xs ys = raw (merge-list-with _⊚_ xs ys) (xs .base ⊚ ys .base) - - abstract - index-merge-with : ∀ f xs ys n → index (merge-with f xs ys) n ≡ f (index xs n) (index ys n) - index-merge-with f (raw [] b1) (raw [] b2) n = refl - index-merge-with f (raw [] b1) (raw (y ∷ ys) b2) zero = refl - index-merge-with f (raw [] b1) (raw (y ∷ ys) b2) (suc n) = index-merge-with f (raw [] b1) (raw ys b2) n - index-merge-with f (raw (x ∷ xs) b1) (raw [] b2) zero = refl - index-merge-with f (raw (x ∷ xs) b1) (raw [] b2) (suc n) = index-merge-with f (raw xs b1) (raw [] b2) n - index-merge-with f (raw (x ∷ xs) b1) (raw (y ∷ ys) b2) zero = refl - index-merge-with f (raw (x ∷ xs) b1) (raw (y ∷ ys) b2) (suc n) = index-merge-with f (raw xs b1) (raw ys b2) n - - base-merge-with : ∀ f xs ys → merge-with f xs ys .base ≡ f (xs .base) (ys .base) - base-merge-with f xs ys = refl - - - -------------------------------------------------------------------------------- - -- Order - - _raw≤_ : RawList → RawList → Type r - xs raw≤ ys = index xs idx𝒟.≤ index ys - - index= : RawList → RawList → Type o - index= xs ys = (n : Nat) → index xs n ≡ index ys n - - abstract - index=? : ∀ xs ys → Dec (index= xs ys) - index=? (raw [] b1) (raw [] b2) with b1 ≡? b2 - ... | yes b1=b2 = yes λ n → b1=b2 - ... | no b1≠b2 = no λ p → b1≠b2 (p 0) - index=? (raw (x ∷ xs) b1) (raw [] b2) with x ≡? b2 | index=? (raw xs b1) (raw [] b2) - ... | no x≠b2 | _ = no λ p → x≠b2 (p 0) - ... | yes _ | no xs≠[] = no λ p → xs≠[] (p ⊙ suc) - ... | yes x=b2 | yes xs=[] = yes λ { zero → x=b2; (suc n) → xs=[] n } - index=? (raw [] b1) (raw (y ∷ ys) b2) with b1 ≡? y | index=? (raw [] b1) (raw ys b2) - ... | no b1≠y | _ = no λ p → b1≠y (p 0) - ... | yes _ | no []≠ys = no λ p → []≠ys (p ⊙ suc) - ... | yes b1=y | yes []=ys = yes λ { zero → b1=y; (suc n) → []=ys n } - index=? (raw (x ∷ xs) b1) (raw (y ∷ ys) b2) with x ≡? y | index=? (raw xs b1) (raw ys b2) - ... | no x≠y | _ = no λ p → x≠y (p 0) - ... | yes _ | no xs≠ys = no λ p → xs≠ys (p ⊙ suc) - ... | yes x=y | yes xs=ys = yes λ { zero → x=y; (suc n) → xs=ys n } - - -- 'index=' implies equality - abstract - private - base-singleton-isnt-compact : ∀ {x xs b} → x ≡ b → xs ≡ raw [] b → is-compact (x raw∷ xs) → ⊥ - base-singleton-isnt-compact {xs = raw [] _} x=b xs=[] is-compact = is-compact $ x=b ∙ sym (ap base xs=[]) - base-singleton-isnt-compact {xs = raw (_ ∷ _) _} x=b xs=[] is-compact = ∷≠[] $ ap elts xs=[] - - index-compacted-inj : ∀ xs ys - → is-compact xs - → is-compact ys - → index= xs ys - → xs ≡ ys - index-compacted-inj (raw [] b1) (raw [] b2) _ _ p = raw-path refl (p 0) - index-compacted-inj (raw (x ∷ xs) b1) (raw [] b2) x∷xs-compact []-compact p = - let xs-compact = tail-is-compact x (raw xs b1) x∷xs-compact in - let xs=[] = index-compacted-inj (raw xs b1) (raw [] b2) xs-compact []-compact (p ⊙ suc) in - absurd (base-singleton-isnt-compact (p 0) xs=[] x∷xs-compact) - index-compacted-inj (raw [] b1) (raw (y ∷ ys) b2) []-compact y∷ys-compact p = - let ys-compact = tail-is-compact y (raw ys b2) y∷ys-compact in - let []=ys = index-compacted-inj (raw [] b1) (raw ys b2) []-compact ys-compact (p ⊙ suc) in - absurd $ᵢ base-singleton-isnt-compact (sym (p 0)) (sym []=ys) y∷ys-compact - index-compacted-inj (raw (x ∷ xs) b1) (raw (y ∷ ys) b2) x∷xs-compact y∷ys-compact p = - let xs-compact = tail-is-compact x (raw xs b1) x∷xs-compact in - let ys-compact = tail-is-compact y (raw ys b2) y∷ys-compact in - let xs=ys = index-compacted-inj (raw xs b1) (raw ys b2) xs-compact ys-compact (p ⊙ suc) in - ap₂ _raw∷_ (p 0) xs=ys - - record SupportList : Type o where - constructor support-list - no-eta-equality - field - list : RawList - has-is-compact : Raw.is-compact list - - open RawList list public - - open SupportList - - -- Paths in support lists are determined by paths between the bases + paths between the elements. - support-list-path : ∀ {xs ys : SupportList} → xs .list ≡ ys .list → xs ≡ ys - support-list-path p i .list = p i - support-list-path {xs = xs} {ys = ys} p i .has-is-compact = - is-prop→pathp (λ i → Raw.is-compact-is-prop (p i)) (xs .has-is-compact) (ys .has-is-compact) i - - private unquoteDecl eqv = declare-record-iso eqv (quote SupportList) - - SupportList-is-set : is-set SupportList - SupportList-is-set = - is-hlevel≃ 2 (Iso→Equiv eqv) $ - Σ-is-hlevel 2 RawList-is-set λ xs → - is-prop→is-set (Raw.is-compact-is-prop xs) - - merge-with : (⌞ 𝒟 ⌟ → ⌞ 𝒟 ⌟ → ⌞ 𝒟 ⌟) → SupportList → SupportList → SupportList - merge-with f xs ys .list = Raw.compact $ Raw.merge-with f (xs .list) (ys .list) - merge-with f xs ys .has-is-compact = Raw.compact-is-compact $ Raw.merge-with f (xs .list) (ys .list) - - merge : SupportList → SupportList → SupportList - merge = merge-with 𝒟._⊗_ - - -- The empty SupportList - empty : SupportList - empty .list = raw [] 𝒟.ε - empty .has-is-compact = lift tt - - _supp≤_ : SupportList → SupportList → Type r - xs supp≤ ys = xs .list Raw.raw≤ ys .list - - index : SupportList → (Nat → ⌞ 𝒟 ⌟) - index xs = Raw.index (xs .list) - - abstract - index-merge-with : ∀ f xs ys → index (merge-with f xs ys) ≡ map₂ f (index xs) (index ys) - index-merge-with f xs ys = funext λ n → - Raw.index-compact (Raw.merge-with f (xs .list) (ys .list)) n - ∙ Raw.index-merge-with f (xs .list) (ys .list) n - - index-merge : ∀ xs ys → index (merge xs ys) ≡ (index xs idx⊗ index ys) - index-merge = index-merge-with 𝒟._⊗_ - - base-merge-with : ∀ f xs ys → merge-with f xs ys .base ≡ f (xs .base) (ys .base) - base-merge-with f xs ys = Raw.base-compact (Raw.merge-with f (xs .list) (ys .list)) - - base-merge : ∀ xs ys → merge xs ys .base ≡ (xs .base 𝒟.⊗ ys .base) - base-merge = base-merge-with 𝒟._⊗_ - - abstract - supp-ext : ∀ {xs ys} → ((n : Nat) → index xs n ≡ index ys n) → xs ≡ ys - supp-ext {xs} {ys} p = support-list-path $ - Raw.index-compacted-inj (xs .list) (ys .list) (xs .has-is-compact) (ys .has-is-compact) p - - index-inj : ∀ {xs ys} → index xs ≡ index ys → xs ≡ ys - index-inj p = supp-ext (happly p) - - -- XXX this will be replaced by the Immortal specification builders - merge-left-invariant : ∀ {xs ys zs} → ys supp≤ zs → merge xs ys supp≤ merge xs zs - merge-left-invariant {xs} {ys} {zs} ys≤zs = - coe1→0 (λ i → index-merge xs ys i idx𝒟.≤ index-merge xs zs i) $ - idx𝒟.left-invariant ys≤zs - - -- XXX this will be replaced by the Immortal specification builders - merge-injr-on-≤ : ∀ {xs ys zs} → ys supp≤ zs → merge xs ys ≡ merge xs zs → ys ≡ zs - merge-injr-on-≤ {xs} {ys} {zs} ys≤zs p = index-inj $ idx𝒟.injr-on-related ys≤zs $ - coe0→1 (λ i → index-merge xs ys i ≡ index-merge xs zs i) (ap index p) - - --------------------------------------------------------------------------------- --- Bundled Instances - -module _ {o r} (𝒟 : Displacement-algebra o r) ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄ where - private module 𝒟 = Displacement-algebra 𝒟 - open Idx Nat (λ _ → 𝒟) - open NearlyConst 𝒟 - - NearlyConstant : Displacement-algebra o r - NearlyConstant = to-displacement-algebra mk where - open make-poset - mk-poset : make-poset r SupportList - mk-poset ._≤_ = _supp≤_ - mk-poset .≤-refl = idx≤-refl - mk-poset .≤-trans = idx≤-trans - mk-poset .≤-thin = idx≤-thin - mk-poset .≤-antisym p q = index-inj $ idx≤-antisym p q - - open make-displacement-algebra - mk : make-displacement-algebra (to-poset mk-poset) - mk .ε = empty - mk ._⊗_ = merge - mk .idl {xs} = index-inj $ index-merge empty xs ∙ idx⊗-idl {index xs} - mk .idr {xs} = index-inj $ index-merge xs empty ∙ idx⊗-idr {index xs} - mk .associative {xs} {ys} {zs} = index-inj $ - index (merge xs (merge ys zs)) - ≡⟨ index-merge xs (merge ys zs) ⟩ - (index xs idx⊗ index (merge ys zs)) - ≡⟨ ap (index xs idx⊗_) $ index-merge ys zs ⟩ - (index xs idx⊗ (index ys idx⊗ index zs)) - ≡⟨ idx⊗-associative ⟩ - ((index xs idx⊗ index ys) idx⊗ index zs) - ≡˘⟨ ap (_idx⊗ index zs) $ index-merge xs ys ⟩ - (index (merge xs ys) idx⊗ index zs) - ≡˘⟨ index-merge (merge xs ys) zs ⟩ - index (merge (merge xs ys) zs) - ∎ - mk .left-strict-invariant {xs} {ys} {zs} p = - merge-left-invariant {xs = xs} {ys} {zs} p , merge-injr-on-≤ {xs = xs} {ys} {zs} p - --------------------------------------------------------------------------------- --- Subalgebra Structure - -module _ {o r} {𝒟 : Displacement-algebra o r} ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄ where - open NearlyConst 𝒟 - - NearlyConstant⊆IdxProd : is-displacement-subalgebra (NearlyConstant 𝒟) (IdxProd Nat λ _ → 𝒟) - NearlyConstant⊆IdxProd = to-displacement-subalgebra mk where - mk : make-displacement-subalgebra (NearlyConstant 𝒟) (IdxProd Nat λ _ → 𝒟) - mk .make-displacement-subalgebra.into = index - mk .make-displacement-subalgebra.pres-ε = refl - mk .make-displacement-subalgebra.pres-⊗ xs ys = index-merge xs ys - mk .make-displacement-subalgebra.mono xs ys xs≤ys = xs≤ys - mk .make-displacement-subalgebra.inj = index-inj - --------------------------------------------------------------------------------- --- Ordered Monoid - -module _ - {o r} - {𝒟 : Displacement-algebra o r} - (𝒟-ordered-monoid : has-ordered-monoid 𝒟) - ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄ - where - private module 𝒟 = Displacement-algebra 𝒟 - open Idx Nat (λ _ → 𝒟) - open NearlyConst 𝒟 - open is-ordered-monoid (idx⊗-has-ordered-monoid Nat (λ _ → 𝒟) (λ _ → 𝒟-ordered-monoid)) - - supp≤-right-invariant : ∀ {xs ys zs} → xs supp≤ ys → merge xs zs supp≤ merge ys zs - supp≤-right-invariant {xs} {ys} {zs} xs≤ys = - coe1→0 (λ i → index-merge xs zs i idx≤ index-merge ys zs i) $ - right-invariant xs≤ys - - nearly-constant-has-ordered-monoid : has-ordered-monoid (NearlyConstant 𝒟) - nearly-constant-has-ordered-monoid = right-invariant→has-ordered-monoid (NearlyConstant 𝒟) $ λ {xs} {ys} {zs} → - supp≤-right-invariant {xs} {ys} {zs} - --------------------------------------------------------------------------------- --- Joins - -module NearlyConstJoins - {o r} - {𝒟 : Displacement-algebra o r} - (𝒟-joins : has-joins 𝒟) - ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄ - where - open Idx Nat (λ _ → 𝒟) - open NearlyConst 𝒟 - private module 𝒟 = Displacement-algebra 𝒟 - private module 𝒥 = has-joins 𝒟-joins - private module idx𝒥 = has-joins (idx⊗-has-joins Nat (λ _ → 𝒟) (λ _ → 𝒟-joins)) - - join : SupportList → SupportList → SupportList - join = merge-with 𝒥.join - - index-preserves-join : ∀ xs ys → index (join xs ys) ≡ idx𝒥.join (index xs) (index ys) - index-preserves-join = index-merge-with 𝒥.join - - nearly-constant-has-joins : has-joins (NearlyConstant 𝒟) - nearly-constant-has-joins .has-joins.join = join - nearly-constant-has-joins .has-joins.joinl {xs} {ys} n = - 𝒟.≤+=→≤ 𝒥.joinl (sym $ happly (index-preserves-join xs ys) n) - nearly-constant-has-joins .has-joins.joinr {xs} {ys} n = - 𝒟.≤+=→≤ 𝒥.joinr (sym $ happly (index-preserves-join xs ys) n) - nearly-constant-has-joins .has-joins.universal {xs} {ys} {zs} xs≤zs ys≤zs n = - 𝒟.=+≤→≤ (happly (index-preserves-join xs ys) n) (𝒥.universal (xs≤zs n) (ys≤zs n)) - - nearly-constant-is-subsemilattice : is-displacement-subsemilattice nearly-constant-has-joins (idx⊗-has-joins Nat (λ _ → 𝒟) (λ _ → 𝒟-joins)) - nearly-constant-is-subsemilattice .is-displacement-subsemilattice.has-displacement-subalgebra = NearlyConstant⊆IdxProd - nearly-constant-is-subsemilattice .is-displacement-subsemilattice.pres-joins x y = index-preserves-join x y - --------------------------------------------------------------------------------- --- Bottoms - -module _ - {o r} - {𝒟 : Displacement-algebra o r} - (𝒟-bottom : has-bottom 𝒟) - ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄ - where - private module 𝒟 = Displacement-algebra 𝒟 - open NearlyConst 𝒟 - open has-bottom 𝒟-bottom - - nearly-constant-has-bottom : has-bottom (NearlyConstant 𝒟) - nearly-constant-has-bottom .has-bottom.bot = support-list (raw [] bot) (lift tt) - nearly-constant-has-bottom .has-bottom.is-bottom xs n = is-bottom _ - - nearly-constant-is-bounded-subalgebra : is-bounded-displacement-subalgebra nearly-constant-has-bottom (idx⊗-has-bottom Nat (λ _ → 𝒟) (λ _ → 𝒟-bottom)) - nearly-constant-is-bounded-subalgebra .is-bounded-displacement-subalgebra.has-displacement-subalgebra = NearlyConstant⊆IdxProd - nearly-constant-is-bounded-subalgebra .is-bounded-displacement-subalgebra.pres-bottom = refl - --------------------------------------------------------------------------------- --- Extensionality based on 'index-ext' - --- FIXME: Need to check the accuracy of the following statement again: --- 1lab's or Agda's instance search somehow does not seem to deal with explicit arguments? --- So we re-parametrize things with implicit '𝒟' and '_≡?_'. -module _ {o r} - {𝒟 : Displacement-algebra o r} - ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄ - where - private module 𝒟 = Displacement-algebra 𝒟 - open NearlyConst 𝒟 - - Extensional-SupportList : ∀ {ℓr} ⦃ s : Extensional ⌞ 𝒟 ⌟ ℓr ⦄ → Extensional SupportList ℓr - Extensional-SupportList ⦃ s ⦄ .Pathᵉ xs ys = - (n : Nat) → s .Pathᵉ (index xs n) (index ys n) - Extensional-SupportList ⦃ s ⦄ .reflᵉ xs = - λ n → s .reflᵉ (index xs n) - Extensional-SupportList ⦃ s ⦄ .idsᵉ .to-path p = - supp-ext λ n → s .idsᵉ .to-path (p n) - Extensional-SupportList ⦃ s ⦄ .idsᵉ .to-path-over p = - is-prop→pathp (λ _ → Π-is-hlevel 1 λ n → identity-system-hlevel 1 (s .idsᵉ) 𝒟.has-is-set) _ p - - instance - extensionality-support-list : ∀ {ℓr} ⦃ s : Extensional ⌞ 𝒟 ⌟ ℓr ⦄ → Extensionality SupportList - extensionality-support-list = record { lemma = quote Extensional-SupportList } diff --git a/src/Mugen/Algebra/Displacement/NonPositive.agda b/src/Mugen/Algebra/Displacement/NonPositive.agda deleted file mode 100644 index 359a820..0000000 --- a/src/Mugen/Algebra/Displacement/NonPositive.agda +++ /dev/null @@ -1,53 +0,0 @@ -module Mugen.Algebra.Displacement.NonPositive where - -open import Mugen.Prelude -open import Mugen.Algebra.Displacement -open import Mugen.Algebra.Displacement.Int -open import Mugen.Algebra.Displacement.Nat -open import Mugen.Algebra.Displacement.Opposite - -open import Mugen.Order.Opposite - -open import Mugen.Data.Int -open import Mugen.Data.Nat - --------------------------------------------------------------------------------- --- The Non-Positive Integers --- Section 3.3.1 --- --- These have a terse definition as the opposite order of Nat+, --- so we just use that. - -NonPositive+ : Displacement-algebra lzero lzero -NonPositive+ = Nat+ ^opᵈ - --------------------------------------------------------------------------------- --- Joins - -non-positive-+-has-joins : has-joins NonPositive+ -non-positive-+-has-joins .has-joins.join = min -non-positive-+-has-joins .has-joins.joinl {x} {y} = - min-≤l x y -non-positive-+-has-joins .has-joins.joinr {x} {y} = - min-≤r x y -non-positive-+-has-joins .has-joins.universal {x} {y} {z} z≤x z≤y = - min-is-glb x y z z≤x z≤y - --------------------------------------------------------------------------------- --- Subalgebra - -NonPositive+⊆Int+ : is-displacement-subalgebra NonPositive+ Int+ -NonPositive+⊆Int+ = to-displacement-subalgebra subalg where - subalg : make-displacement-subalgebra NonPositive+ Int+ - subalg .make-displacement-subalgebra.into x = - x - subalg .make-displacement-subalgebra.pres-ε = refl - subalg .make-displacement-subalgebra.pres-⊗ = +ℤ-negate - subalg .make-displacement-subalgebra.mono x y = negate-anti-mono y x - subalg .make-displacement-subalgebra.inj = negate-inj _ _ - -NonPositive-is-subsemilattice : is-displacement-subsemilattice non-positive-+-has-joins Int+-has-joins -NonPositive-is-subsemilattice .is-displacement-subsemilattice.has-displacement-subalgebra = NonPositive+⊆Int+ -NonPositive-is-subsemilattice .is-displacement-subsemilattice.pres-joins zero zero = refl -NonPositive-is-subsemilattice .is-displacement-subsemilattice.pres-joins zero (suc y) = refl -NonPositive-is-subsemilattice .is-displacement-subsemilattice.pres-joins (suc x) zero = refl -NonPositive-is-subsemilattice .is-displacement-subsemilattice.pres-joins (suc x) (suc y) = refl diff --git a/src/Mugen/Algebra/Displacement/Opposite.agda b/src/Mugen/Algebra/Displacement/Opposite.agda deleted file mode 100644 index e4614e8..0000000 --- a/src/Mugen/Algebra/Displacement/Opposite.agda +++ /dev/null @@ -1,38 +0,0 @@ -module Mugen.Algebra.Displacement.Opposite where - -open import Mugen.Prelude -open import Mugen.Order.Poset -open import Mugen.Order.Opposite -open import Mugen.Algebra.Displacement -open import Mugen.Algebra.OrderedMonoid - --------------------------------------------------------------------------------- --- The Opposite Displacement Algebra --- Section 3.3.8 --- --- Given a displacement algebra '𝒟', we can define another displacement --- algebra with the same monoid structure, but with a reverse order. - -_^opᵈ : ∀ {o r} → Displacement-algebra o r → Displacement-algebra o r -𝒟 ^opᵈ = to-displacement-algebra displacement where - open Displacement-algebra 𝒟 - - displacement : make-displacement-algebra (poset ^opˢ) - displacement .make-displacement-algebra.ε = ε - displacement .make-displacement-algebra._⊗_ = _⊗_ - displacement .make-displacement-algebra.idl = idl - displacement .make-displacement-algebra.idr = idr - displacement .make-displacement-algebra.associative = associative - displacement .make-displacement-algebra.left-strict-invariant p = - left-invariant p , λ q → sym $ injr-on-related p (sym q) - -module OpProperties {o r} {𝒟 : Displacement-algebra o r} where - open Displacement-algebra 𝒟 - - -------------------------------------------------------------------------------- - -- Ordered Monoid - - op-has-ordered-monoid : has-ordered-monoid 𝒟 → has-ordered-monoid (𝒟 ^opᵈ) - op-has-ordered-monoid 𝒟-ordered-monoid = right-invariant→has-ordered-monoid (𝒟 ^opᵈ) right-invariant - where - open is-ordered-monoid 𝒟-ordered-monoid diff --git a/src/Mugen/Algebra/Displacement/Prefix.agda b/src/Mugen/Algebra/Displacement/Prefix.agda deleted file mode 100644 index 912dbdc..0000000 --- a/src/Mugen/Algebra/Displacement/Prefix.agda +++ /dev/null @@ -1,48 +0,0 @@ -module Mugen.Algebra.Displacement.Prefix where - -open import Algebra.Magma -open import Algebra.Monoid -open import Algebra.Semigroup - -open import Mugen.Prelude -open import Mugen.Data.List -open import Mugen.Order.Poset -open import Mugen.Order.Prefix -open import Mugen.Algebra.Displacement - --------------------------------------------------------------------------------- --- Prefix Displacements --- Section 3.3.6 --- --- Given a set 'A', we can define a displacement algebra on 'List A', --- where 'xs ≤ ys' if 'xs' is a prefix of 'ys'. - - -------------------------------------------------------------------------------- - -- Left Invariance - -++-left-invariant : ∀ {ℓ} {A : Type ℓ} (xs ys zs : List A) → Prefix[ ys ≤ zs ] → Prefix[ (xs ++ ys) ≤ (xs ++ zs) ] -++-left-invariant [] ys zs ys≤zs = ys≤zs -++-left-invariant (x ∷ xs) ys zs ys_ M : Functor (Strict-orders o o) (Strict-orders o o) - M .F₀ L = L ⋉[ ε ] poset + M .F₀ L = L ⋉[ ε ] A M .F₁ f .hom (l , d) = (f .hom l) , d - M .F₁ {L} {N} f .strict-mono {l1 , d1} {l2 , d2} = - ∥-∥-rec (×-is-hlevel 1 squash $ Π-is-hlevel 1 λ _ → Poset.has-is-set (M .F₀ L) _ _) λ where + M .F₁ {L} {N} f .pres-< {l1 , d1} {l2 , d2} = + ∥-∥-rec (×-is-hlevel 1 squash $ Π-is-hlevel 1 λ _ → Poset.Ob-is-set (M .F₀ L) _ _) λ where (biased l1=l2 d1≤d2) → inc (biased (ap (f .hom) l1=l2) d1≤d2) , λ p → ap₂ _,_ l1=l2 (ap snd p) - (centred l1≤l2 d1≤ε ε≤d2) → inc (centred (mono f l1≤l2) d1≤ε ε≤d2) , λ p → - ap₂ _,_ (inj-on-related f l1≤l2 (ap fst p)) (ap snd p) + (centred l1≤l2 d1≤ε ε≤d2) → inc (centred (pres-≤ f l1≤l2) d1≤ε ε≤d2) , λ p → + ap₂ _,_ (injective-on-related f l1≤l2 (ap fst p)) (ap snd p) M .F-id = trivial! M .F-∘ f g = trivial! unit : Id => M unit .η L .hom l = l , ε - unit .η L .strict-mono l1≤l2 = inc (centred l1≤l2 ≤-refl ≤-refl) , ap fst + unit .η L .pres-< l1≤l2 = inc (centred l1≤l2 ≤-refl ≤-refl) , ap fst unit .is-natural L L' f = trivial! mult : M F∘ M => M mult .η L .hom ((l , x) , y) = l , (x ⊗ y) - mult .η L .strict-mono {(a1 , d1) , e1} {(a2 , d2) , e2} = - ∥-∥-rec (×-is-hlevel 1 squash $ Π-is-hlevel 1 λ _ → Poset.has-is-set (M .F₀ (M .F₀ L)) _ _) lemma where - lemma : (M .F₀ L) ⋉[ ε ] poset [ ((a1 , d1) , e1) raw≤ ((a2 , d2) , e2) ] - → (L ⋉[ ε ] poset [ (a1 , (d1 ⊗ e1)) ≤ (a2 , (d2 ⊗ e2)) ]) + mult .η L .pres-< {(a1 , d1) , e1} {(a2 , d2) , e2} = + ∥-∥-rec (×-is-hlevel 1 squash $ Π-is-hlevel 1 λ _ → Poset.Ob-is-set (M .F₀ (M .F₀ L)) _ _) lemma where + lemma : (M .F₀ L) ⋉[ ε ] A [ ((a1 , d1) , e1) raw≤ ((a2 , d2) , e2) ] + → (L ⋉[ ε ] A [ (a1 , (d1 ⊗ e1)) ≤ (a2 , (d2 ⊗ e2)) ]) × ((a1 , (d1 ⊗ e1)) ≡ (a2 , (d2 ⊗ e2)) → ((a1 , d1) , e1) ≡ ((a2 , d2) , e2)) lemma (biased ad1=ad2 e1≤e2) = inc (biased (ap fst ad1=ad2) (=+≤→≤ (ap (_⊗ e1) (ap snd ad1=ad2)) (left-invariant e1≤e2))) , - λ p i → ad1=ad2 i , injr-on-related e1≤e2 (ap snd p ∙ ap (_⊗ e2) (sym $ ap snd ad1=ad2)) i + λ p i → ad1=ad2 i , injectiver-on-related e1≤e2 (ap snd p ∙ ap (_⊗ e2) (sym $ ap snd ad1=ad2)) i lemma (centred ad1≤ad2 e1≤ε ε≤e2) = ∥-∥-map lemma₂ ad1≤ad2 , lemma₃ where d1⊗e1≤d1 : (d1 ⊗ e1) ≤ d1 d1⊗e1≤d1 = ≤+=→≤ (left-invariant e1≤ε) idr @@ -59,8 +59,8 @@ import Mugen.Order.Reasoning d2≤d2⊗e2 : d2 ≤ (d2 ⊗ e2) d2≤d2⊗e2 = =+≤→≤ (sym idr) (left-invariant ε≤e2) - lemma₂ : L ⋉[ ε ] poset [ (a1 , d1) raw≤ (a2 , d2) ] - → L ⋉[ ε ] poset [ (a1 , (d1 ⊗ e1)) raw≤ (a2 , (d2 ⊗ e2)) ] + lemma₂ : L ⋉[ ε ] A [ (a1 , d1) raw≤ (a2 , d2) ] + → L ⋉[ ε ] A [ (a1 , (d1 ⊗ e1)) raw≤ (a2 , (d2 ⊗ e2)) ] lemma₂ (biased a1=a2 d1≤d2) = biased a1=a2 (≤-trans d1⊗e1≤d1 (≤-trans d1≤d2 d2≤d2⊗e2)) lemma₂ (centred a1≤a2 d1≤ε ε≤d2) = centred a1≤a2 (≤-trans d1⊗e1≤d1 d1≤ε) (≤-trans ε≤d2 d2≤d2⊗e2) @@ -70,7 +70,7 @@ import Mugen.Order.Reasoning a1=a2 = ap fst p d2≤d1 : d2 ≤ d1 - d2≤d1 = + d2≤d1 = begin-≤[ lzero ] d2 ≐⟨ sym idr ⟩ d2 ⊗ ε ≤⟨ left-invariant ε≤e2 ⟩ d2 ⊗ e2 ≐⟨ sym $ ap snd p ⟩ @@ -82,7 +82,7 @@ import Mugen.Order.Reasoning d1=d2 = ≤-antisym (⋉-snd-invariant ad1≤ad2) d2≤d1 e1=e2 : e1 ≡ e2 - e1=e2 = injr-on-related (≤-trans e1≤ε ε≤e2) $ ap snd p ∙ ap (_⊗ e2) (sym d1=d2) + e1=e2 = injectiver-on-related (≤-trans e1≤ε ε≤e2) $ ap snd p ∙ ap (_⊗ e2) (sym d1=d2) mult .is-natural L L' f = trivial! diff --git a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda index 4bbc1c7..7499526 100644 --- a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda +++ b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda @@ -12,7 +12,7 @@ import Cat.Functor.Reasoning as FR open import Mugen.Prelude open import Mugen.Algebra.Displacement -open import Mugen.Algebra.Displacement.Endomorphism +open import Mugen.Algebra.Displacement.Instances.Endomorphism open import Mugen.Cat.Endomorphisms open import Mugen.Cat.StrictOrders @@ -20,13 +20,14 @@ open import Mugen.Cat.Monad open import Mugen.Cat.HierarchyTheory open import Mugen.Cat.HierarchyTheory.McBride -open import Mugen.Order.Coproduct -open import Mugen.Order.LeftInvariantRightCentered -open import Mugen.Order.Poset -open import Mugen.Order.Singleton -open import Mugen.Order.Discrete +open import Mugen.Order.StrictOrder +open import Mugen.Order.Instances.Endomorphism renaming (Endomorphism to Endomorphism-poset) +open import Mugen.Order.Instances.Coproduct +open import Mugen.Order.Instances.LeftInvariantRightCentered +open import Mugen.Order.Instances.Singleton +open import Mugen.Order.Instances.Discrete -import Mugen.Order.Reasoning +import Mugen.Order.Reasoning as Reasoning -------------------------------------------------------------------------------- -- The Universal Embedding Theorem @@ -49,10 +50,13 @@ module _ {o r} (H : Hierarchy-theory o r) (Δ : Poset o r) (Ψ : Set (lsuc o ⊔ private Δ⁺ : Poset o r - Δ⁺ = ◆ ⊕ (Δ ⊕ Δ) + Δ⁺ = Coproduct ◆ (Coproduct Δ Δ) - 𝒟 : Displacement-algebra (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) - 𝒟 = Endo∘ H Δ⁺ + H⟨Δ⁺⟩→-poset : Poset (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) + H⟨Δ⁺⟩→-poset = Endomorphism-poset H Δ⁺ + + H⟨Δ⁺⟩→ : Displacement-on H⟨Δ⁺⟩→-poset + H⟨Δ⁺⟩→ = Endomorphism H Δ⁺ SOrd : Precategory (lsuc o ⊔ lsuc r) (o ⊔ r) SOrd = Strict-orders o r @@ -65,7 +69,7 @@ module _ {o r} (H : Hierarchy-theory o r) (Δ : Poset o r) (Ψ : Set (lsuc o ⊔ SOrd↑ = Strict-orders (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) SOrdᴹᴰ : Precategory (lsuc (lsuc o) ⊔ lsuc (lsuc r)) (lsuc (lsuc o) ⊔ lsuc (lsuc r)) - SOrdᴹᴰ = Eilenberg-Moore SOrd↑ (ℳ 𝒟) + SOrdᴹᴰ = Eilenberg-Moore SOrd↑ (ℳ H⟨Δ⁺⟩→) Fᴴ⟨_⟩ : Poset o r → Algebra SOrd H Fᴴ⟨_⟩ = Functor.F₀ (Free SOrd H) @@ -73,20 +77,20 @@ module _ {o r} (H : Hierarchy-theory o r) (Δ : Poset o r) (Ψ : Set (lsuc o ⊔ Endoᴴ⟨Δ⟩ : Type (o ⊔ r) Endoᴴ⟨Δ⟩ = Hom (fst Fᴴ⟨ Δ ⟩) (fst Fᴴ⟨ Δ ⟩) - Fᴹᴰ⟨_⟩ : Poset (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) → Algebra SOrd↑ (ℳ 𝒟) - Fᴹᴰ⟨_⟩ = Functor.F₀ (Free SOrd↑ (ℳ 𝒟)) + Fᴹᴰ⟨_⟩ : Poset (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) → Algebra SOrd↑ (ℳ H⟨Δ⁺⟩→) + Fᴹᴰ⟨_⟩ = Functor.F₀ (Free SOrd↑ (ℳ H⟨Δ⁺⟩→)) module Δ = Poset Δ - module 𝒟 = Displacement-algebra 𝒟 + module H⟨Δ⁺⟩→-poset = Reasoning H⟨Δ⁺⟩→-poset + module H⟨Δ⁺⟩→ = Displacement-on H⟨Δ⁺⟩→ module H = Monad H module HR = FR H.M - module ℳᴰ = Monad (ℳ 𝒟) + module ℳᴰ = Monad (ℳ H⟨Δ⁺⟩→) module H⟨Δ⁺⟩ = Poset (H.M₀ Δ⁺) module H⟨Δ⟩ = Poset (H.M₀ Δ) module Fᴹᴰ⟨Δ⁺⟩ = Poset (fst Fᴹᴰ⟨ Lift≤ (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) Δ⁺ ⟩) module Fᴹᴰ⟨Ψ⟩ = Poset (fst Fᴹᴰ⟨ Disc Ψ ⟩) - module H⟨Δ⁺⟩→ = Displacement-algebra (Endo∘ H Δ⁺) module SOrd {o} {r} = Cat (Strict-orders o r) module SOrdᴴ = Cat SOrdᴴ module SOrdᴹᴰ = Cat SOrdᴹᴰ @@ -104,11 +108,11 @@ module _ {o r} (H : Hierarchy-theory o r) (Δ : Poset o r) (Ψ : Set (lsuc o ⊔ ι₀-hom : Hom ◆ Δ⁺ ι₀-hom .hom = ι₀ - ι₀-hom .strict-mono α≤β = α≤β , λ _ → refl + ι₀-hom .pres-< α≤β = α≤β , λ _ → refl ι₁-hom : Hom Δ Δ⁺ ι₁-hom .hom = ι₁ - ι₁-hom .strict-mono α≤β = α≤β , ι₁-inj + ι₁-hom .pres-< α≤β = α≤β , ι₁-inj ι₁-monic : SOrd.is-monic ι₁-hom ι₁-monic g h p = ext λ α → ι₁-inj (p #ₚ α) @@ -122,9 +126,9 @@ module _ {o r} (H : Hierarchy-theory o r) (Δ : Poset o r) (Ψ : Set (lsuc o ⊔ σ̅ σ .hom (ι₀ ⋆) = H.unit.η Δ⁺ # ι₀ ⋆ σ̅ σ .hom (ι₁ α) = H.M₁ ι₁-hom # (σ # (H.unit.η Δ # α)) σ̅ σ .hom (ι₂ α) = H.unit.η _ # ι₂ α - σ̅ σ .strict-mono {ι₀ ⋆} {ι₀ ⋆} _ = H⟨Δ⁺⟩.≤-refl , λ _ → refl - σ̅ σ .strict-mono {ι₁ α} {ι₁ β} α≤β = Σ-map₂ (ap ι₁ ⊙_) $ (H.M₁ ι₁-hom ∘ σ .morphism ∘ H.unit.η Δ) .strict-mono α≤β - σ̅ σ .strict-mono {ι₂ α} {ι₂ β} α≤β = H.unit.η Δ⁺ .strict-mono α≤β + σ̅ σ .pres-< {ι₀ ⋆} {ι₀ ⋆} _ = H⟨Δ⁺⟩.≤-refl , λ _ → refl + σ̅ σ .pres-< {ι₁ α} {ι₁ β} α≤β = Σ-map₂ (ap ι₁ ⊙_) $ (H.M₁ ι₁-hom ∘ σ .morphism ∘ H.unit.η Δ) .pres-< α≤β + σ̅ σ .pres-< {ι₂ α} {ι₂ β} α≤β = H.unit.η Δ⁺ .pres-< α≤β module _ where abstract σ̅-id : σ̅ SOrdᴴ.id ≡ H.unit.η Δ⁺ @@ -183,8 +187,8 @@ module _ {o r} (H : Hierarchy-theory o r) (Δ : Poset o r) (Ψ : Set (lsuc o ⊔ functor : Functor (Endos SOrdᴴ Fᴴ⟨ Δ ⟩) (Endos SOrdᴹᴰ Fᴹᴰ⟨ Disc Ψ ⟩) functor .Functor.F₀ _ = tt functor .Functor.F₁ σ .morphism .hom (α , d) = α , (T′ σ SOrdᴴ.∘ d) - functor .Functor.F₁ σ .morphism .strict-mono {α , d1} {β , d2} p = - let d1≤d2 , injr = 𝒟.left-strict-invariant {T′ σ} {d1} {d2} (⋉-snd-invariant p) in + functor .Functor.F₁ σ .morphism .pres-< {α , d1} {β , d2} p = + let d1≤d2 , injr = H⟨Δ⁺⟩→.left-strict-invariant {T′ σ} {d1} {d2} (⋉-snd-invariant p) in inc (biased (⋉-fst-invariant p) d1≤d2) , λ q i → fst (q i) , injr (ap snd q) i functor .Functor.F₁ σ .commutes = trivial! functor .Functor.F-id = ext λ (α , d) → @@ -210,8 +214,8 @@ module _ {o r} (H : Hierarchy-theory o r) (Δ : Poset o r) (Ψ : Set (lsuc o ⊔ Uᴴ : ∀ {X} → Functor (Endos SOrdᴴ X) SOrd↑ Uᴴ {X} .Functor.F₀ _ = Lift≤ _ _ (fst X) Uᴴ .Functor.F₁ σ .hom (lift α) = lift (σ # α) - Uᴴ .Functor.F₁ σ .strict-mono (lift α≤β) = - let σα≤σβ , inj = (σ .morphism) .strict-mono α≤β in + Uᴴ .Functor.F₁ σ .pres-< (lift α≤β) = + let σα≤σβ , inj = (σ .morphism) .pres-< α≤β in lift σα≤σβ , λ p → ap lift (inj (lift-inj p)) Uᴴ .Functor.F-id = ext λ _ → refl Uᴴ .Functor.F-∘ _ _ = ext λ _ → refl @@ -233,13 +237,13 @@ module _ {o r} (H : Hierarchy-theory o r) (Δ : Poset o r) (Ψ : Set (lsuc o ⊔ ℓ̅ ℓ .hom (ι₀ _) = H.M₁ ι₁-hom # ℓ ℓ̅ ℓ .hom (ι₁ α) = H.unit.η _ # ι₂ α ℓ̅ ℓ .hom (ι₂ α) = H.unit.η _ # ι₂ α - ℓ̅ ℓ .strict-mono {ι₀ ⋆} {ι₀ ⋆} _ = H⟨Δ⁺⟩.≤-refl , λ _ → refl - ℓ̅ ℓ .strict-mono {ι₁ α} {ι₁ β} α≤β = Σ-map₂ ((ap ι₁ ⊙ ι₂-inj) ⊙_) $ H.unit.η _ .strict-mono α≤β - ℓ̅ ℓ .strict-mono {ι₂ α} {ι₂ β} α≤β = H.unit.η _ .strict-mono α≤β + ℓ̅ ℓ .pres-< {ι₀ ⋆} {ι₀ ⋆} _ = H⟨Δ⁺⟩.≤-refl , λ _ → refl + ℓ̅ ℓ .pres-< {ι₁ α} {ι₁ β} α≤β = Σ-map₂ ((ap ι₁ ⊙ ι₂-inj) ⊙_) $ H.unit.η _ .pres-< α≤β + ℓ̅ ℓ .pres-< {ι₂ α} {ι₂ β} α≤β = H.unit.η _ .pres-< α≤β module _ where abstract ℓ̅-mono : ∀ {ℓ ℓ′} → ℓ′ H⟨Δ⟩.≤ ℓ → ∀ (α : ⌞ Δ⁺ ⌟) → ℓ̅ ℓ′ # α H⟨Δ⁺⟩.≤ ℓ̅ ℓ # α - ℓ̅-mono ℓ′≤ℓ (ι₀ _) = (mono (H.M₁ ι₁-hom) ℓ′≤ℓ) + ℓ̅-mono ℓ′≤ℓ (ι₀ _) = (pres-≤ (H.M₁ ι₁-hom) ℓ′≤ℓ) ℓ̅-mono ℓ′≤ℓ (ι₁ _) = H⟨Δ⁺⟩.≤-refl ℓ̅-mono ℓ′≤ℓ (ι₂ _) = H⟨Δ⁺⟩.≤-refl @@ -252,18 +256,18 @@ module _ {o r} (H : Hierarchy-theory o r) (Δ : Poset o r) (Ψ : Set (lsuc o ⊔ H.mult.η Δ⁺ # (H.M₁ (H.mult.η Δ⁺ ∘ H.M₁ (ℓ̅ ℓ)) # α) ∎ module _ where abstract - ν′-mono : ∀ {ℓ′ ℓ : ⌞ H.M₀ Δ ⌟} → ℓ′ H⟨Δ⟩.≤ ℓ → ν′ ℓ′ H⟨Δ⁺⟩→.≤ ν′ ℓ - ν′-mono {ℓ′} {ℓ} ℓ′≤ℓ .Lift.lower α = + ν′-mono : ∀ {ℓ′ ℓ : ⌞ H.M₀ Δ ⌟} → ℓ′ H⟨Δ⟩.≤ ℓ → ν′ ℓ′ H⟨Δ⁺⟩→-poset.≤ ν′ ℓ + ν′-mono {ℓ′} {ℓ} ℓ′≤ℓ .Lift.lower α = begin-≤[ lzero ] H.mult.η Δ⁺ # (H.M₁ (ℓ̅ ℓ′) # (H.unit.η Δ⁺ # α)) ≐⟨ ap (H.mult.η _ #_) (sym $ H.unit.is-natural _ _ (ℓ̅ ℓ′) #ₚ α) ⟩ - H.mult.η Δ⁺ # (H.unit.η (H.M₀ Δ⁺) # (ℓ̅ ℓ′ # α)) ≤⟨ mono (H.mult.η _ ∘ H.unit.η _) (ℓ̅-mono ℓ′≤ℓ α) ⟩ + H.mult.η Δ⁺ # (H.unit.η (H.M₀ Δ⁺) # (ℓ̅ ℓ′ # α)) ≤⟨ pres-≤ (H.mult.η _ ∘ H.unit.η _) (ℓ̅-mono ℓ′≤ℓ α) ⟩ H.mult.η Δ⁺ # (H.unit.η (H.M₀ Δ⁺) # (ℓ̅ ℓ # α)) ≐⟨ ap (H.mult.η _ #_) (H.unit.is-natural _ _ (ℓ̅ ℓ) #ₚ α) ⟩ H.mult.η Δ⁺ # (H.M₁ (ℓ̅ ℓ) # (H.unit.η Δ⁺ # α)) ≤∎ where - open Mugen.Order.Reasoning (H.M₀ Δ⁺) + open Reasoning (H.M₀ Δ⁺) module _ where abstract ν′-inj-on-related : ∀ {ℓ′ ℓ : ⌞ H.M₀ Δ ⌟} → ℓ′ H⟨Δ⟩.≤ ℓ → ν′ ℓ′ ≡ ν′ ℓ → ℓ′ ≡ ℓ - ν′-inj-on-related {ℓ′} {ℓ} ℓ′≤ℓ p = inj-on-related (H.mult.η _ ∘ H.unit.η _ ∘ H.M₁ ι₁-hom) ℓ′≤ℓ $ + ν′-inj-on-related {ℓ′} {ℓ} ℓ′≤ℓ p = injective-on-related (H.mult.η _ ∘ H.unit.η _ ∘ H.M₁ ι₁-hom) ℓ′≤ℓ $ H.mult.η Δ⁺ # (H.unit.η (H.M₀ Δ⁺) # (H.M₁ ι₁-hom # ℓ′)) ≡⟨ ap (H.mult.η _ #_) (H.unit.is-natural _ _ (ℓ̅ ℓ′) #ₚ _) ⟩ H.mult.η Δ⁺ # (H.M₁ (ℓ̅ ℓ′) # (H.unit.η Δ⁺ # ι₀ ⋆)) ≡⟨ ap (_# (H.unit.η _ # ι₀ ⋆)) p ⟩ H.mult.η Δ⁺ # (H.M₁ (ℓ̅ ℓ) # (H.unit.η Δ⁺ # ι₀ ⋆)) ≡˘⟨ ap (H.mult.η _ #_) (H.unit.is-natural _ _ (ℓ̅ ℓ) #ₚ _) ⟩ @@ -289,7 +293,7 @@ module _ {o r} (H : Hierarchy-theory o r) (Δ : Poset o r) (Ψ : Set (lsuc o ⊔ nt : Uᴴ => Uᴹᴰ F∘ T nt ._=>_.η _ .hom (lift ℓ) = pt , ν′ ℓ - nt ._=>_.η _ .strict-mono (lift ℓ≤ℓ′) = + nt ._=>_.η _ .pres-< (lift ℓ≤ℓ′) = inc (biased refl (ν′-mono ℓ≤ℓ′)) , λ p → ap lift $ ν′-inj-on-related ℓ≤ℓ′ (ap snd p) nt ._=>_.is-natural _ _ σ = ext λ (lift ℓ) → refl , λ α → diff --git a/src/Mugen/Cat/Monad.agda b/src/Mugen/Cat/Monad.agda index 3507515..592a887 100644 --- a/src/Mugen/Cat/Monad.agda +++ b/src/Mugen/Cat/Monad.agda @@ -4,7 +4,6 @@ open import Cat.Diagram.Monad import Cat.Reasoning as Cat open import Mugen.Prelude -open import Mugen.Order.Poset -------------------------------------------------------------------------------- -- Misc. Lemmas for Monads diff --git a/src/Mugen/Cat/README.md b/src/Mugen/Cat/README.md index ad40ecd..339fe31 100644 --- a/src/Mugen/Cat/README.md +++ b/src/Mugen/Cat/README.md @@ -1,4 +1,4 @@ # Categorical Properties -This directory formalizes various categorical results, focusing on the definition of [heirarchy theories](https://github.com/RedPRL/agda-mugen/blob/main/src/Mugen/Cat/HierarchyTheory.agda), -as well as the first steps towards proving that the McBride Heirarchy Theory is universal (See [`Mugen.Cat.HierarchyTheory.Properties`](https://github.com/RedPRL/agda-mugen/blob/main/src/Mugen/Cat/HierarchyTheory/Properties.agda)). +This directory formalizes various categorical results, focusing on the definition of [heirarchy theories](HierarchyTheory.agda), +as well as the first steps towards proving that the [McBride Heirarchy Theory is universal](HierarchyTheory/). diff --git a/src/Mugen/Cat/StrictOrders.agda b/src/Mugen/Cat/StrictOrders.agda index 0af438b..1039518 100644 --- a/src/Mugen/Cat/StrictOrders.agda +++ b/src/Mugen/Cat/StrictOrders.agda @@ -1,7 +1,7 @@ module Mugen.Cat.StrictOrders where open import Mugen.Prelude -open import Mugen.Order.Poset +open import Mugen.Order.StrictOrder private variable o r : Level @@ -18,21 +18,18 @@ Strict-orders o r .Hom = Strictly-monotone Strict-orders o r .Hom-set X Y = hlevel 2 Strict-orders o r .id = strictly-monotone-id Strict-orders o r ._∘_ = strictly-monotone-∘ -Strict-orders o r .idr f = ext (λ _ → refl) -Strict-orders o r .idl f = ext (λ _ → refl) -Strict-orders o r .assoc f g h = ext (λ _ → refl) +Strict-orders o r .idr f = ext λ _ → refl +Strict-orders o r .idl f = ext λ _ → refl +Strict-orders o r .assoc f g h = ext λ _ → refl Lift≤ : ∀ {o r} → (o′ r′ : Level) → Poset o r → Poset (o ⊔ o′) (r ⊔ r′) -Lift≤ o' r' X = to-poset mk where - open Poset X - - mk : make-poset _ (Lift o' ⌞ X ⌟) - mk .make-poset._≤_ x y = Lift r' (Lift.lower x ≤ Lift.lower y) - mk .make-poset.≤-refl = lift ≤-refl - mk .make-poset.≤-trans (lift p) (lift q) = lift (≤-trans p q) - mk .make-poset.≤-thin = Lift-is-hlevel 1 ≤-thin - mk .make-poset.≤-antisym (lift p) (lift q) = ap lift (≤-antisym p q) +Lift≤ o' r' X .Poset.Ob = Lift o' ⌞ X ⌟ +Lift≤ o' r' X .Poset._≤_ x y = Lift r' $ (X .Poset._≤_) (Lift.lower x) (Lift.lower y) +Lift≤ o' r' X .Poset.≤-thin = Lift-is-hlevel 1 $ X .Poset.≤-thin +Lift≤ o' r' X .Poset.≤-refl = lift $ X .Poset.≤-refl +Lift≤ o' r' X .Poset.≤-trans (lift p) (lift q) = lift (X .Poset.≤-trans p q) +Lift≤ o' r' X .Poset.≤-antisym (lift p) (lift q) = ap lift (X .Poset.≤-antisym p q) diff --git a/src/Mugen/Data/Int.agda b/src/Mugen/Data/Int.agda index 4353cd5..2a4e602 100644 --- a/src/Mugen/Data/Int.agda +++ b/src/Mugen/Data/Int.agda @@ -1,10 +1,10 @@ module Mugen.Data.Int where -open import Data.Int.Inductive +open import Data.Nat open import Mugen.Prelude -open import Mugen.Order.Poset -open import Mugen.Data.Nat + +open import Data.Int.Inductive public -------------------------------------------------------------------------------- -- General Facts @@ -111,41 +111,41 @@ abstract +ℤ-pos zero y = refl +ℤ-pos (suc x) y = ap suc-int $ +ℤ-pos x y - negate-inj : ∀ x y → (- x) ≡ (- y) → x ≡ y - negate-inj zero zero p = refl - negate-inj zero (suc y) p = absurd (pos≠negsuc p) - negate-inj (suc x) zero p = absurd (pos≠negsuc (sym p)) - negate-inj (suc x) (suc y) p = ap suc (negsuc-injective p) - - suc-int-inj : ∀ x y → suc-int x ≡ suc-int y → x ≡ y - suc-int-inj (pos _) (pos _) p = ap pred-int p - suc-int-inj (pos _) (negsuc zero) p = ap pred-int p - suc-int-inj (pos _) (negsuc (suc _)) p = ap pred-int p - suc-int-inj (negsuc zero) (pos _) p = ap pred-int p - suc-int-inj (negsuc zero) (negsuc zero) p = ap pred-int p - suc-int-inj (negsuc zero) (negsuc (suc _)) p = ap pred-int p - suc-int-inj (negsuc (suc _)) (pos _) p = ap pred-int p - suc-int-inj (negsuc (suc _)) (negsuc zero) p = ap pred-int p - suc-int-inj (negsuc (suc _)) (negsuc (suc _)) p = ap pred-int p - - pred-int-inj : ∀ x y → pred-int x ≡ pred-int y → x ≡ y - pred-int-inj (pos zero) (pos zero) p = ap suc-int p - pred-int-inj (pos zero) (pos (suc _)) p = ap suc-int p - pred-int-inj (pos zero) (negsuc _) p = ap suc-int p - pred-int-inj (pos (suc _)) (pos zero) p = ap suc-int p - pred-int-inj (pos (suc _)) (pos (suc _)) p = ap suc-int p - pred-int-inj (pos (suc _)) (negsuc _) p = ap suc-int p - pred-int-inj (negsuc _) (pos zero) p = ap suc-int p - pred-int-inj (negsuc _) (pos (suc _)) p = ap suc-int p - pred-int-inj (negsuc _) (negsuc _) p = ap suc-int p - - +ℤ-injr : ∀ k x y → k +ℤ x ≡ k +ℤ y → x ≡ y - +ℤ-injr (pos zero) x y p = p - +ℤ-injr (pos (suc k)) x y p = - +ℤ-injr (pos k) x y $ suc-int-inj (pos k +ℤ x) (pos k +ℤ y) p - +ℤ-injr (negsuc zero) x y p = pred-int-inj x y p - +ℤ-injr (negsuc (suc k)) x y p = - +ℤ-injr (negsuc k) x y $ pred-int-inj (negsuc k +ℤ x) (negsuc k +ℤ y) p + negate-injective : ∀ x y → (- x) ≡ (- y) → x ≡ y + negate-injective zero zero p = refl + negate-injective zero (suc y) p = absurd (pos≠negsuc p) + negate-injective (suc x) zero p = absurd (pos≠negsuc (sym p)) + negate-injective (suc x) (suc y) p = ap suc (negsuc-injective p) + + suc-int-injective : ∀ x y → suc-int x ≡ suc-int y → x ≡ y + suc-int-injective (pos _) (pos _) p = ap pred-int p + suc-int-injective (pos _) (negsuc zero) p = ap pred-int p + suc-int-injective (pos _) (negsuc (suc _)) p = ap pred-int p + suc-int-injective (negsuc zero) (pos _) p = ap pred-int p + suc-int-injective (negsuc zero) (negsuc zero) p = ap pred-int p + suc-int-injective (negsuc zero) (negsuc (suc _)) p = ap pred-int p + suc-int-injective (negsuc (suc _)) (pos _) p = ap pred-int p + suc-int-injective (negsuc (suc _)) (negsuc zero) p = ap pred-int p + suc-int-injective (negsuc (suc _)) (negsuc (suc _)) p = ap pred-int p + + pred-int-injective : ∀ x y → pred-int x ≡ pred-int y → x ≡ y + pred-int-injective (pos zero) (pos zero) p = ap suc-int p + pred-int-injective (pos zero) (pos (suc _)) p = ap suc-int p + pred-int-injective (pos zero) (negsuc _) p = ap suc-int p + pred-int-injective (pos (suc _)) (pos zero) p = ap suc-int p + pred-int-injective (pos (suc _)) (pos (suc _)) p = ap suc-int p + pred-int-injective (pos (suc _)) (negsuc _) p = ap suc-int p + pred-int-injective (negsuc _) (pos zero) p = ap suc-int p + pred-int-injective (negsuc _) (pos (suc _)) p = ap suc-int p + pred-int-injective (negsuc _) (negsuc _) p = ap suc-int p + + +ℤ-injectiver : ∀ k x y → k +ℤ x ≡ k +ℤ y → x ≡ y + +ℤ-injectiver (pos zero) x y p = p + +ℤ-injectiver (pos (suc k)) x y p = + +ℤ-injectiver (pos k) x y $ suc-int-injective (pos k +ℤ x) (pos k +ℤ y) p + +ℤ-injectiver (negsuc zero) x y p = pred-int-injective x y p + +ℤ-injectiver (negsuc (suc k)) x y p = + +ℤ-injectiver (negsuc k) x y $ pred-int-injective (negsuc k +ℤ x) (negsuc k +ℤ y) p -------------------------------------------------------------------------------- -- Order @@ -156,14 +156,11 @@ pos x ≤ℤ negsuc y = ⊥ negsuc x ≤ℤ pos y = ⊤ negsuc x ≤ℤ negsuc y = y ≤ x -_<ℤ_ : Int → Int → Type -_<ℤ_ = strict _≤ℤ_ - -≤ℤ-refl : ∀ x → x ≤ℤ x -≤ℤ-refl (pos x) = ≤-refl -≤ℤ-refl (negsuc x) = ≤-refl - abstract + ≤ℤ-refl : ∀ x → x ≤ℤ x + ≤ℤ-refl (pos x) = ≤-refl + ≤ℤ-refl (negsuc x) = ≤-refl + ≤ℤ-trans : ∀ x y z → x ≤ℤ y → y ≤ℤ z → x ≤ℤ z ≤ℤ-trans (pos x) (pos y) (pos z) x≤y y≤z = ≤-trans x≤y y≤z ≤ℤ-trans (negsuc x) (pos y) (pos z) x≤y y≤z = tt @@ -245,15 +242,14 @@ abstract negate-anti-mono zero zero _ = 0≤x negate-anti-mono zero (suc y) x≤y = tt negate-anti-mono (suc x) (suc y) (s≤s x≤y) = x≤y - -------------------------------------------------------------------------------- --- Bundles - -ℤ-Strict-order : Poset lzero lzero -ℤ-Strict-order = to-poset mk where - mk : make-poset _ _ - mk .make-poset._≤_ = _≤ℤ_ - mk .make-poset.≤-refl = ≤ℤ-refl _ - mk .make-poset.≤-trans = ≤ℤ-trans _ _ _ - mk .make-poset.≤-thin = ≤ℤ-is-prop _ _ - mk .make-poset.≤-antisym = ≤ℤ-antisym _ _ + + negate-anti-full : ∀ x y → (- y) ≤ℤ (- x) → x ≤ y + negate-anti-full zero _ _ = 0≤x + negate-anti-full (suc x) zero () + negate-anti-full (suc x) (suc y) x≤y = (s≤s x≤y) + + negate-min : ∀ x y → - (min x y) ≡ maxℤ (- x) (- y) + negate-min zero zero = refl + negate-min zero (suc y) = refl + negate-min (suc x) zero = refl + negate-min (suc x) (suc y) = refl diff --git a/src/Mugen/Data/Nat.agda b/src/Mugen/Data/Nat.agda deleted file mode 100644 index edf9581..0000000 --- a/src/Mugen/Data/Nat.agda +++ /dev/null @@ -1,66 +0,0 @@ -module Mugen.Data.Nat where - -open import Algebra.Magma -open import Algebra.Monoid -open import Algebra.Semigroup - -open import Mugen.Prelude hiding (Nat-is-set) -open import Mugen.Order.Poset - -open import Data.Nat public - - --------------------------------------------------------------------------------- --- Algebra - -+-is-magma : is-magma _+_ -+-is-magma .has-is-set = Nat-is-set - -+-is-semigroup : is-semigroup _+_ -+-is-semigroup .has-is-magma = +-is-magma -+-is-semigroup .associative {x} {y} {z} = +-associative x y z - -+-0-is-monoid : is-monoid 0 _+_ -+-0-is-monoid .has-is-semigroup = +-is-semigroup -+-0-is-monoid .idl {x} = refl -+-0-is-monoid .idr {x} = +-zeror x - --------------------------------------------------------------------------------- --- Order - -≡→≤ : ∀ {x y} → x ≡ y → x ≤ y -≡→≤ {x = zero} {y = y} p = 0≤x -≡→≤ {x = suc x} {y = zero} p = absurd (suc≠zero p) -≡→≤ {x = suc x} {y = suc y} p = s≤s (≡→≤ (suc-inj p)) - -≤-is-partial-order : is-partial-order _≤_ -≤-is-partial-order .is-partial-order.≤-refl = ≤-refl -≤-is-partial-order .is-partial-order.≤-trans = ≤-trans -≤-is-partial-order .is-partial-order.≤-thin = ≤-is-prop -≤-is-partial-order .is-partial-order.≤-antisym = ≤-antisym - -max-zerol : ∀ x → max 0 x ≡ x -max-zerol zero = refl -max-zerol (suc x) = refl - -max-zeror : ∀ x → max x 0 ≡ x -max-zeror zero = refl -max-zeror (suc x) = refl - -max-is-lub : ∀ x y z → x ≤ z → y ≤ z → max x y ≤ z -max-is-lub zero zero z 0≤x 0≤x = 0≤x -max-is-lub zero (suc y) (suc z) 0≤x (s≤s q) = s≤s q -max-is-lub (suc x) zero (suc z) (s≤s p) 0≤x = s≤s p -max-is-lub (suc x) (suc y) (suc z) (s≤s p) (s≤s q) = s≤s (max-is-lub x y z p q) - -min-is-glb : ∀ x y z → z ≤ x → z ≤ y → z ≤ min x y -min-is-glb x y zero 0≤x 0≤x = 0≤x -min-is-glb (suc x) (suc y) (suc z) (s≤s p) (s≤s q) = s≤s (min-is-glb x y z p q) - --------------------------------------------------------------------------------- --- Bundles - -Nat≤ : Poset lzero lzero -Nat≤ .Poset.Ob = Nat -Nat≤ .Poset.poset-on .Poset-on._≤_ = _≤_ -Nat≤ .Poset.poset-on .Poset-on.has-is-poset = ≤-is-partial-order diff --git a/src/Mugen/Everything.agda b/src/Mugen/Everything.agda index 1089322..78f9b1a 100644 --- a/src/Mugen/Everything.agda +++ b/src/Mugen/Everything.agda @@ -4,19 +4,21 @@ module Mugen.Everything where import Mugen.Algebra.Displacement -import Mugen.Algebra.Displacement.Constant -import Mugen.Algebra.Displacement.Endomorphism -import Mugen.Algebra.Displacement.FiniteSupport -import Mugen.Algebra.Displacement.Fractal -import Mugen.Algebra.Displacement.IndexedProduct -import Mugen.Algebra.Displacement.Int -import Mugen.Algebra.Displacement.Lexicographic -import Mugen.Algebra.Displacement.Nat -import Mugen.Algebra.Displacement.NearlyConstant -import Mugen.Algebra.Displacement.NonPositive -import Mugen.Algebra.Displacement.Opposite -import Mugen.Algebra.Displacement.Prefix -import Mugen.Algebra.Displacement.Product +import Mugen.Algebra.Displacement.Action +import Mugen.Algebra.Displacement.Instances.Constant +import Mugen.Algebra.Displacement.Instances.Endomorphism +import Mugen.Algebra.Displacement.Instances.Fractal +import Mugen.Algebra.Displacement.Instances.IndexedProduct +import Mugen.Algebra.Displacement.Instances.Int +import Mugen.Algebra.Displacement.Instances.Lexicographic +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 import Mugen.Algebra.OrderedMonoid import Mugen.Cat.Endomorphisms import Mugen.Cat.HierarchyTheory @@ -26,14 +28,24 @@ import Mugen.Cat.Monad import Mugen.Cat.StrictOrders import Mugen.Data.Int import Mugen.Data.List -import Mugen.Data.Nat import Mugen.Data.NonEmpty -import Mugen.Order.Coproduct -import Mugen.Order.Discrete -import Mugen.Order.LeftInvariantRightCentered -import Mugen.Order.Opposite -import Mugen.Order.Poset -import Mugen.Order.Prefix +import Mugen.Order.Instances.BasedSupport +import Mugen.Order.Instances.Coproduct +import Mugen.Order.Instances.Discrete +import Mugen.Order.Instances.Endomorphism +import Mugen.Order.Instances.Fractal +import Mugen.Order.Instances.Int +import Mugen.Order.Instances.LeftInvariantRightCentered +import Mugen.Order.Instances.Lexicographic +import Mugen.Order.Instances.Nat +import Mugen.Order.Instances.NonPositive +import Mugen.Order.Instances.Opposite +import Mugen.Order.Instances.Pointwise +import Mugen.Order.Instances.Prefix +import Mugen.Order.Instances.Product +import Mugen.Order.Instances.Singleton +import Mugen.Order.Instances.Support +import Mugen.Order.Lattice import Mugen.Order.Reasoning -import Mugen.Order.Singleton +import Mugen.Order.StrictOrder import Mugen.Prelude diff --git a/src/Mugen/Order/Coproduct.agda b/src/Mugen/Order/Coproduct.agda deleted file mode 100644 index 897017b..0000000 --- a/src/Mugen/Order/Coproduct.agda +++ /dev/null @@ -1,60 +0,0 @@ -module Mugen.Order.Coproduct where - -open import Mugen.Prelude -open import Mugen.Order.Poset - --- NOTE: We require that both 'A' and 'B' live in the same universe --- to avoid large amounts of 'Lift'. If you need to take the coproduct --- of two partial orders that live in different universes, perform a lift --- on the partial order before taking the coproduct. -module Poset-coproduct - {o r} - (A B : Poset o r) - where - private - module A = Poset A - module B = Poset B - - _⊕≤_ : (⌞ A ⌟ ⊎ ⌞ B ⌟) → (⌞ A ⌟ ⊎ ⌞ B ⌟) → Type r - inl x ⊕≤ inl y = x A.≤ y - inl x ⊕≤ inr y = Lift _ ⊥ - inr x ⊕≤ inl y = Lift _ ⊥ - inr x ⊕≤ inr y = x B.≤ y - - ⊕≤-thin : ∀ x y → is-prop (x ⊕≤ y) - ⊕≤-thin (inl _) (inl _) = A.≤-thin - ⊕≤-thin (inl _) (inr _) = hlevel 1 - ⊕≤-thin (inr _) (inl _) = hlevel 1 - ⊕≤-thin (inr _) (inr _) = B.≤-thin - - ⊕≤-refl : ∀ x → x ⊕≤ x - ⊕≤-refl (inl x) = A.≤-refl - ⊕≤-refl (inr x) = B.≤-refl - - ⊕≤-trans : ∀ x y z → x ⊕≤ y → y ⊕≤ z → x ⊕≤ z - ⊕≤-trans (inl x) (inl y) (inl z) p q = A.≤-trans p q - ⊕≤-trans (inr x) (inr y) (inr z) p q = B.≤-trans p q - - ⊕≤-antisym : ∀ x y → x ⊕≤ y → y ⊕≤ x → x ≡ y - ⊕≤-antisym (inl _) (inl _) p q = ap inl $ A.≤-antisym p q - ⊕≤-antisym (inl _) (inr _) () - ⊕≤-antisym (inr _) (inl _) () - ⊕≤-antisym (inr _) (inr _) p q = ap inr $ B.≤-antisym p q - - - ⊕≤-is-partial-order : is-partial-order _⊕≤_ - ⊕≤-is-partial-order .is-partial-order.≤-refl {x} = ⊕≤-refl x - ⊕≤-is-partial-order .is-partial-order.≤-trans {x} {y} {z} = ⊕≤-trans x y z - ⊕≤-is-partial-order .is-partial-order.≤-thin {x} {y} = ⊕≤-thin x y - ⊕≤-is-partial-order .is-partial-order.≤-antisym {x} {y} = ⊕≤-antisym x y - -module _ {o r} (A B : Poset o r) where - private - module A = Poset A - module B = Poset B - open Poset-coproduct A B - - _⊕_ : Poset o r - _⊕_ .Poset.Ob = ⌞ A ⌟ ⊎ ⌞ B ⌟ - .Poset.poset-on ⊕ .Poset-on._≤_ = _⊕≤_ - .Poset.poset-on ⊕ .Poset-on.has-is-poset = ⊕≤-is-partial-order diff --git a/src/Mugen/Order/Discrete.agda b/src/Mugen/Order/Discrete.agda deleted file mode 100644 index 0c736a7..0000000 --- a/src/Mugen/Order/Discrete.agda +++ /dev/null @@ -1,14 +0,0 @@ -module Mugen.Order.Discrete where - -open import Mugen.Prelude - -open import Mugen.Order.Poset - --- We do this entirely with copatterns for performance reasons. -Disc : ∀ {o} → (A : Set o) → Poset o o -Disc A .Poset.Ob = ⌞ A ⌟ -Disc {o = o} A .Poset.poset-on .Poset-on._≤_ x y = (x ≡ y) -Disc A .Poset.poset-on .Poset-on.has-is-poset .is-partial-order.≤-thin = hlevel! -Disc A .Poset.poset-on .Poset-on.has-is-poset .is-partial-order.≤-refl = refl -Disc A .Poset.poset-on .Poset-on.has-is-poset .is-partial-order.≤-trans = _∙_ -Disc A .Poset.poset-on .Poset-on.has-is-poset .is-partial-order.≤-antisym p _ = p diff --git a/src/Mugen/Order/Instances/BasedSupport.agda b/src/Mugen/Order/Instances/BasedSupport.agda new file mode 100644 index 0000000..d5c009b --- /dev/null +++ b/src/Mugen/Order/Instances/BasedSupport.agda @@ -0,0 +1,372 @@ +-- vim: nowrap +module Mugen.Order.Instances.BasedSupport where + +open import Mugen.Prelude +open import Mugen.Data.List +open import Mugen.Order.Lattice +open import Mugen.Order.StrictOrder +open import Mugen.Order.Instances.Pointwise + +import Mugen.Order.Reasoning as Reasoning + +private variable + o o' r r' : Level + +-------------------------------------------------------------------------------- +-- Nearly Constant Functions +-- Section 3.3.5 +-- +-- A "nearly constant function" is a function 'f : Nat → 𝒟' +-- that differs from some fixed 'base : 𝒟' for only +-- a finite set of 'n : Nat' +-- +-- We represent these via prefix lists. IE: the function +-- +-- > λ n → if n = 1 then 2 else if n = 3 then 1 else 5 +-- +-- will be represented as a pair (5, [5,2,5,3]). We will call the +-- first element of this pair "the base" of the function, and the +-- prefix list "the support". +-- +-- However, there is a slight problem here when we go to show that +-- this is a subalgebra of 'IdxProd': it's not injective! The problem +-- occurs when you have trailing base elements, meaning 2 lists can +-- denote the same function! +-- +-- To resolve this, we say that a list is compact relative +-- to some 'base : 𝒟' if it does not have any trailing base's. +-- We then only work with compact lists in our displacement algebra. + +-------------------------------------------------------------------------------- +-- Raw Support Lists +-- + +record RawList (A : Type o) : Type o where + constructor raw + field + elts : List A + base : A +open RawList + +raw-path : ∀ {A : Type o} {xs ys : RawList A} + → xs .elts ≡ ys .elts + → xs .base ≡ ys .base + → xs ≡ ys +raw-path p q i .elts = p i +raw-path p q i .base = q i + +-- Lemmas about hlevel +module _ {A : Type o} where + abstract + RawList-is-hlevel : (n : Nat) → is-hlevel A (2 + n) → is-hlevel (RawList A) (2 + n) + RawList-is-hlevel n A-is-hlevel = + is-hlevel≃ (2 + n) (Iso→Equiv raw-eqv) $ + ×-is-hlevel (2 + n) (ListPath.List-is-hlevel n A-is-hlevel) A-is-hlevel + where + unquoteDecl raw-eqv = declare-record-iso raw-eqv (quote RawList) + + instance + decomp-RawList : hlevel-decomposition (RawList A) + decomp-RawList = decomp (quote RawList-is-hlevel) (`level-minus 2 ∷ `search ∷ []) + +-- Operations and properties for raw support lists +module Raw {A : Type o} where + private + _raw∷_ : A → RawList A → RawList A + x raw∷ (raw xs b) = raw (x ∷ xs) b + + -- Indexing function that turns a list into a map 'Nat → A' + index : RawList A → (Nat → A) + index (raw [] b) n = b + index (raw (x ∷ xs) b) zero = x + index (raw (x ∷ xs) b) (suc n) = index (raw xs b) n + + -------------------------------------------------------------------------------- + -- Compactness of Raw Lists + + is-compact : RawList A → Type o + is-compact (raw [] b) = Lift o ⊤ + is-compact (raw (x ∷ []) b) = ¬ (x ≡ b) + is-compact (raw (_ ∷ y ∷ ys) b) = is-compact (raw (y ∷ ys) b) + + abstract + is-compact-is-prop : ∀ xs → is-prop (is-compact xs) + is-compact-is-prop (raw [] _) = hlevel 1 + is-compact-is-prop (raw (_ ∷ []) _) = hlevel 1 + is-compact-is-prop (raw (_ ∷ y ∷ ys) _) = is-compact-is-prop (raw (y ∷ ys) _) + + abstract + tail-is-compact : ∀ x xs → is-compact (x raw∷ xs) → is-compact xs + tail-is-compact x (raw [] _) _ = lift tt + tail-is-compact x (raw (y ∷ ys) _) compact = compact + + abstract + private + base-singleton-isnt-compact : ∀ {x xs b} → x ≡ b → xs ≡ raw [] b → is-compact (x raw∷ xs) → ⊥ + base-singleton-isnt-compact {xs = raw [] _} x=b xs=[] is-compact = is-compact $ x=b ∙ sym (ap base xs=[]) + base-singleton-isnt-compact {xs = raw (_ ∷ _) _} x=b xs=[] is-compact = ∷≠[] $ ap elts xs=[] + + -------------------------------------------------------------------------------- + -- Compacting of Raw Lists + + module _ ⦃ _ : Discrete A ⦄ where + module _ (b : A) where + compact-list-step : A → List A → List A + compact-list-step x [] with x ≡? b + ... | yes _ = [] + ... | no _ = x ∷ [] + compact-list-step x (y ∷ ys) = x ∷ y ∷ ys + + compact-list : List A → List A + compact-list [] = [] + compact-list (x ∷ xs) = compact-list-step x (compact-list xs) + + compact-step : A → RawList A → RawList A + compact-step x (raw xs b) = raw (compact-list-step b x xs) b + + compact : RawList A → RawList A + compact (raw xs b) = raw (compact-list b xs) b + + abstract + compact-compacted : ∀ {xs} → is-compact xs → compact xs ≡ xs + compact-compacted {xs = raw [] _} _ = refl + compact-compacted {xs = raw (x ∷ []) b} x≠b with x ≡? b + ... | yes x=b = absurd (x≠b x=b) + ... | no _ = refl + compact-compacted {xs = raw (x ∷ y ∷ ys) b} is-compact = + ap (compact-step x) $ compact-compacted {xs = raw (y ∷ ys) b} is-compact + + -- the result of 'compact' is a compact list + abstract + private + compact-step-is-compact : ∀ x xs + → is-compact xs + → is-compact (compact-step x xs) + compact-step-is-compact x (raw [] b) _ with x ≡? b + ... | yes _ = lift tt + ... | no x≠b = x≠b + compact-step-is-compact x (raw (y ∷ ys) b) is-compact = is-compact + + compact-is-compact : ∀ xs → is-compact (compact xs) + compact-is-compact (raw [] _) = lift tt + compact-is-compact (raw (x ∷ xs) b) = + compact-step-is-compact x (compact (raw xs b)) (compact-is-compact (raw xs b)) + + -------------------------------------------------------------------------------- + -- Lemmas about Indexing and Compacting + -- + -- Compacting a raw list does not change its indexed values. + + module _ ⦃ _ : Discrete A ⦄ where + abstract + private + index-compact-step-zero : ∀ x xs + → index (compact-step x xs) zero ≡ x + index-compact-step-zero x (raw [] b) with x ≡? b + ... | yes x=b = sym x=b + ... | no _ = refl + index-compact-step-zero x (raw (_ ∷ _) _) = refl + + index-compact-step-suc : ∀ x xs n + → index (compact-step x xs) (suc n) ≡ index xs n + index-compact-step-suc x (raw [] b) n with x ≡? b + ... | yes _ = refl + ... | no _ = refl + index-compact-step-suc x (raw (_ ∷ _) _) n = refl + + index-compact : ∀ xs n → index (compact xs) n ≡ index xs n + index-compact (raw [] _) n = refl + index-compact (raw (x ∷ xs) b) zero = + index-compact-step-zero x (compact (raw xs b)) + index-compact (raw (x ∷ xs) b) (suc n) = + index (compact-step x (compact (raw xs b))) (suc n) + ≡⟨ index-compact-step-suc x (compact (raw xs b)) n ⟩ + index (compact (raw xs b)) n + ≡⟨ index-compact (raw xs b) n ⟩ + index (raw xs b) n + ∎ + + -------------------------------------------------------------------------------- + -- Merging Lists + + merge-list-with : (A → A → A) → RawList A → RawList A → List A + merge-list-with _⊚_ (raw [] b1) (raw [] b2) = [] + merge-list-with _⊚_ (raw [] b1) (raw (y ∷ ys) b2) = (b1 ⊚ y) ∷ merge-list-with _⊚_ (raw [] b1) (raw ys b2) + merge-list-with _⊚_ (raw (x ∷ xs) b1) (raw [] b2) = (x ⊚ b2) ∷ merge-list-with _⊚_ (raw xs b1) (raw [] b2) + merge-list-with _⊚_ (raw (x ∷ xs) b1) (raw (y ∷ ys) b2) = (x ⊚ y) ∷ merge-list-with _⊚_ (raw xs b1) (raw ys b2) + + merge-with : (A → A → A) → RawList A → RawList A → RawList A + merge-with _⊚_ xs ys = raw (merge-list-with _⊚_ xs ys) (xs .base ⊚ ys .base) + + abstract + index-merge-with : ∀ f xs ys n → index (merge-with f xs ys) n ≡ f (index xs n) (index ys n) + index-merge-with f (raw [] b1) (raw [] b2) n = refl + index-merge-with f (raw [] b1) (raw (y ∷ ys) b2) zero = refl + index-merge-with f (raw [] b1) (raw (y ∷ ys) b2) (suc n) = index-merge-with f (raw [] b1) (raw ys b2) n + index-merge-with f (raw (x ∷ xs) b1) (raw [] b2) zero = refl + index-merge-with f (raw (x ∷ xs) b1) (raw [] b2) (suc n) = index-merge-with f (raw xs b1) (raw [] b2) n + index-merge-with f (raw (x ∷ xs) b1) (raw (y ∷ ys) b2) zero = refl + index-merge-with f (raw (x ∷ xs) b1) (raw (y ∷ ys) b2) (suc n) = index-merge-with f (raw xs b1) (raw ys b2) n + + -------------------------------------------------------------------------------- + -- Order + + -- 'index' is injective for compacted lists + abstract + index-compacted-injective : ∀ xs ys + → is-compact xs + → is-compact ys + → ((n : Nat) → index xs n ≡ index ys n) + → xs ≡ ys + index-compacted-injective (raw [] b1) (raw [] b2) _ _ p = raw-path refl (p 0) + index-compacted-injective (raw (x ∷ xs) b1) (raw [] b2) x∷xs-compact []-compact p = + let xs-compact = tail-is-compact x (raw xs b1) x∷xs-compact in + let xs=[] = index-compacted-injective (raw xs b1) (raw [] b2) xs-compact []-compact (p ⊙ suc) in + absurd (base-singleton-isnt-compact (p 0) xs=[] x∷xs-compact) + index-compacted-injective (raw [] b1) (raw (y ∷ ys) b2) []-compact y∷ys-compact p = + let ys-compact = tail-is-compact y (raw ys b2) y∷ys-compact in + let []=ys = index-compacted-injective (raw [] b1) (raw ys b2) []-compact ys-compact (p ⊙ suc) in + absurd $ᵢ base-singleton-isnt-compact (sym (p 0)) (sym []=ys) y∷ys-compact + index-compacted-injective (raw (x ∷ xs) b1) (raw (y ∷ ys) b2) x∷xs-compact y∷ys-compact p = + let xs-compact = tail-is-compact x (raw xs b1) x∷xs-compact in + let ys-compact = tail-is-compact y (raw ys b2) y∷ys-compact in + let xs=ys = index-compacted-injective (raw xs b1) (raw ys b2) xs-compact ys-compact (p ⊙ suc) in + ap₂ _raw∷_ (p 0) xs=ys + +-------------------------------------------------------------------------------- +-- These will be the actual elements of our displacement algebra. +-- A support list is a compact raw list. + +record BasedSupportList (A : Type o) : Type o where + constructor based-support-list + no-eta-equality + field + list : RawList A + has-is-compact : Raw.is-compact list + open RawList list public + +module _ {A : Type o} where + open BasedSupportList + + -- Paths in support lists are determined by paths between the bases + paths between the elements. + abstract + based-support-list-path : ∀ {xs ys : BasedSupportList A} → xs .list ≡ ys .list → xs ≡ ys + based-support-list-path p i .list = p i + based-support-list-path {xs = xs} {ys = ys} p i .has-is-compact = + is-prop→pathp (λ i → Raw.is-compact-is-prop (p i)) (xs .has-is-compact) (ys .has-is-compact) i + + BasedSupportList-is-hlevel : (n : Nat) + → is-hlevel A (2 + n) → is-hlevel (BasedSupportList A) (2 + n) + BasedSupportList-is-hlevel n A-is-hlevel = + is-hlevel≃ (2 + n) (Iso→Equiv eqv) $ + Σ-is-hlevel (2 + n) (RawList-is-hlevel n A-is-hlevel) λ xs → + is-prop→is-hlevel-suc {n = 1 + n} (Raw.is-compact-is-prop xs) + where + unquoteDecl eqv = declare-record-iso eqv (quote BasedSupportList) + + instance + decomp-BasedSupportList : hlevel-decomposition (BasedSupportList A) + decomp-BasedSupportList = decomp (quote BasedSupportList-is-hlevel) (`level-minus 2 ∷ `search ∷ []) + + index : BasedSupportList A → (Nat → A) + index xs = Raw.index (xs .list) + + module _ ⦃ _ : Discrete A ⦄ where + merge-with : (A → A → A) → BasedSupportList A → BasedSupportList A → BasedSupportList A + merge-with f xs ys .list = Raw.compact $ Raw.merge-with f (xs .list) (ys .list) + merge-with f xs ys .has-is-compact = Raw.compact-is-compact $ Raw.merge-with f (xs .list) (ys .list) + + -- 'index' commutes with 'merge' + abstract + index-merge-with : ∀ f xs ys + → index (merge-with f xs ys) ≡ pointwise-map₂ (λ _ x y → f x y) (index xs) (index ys) + index-merge-with f xs ys = funext λ n → + Raw.index-compact (Raw.merge-with f (xs .list) (ys .list)) n + ∙ Raw.index-merge-with f (xs .list) (ys .list) n + + abstract + index-injective : ∀ {xs ys} → index xs ≡ index ys → xs ≡ ys + index-injective {xs} {ys} p = based-support-list-path $ + Raw.index-compacted-injective _ _ (xs .has-is-compact) (ys .has-is-compact) $ + happly p + +module _ (A : Poset o r) where + private + rep : represents-full-subposet (Pointwise Nat (λ _ → A)) index + rep .represents-full-subposet.injective = index-injective + module rep = represents-full-subposet rep + + BasedSupport : Poset o r + BasedSupport = rep.poset + + BasedSupport→Pointwise : Strictly-monotone BasedSupport (Pointwise Nat (λ _ → A)) + BasedSupport→Pointwise = rep.strictly-monotone + + BasedSupport→Pointwise-is-full-subposet : is-full-subposet BasedSupport→Pointwise + BasedSupport→Pointwise-is-full-subposet = rep.has-is-full-subposet + +-------------------------------------------------------------------------------- +-- Joins + +module _ + {A : Poset o r} + ⦃ _ : Discrete ⌞ A ⌟ ⦄ + (A-has-joins : has-joins A) + where + private + module A = Reasoning A + module P = Reasoning (Pointwise Nat λ _ → A) + module A-has-joins = has-joins A-has-joins + P-has-joins = Pointwise-has-joins Nat λ _ → A-has-joins + module P-has-joins = has-joins P-has-joins + + rep : represents-full-subsemilattice P-has-joins (BasedSupport→Pointwise-is-full-subposet A) + rep .represents-full-subsemilattice.join = merge-with A-has-joins.join + rep .represents-full-subsemilattice.pres-join {x} {y} = index-merge-with A-has-joins.join x y + module rep = represents-full-subsemilattice rep + + BasedSupport-has-joins : has-joins (BasedSupport A) + BasedSupport-has-joins = rep.joins + + BasedSupport→Pointwise-is-full-subsemilattice + : is-full-subsemilattice BasedSupport-has-joins P-has-joins (BasedSupport→Pointwise A) + BasedSupport→Pointwise-is-full-subsemilattice = rep.has-is-full-subsemilattice + +-------------------------------------------------------------------------------- +-- Bottoms + +module _ + (A : Poset o r) + ⦃ _ : Discrete ⌞ A ⌟ ⦄ + (A-has-bottom : has-bottom A) + where + private + module A = Reasoning A + module P = Reasoning (Pointwise Nat λ _ → A) + module A-has-bottom = has-bottom A-has-bottom + P-has-bottom = Pointwise-has-bottom Nat λ _ → A-has-bottom + module P-has-bottom = has-bottom P-has-bottom + + rep : represents-full-bounded-subposet P-has-bottom (BasedSupport→Pointwise-is-full-subposet A) + rep .represents-full-bounded-subposet.bot = based-support-list (raw [] A-has-bottom.bot) (lift tt) + rep .represents-full-bounded-subposet.pres-bot = refl + module rep = represents-full-bounded-subposet rep + + BasedSupport-has-bottom : has-bottom (BasedSupport A) + BasedSupport-has-bottom = rep.bottom + + BasedSupport→Pointwise-is-full-bounded-subposet + : is-full-bounded-subposet BasedSupport-has-bottom P-has-bottom (BasedSupport→Pointwise A) + BasedSupport→Pointwise-is-full-bounded-subposet = rep.has-is-full-bounded-subposet + +-------------------------------------------------------------------------------- +-- Extensionality + +module _ {A : Type o} ⦃ _ : H-Level A 2 ⦄ {ℓr} ⦃ s : Extensional (Nat → ⌞ A ⌟) ℓr ⦄ where + + Extensional-BasedSupportList : Extensional (BasedSupportList ⌞ A ⌟) ℓr + Extensional-BasedSupportList = injection→extensional! index-injective s + + instance + extensionality-based-support-list : Extensionality (BasedSupportList ⌞ A ⌟) + extensionality-based-support-list = record { lemma = quote Extensional-BasedSupportList } diff --git a/src/Mugen/Order/Instances/Coproduct.agda b/src/Mugen/Order/Instances/Coproduct.agda new file mode 100644 index 0000000..0ba317d --- /dev/null +++ b/src/Mugen/Order/Instances/Coproduct.agda @@ -0,0 +1,46 @@ +module Mugen.Order.Instances.Coproduct where + +open import Mugen.Prelude + +-- NOTE: We require that both 'A' and 'B' live in the same universe +-- to avoid large amounts of 'Lift'. If you need to take the coproduct +-- of two partial orders that live in different universes, perform a lift +-- on the partial order before taking the coproduct. +module _ {o r} (A B : Poset o r) where + private + module A = Poset A + module B = Poset B + + _≤_ : (⌞ A ⌟ ⊎ ⌞ B ⌟) → (⌞ A ⌟ ⊎ ⌞ B ⌟) → Type r + inl x ≤ inl y = x A.≤ y + inl x ≤ inr y = Lift _ ⊥ + inr x ≤ inl y = Lift _ ⊥ + inr x ≤ inr y = x B.≤ y + + ≤-thin : ∀ x y → is-prop (x ≤ y) + ≤-thin (inl _) (inl _) = A.≤-thin + ≤-thin (inl _) (inr _) = hlevel 1 + ≤-thin (inr _) (inl _) = hlevel 1 + ≤-thin (inr _) (inr _) = B.≤-thin + + ≤-refl : ∀ x → x ≤ x + ≤-refl (inl x) = A.≤-refl + ≤-refl (inr x) = B.≤-refl + + ≤-trans : ∀ x y z → x ≤ y → y ≤ z → x ≤ z + ≤-trans (inl x) (inl y) (inl z) p q = A.≤-trans p q + ≤-trans (inr x) (inr y) (inr z) p q = B.≤-trans p q + + ≤-antisym : ∀ x y → x ≤ y → y ≤ x → x ≡ y + ≤-antisym (inl _) (inl _) p q = ap inl $ A.≤-antisym p q + ≤-antisym (inl _) (inr _) () + ≤-antisym (inr _) (inl _) () + ≤-antisym (inr _) (inr _) p q = ap inr $ B.≤-antisym p q + + Coproduct : Poset o r + Coproduct .Poset.Ob = ⌞ A ⌟ ⊎ ⌞ B ⌟ + Coproduct .Poset._≤_ = _≤_ + Coproduct .Poset.≤-thin {x} {y} = ≤-thin x y + Coproduct .Poset.≤-refl {x} = ≤-refl x + Coproduct .Poset.≤-trans {x} {y} {z} = ≤-trans x y z + Coproduct .Poset.≤-antisym {x} {y} = ≤-antisym x y diff --git a/src/Mugen/Order/Instances/Discrete.agda b/src/Mugen/Order/Instances/Discrete.agda new file mode 100644 index 0000000..0779817 --- /dev/null +++ b/src/Mugen/Order/Instances/Discrete.agda @@ -0,0 +1,11 @@ +module Mugen.Order.Instances.Discrete where + +open import Mugen.Prelude + +Disc : ∀ {o} (A : Set o) → Poset o o +Disc A .Poset.Ob = ⌞ A ⌟ +Disc A .Poset._≤_ x y = x ≡ y +Disc A .Poset.≤-thin = hlevel! +Disc A .Poset.≤-refl = refl +Disc A .Poset.≤-trans = _∙_ +Disc A .Poset.≤-antisym p _ = p diff --git a/src/Mugen/Order/Instances/Endomorphism.agda b/src/Mugen/Order/Instances/Endomorphism.agda new file mode 100644 index 0000000..ebfc85a --- /dev/null +++ b/src/Mugen/Order/Instances/Endomorphism.agda @@ -0,0 +1,66 @@ +module Mugen.Order.Instances.Endomorphism where + +open import Cat.Diagram.Monad +import Cat.Reasoning as Cat + +open import Mugen.Prelude + +open import Mugen.Order.StrictOrder +open import Mugen.Cat.StrictOrders +open import Mugen.Cat.Monad + +import Mugen.Order.Reasoning as Reasoning + +-------------------------------------------------------------------------------- +-- Endomorphism Posets +-- Section 3.4 +-- +-- Given a Monad 'H' on the category of strict orders, we can construct a poset +-- whose carrier set is the set of endomorphisms 'Free H Δ → Free H Δ' between +-- free H-algebras in the Eilenberg-Moore category. +open Algebra-hom + +module _ {o r} (H : Monad (Strict-orders o r)) (Δ : Poset o r) where + + open Monad H renaming (M₀ to H₀; M₁ to H₁) + open Cat (Eilenberg-Moore (Strict-orders o r) H) + + private + module H⟨Δ⟩ = Reasoning (H₀ Δ) + Fᴴ⟨Δ⟩ : Algebra (Strict-orders o r) H + Fᴴ⟨Δ⟩ = Functor.F₀ (Free (Strict-orders o r) H) Δ + + Endomorphism-type : Type (lsuc o ⊔ lsuc r) + Endomorphism-type = Hom Fᴴ⟨Δ⟩ Fᴴ⟨Δ⟩ + + -------------------------------------------------------------------------------- + -- Order + + -- Favonia: the following "HACK" note was added when we were using records + -- to define 'endo[_≤_]'. The accuracy of the note should be checked again. + -- > HACK: We could make this live in a lower universe level, + -- > but then we can't construct a hierarchy theory from it without an annoying lift. + endo[_≤_] : ∀ (σ δ : Endomorphism-type) → Type (lsuc o ⊔ lsuc r) + endo[_≤_] σ δ = Lift _ ((α : ⌞ Δ ⌟) → σ # (unit.η Δ # α) H⟨Δ⟩.≤ δ # (unit.η Δ # α)) + + abstract + endo≤-thin : ∀ σ δ → is-prop endo[ σ ≤ δ ] + endo≤-thin σ δ = hlevel 1 + + endo≤-refl : ∀ σ → endo[ σ ≤ σ ] + endo≤-refl σ = lift λ _ → H⟨Δ⟩.≤-refl + + endo≤-trans : ∀ σ δ τ → endo[ σ ≤ δ ] → endo[ δ ≤ τ ] → endo[ σ ≤ τ ] + endo≤-trans σ δ τ (lift σ≤δ) (lift δ≤τ) = lift λ α → H⟨Δ⟩.≤-trans (σ≤δ α) (δ≤τ α) + + endo≤-antisym : ∀ σ δ → endo[ σ ≤ δ ] → endo[ δ ≤ σ ] → σ ≡ δ + endo≤-antisym σ δ (lift σ≤δ) (lift δ≤σ) = free-algebra-hom-path H $ ext λ α → + H⟨Δ⟩.≤-antisym (σ≤δ α) (δ≤σ α) + + Endomorphism : Poset (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) + Endomorphism .Poset.Ob = Endomorphism-type + Endomorphism .Poset._≤_ = endo[_≤_] + Endomorphism .Poset.≤-thin {σ} {δ} = endo≤-thin σ δ + Endomorphism .Poset.≤-refl {σ} = endo≤-refl σ + Endomorphism .Poset.≤-trans {σ} {δ} {τ} = endo≤-trans σ δ τ + Endomorphism .Poset.≤-antisym {σ} {δ} = endo≤-antisym σ δ diff --git a/src/Mugen/Order/Instances/Fractal.agda b/src/Mugen/Order/Instances/Fractal.agda new file mode 100644 index 0000000..d3eb78d --- /dev/null +++ b/src/Mugen/Order/Instances/Fractal.agda @@ -0,0 +1,62 @@ +module Mugen.Order.Instances.Fractal where + +open import Mugen.Prelude +open import Mugen.Data.NonEmpty + +import Mugen.Order.Reasoning as Reasoning + +private variable + o r : Level + +-------------------------------------------------------------------------------- +-- Fractal Posets +-- Section 3.3.7 + +module _ (A : Poset o r) where + private + module A = Reasoning A + + -- The first argument of 'fractal[_][_≤_]' (after being re-exported to the top level) + -- is the poset A. + data fractal[_][_≤_] : List⁺ ⌞ A ⌟ → List⁺ ⌞ A ⌟ → Type (o ⊔ r) where + single≤ : ∀ {x y} → x A.≤ y → fractal[_][_≤_] [ x ] [ y ] + tail≤' : ∀ {x xs y ys} → x A.≤[ fractal[_][_≤_] xs ys ] y → fractal[_][_≤_] (x ∷ xs) (y ∷ ys) + pattern tail≤ α β = tail≤' (α , β) + + private + _≤_ : List⁺ ⌞ A ⌟ → List⁺ ⌞ A ⌟ → Type (o ⊔ r) + x ≤ y = fractal[_][_≤_] x y + + abstract + ≤-refl : ∀ (xs : List⁺ ⌞ A ⌟) → xs ≤ xs + ≤-refl [ x ] = single≤ A.≤-refl + ≤-refl (x ∷ xs) = tail≤ A.≤-refl λ _ → ≤-refl xs + + ≤-trans : ∀ (xs ys zs : List⁺ ⌞ A ⌟) → xs ≤ ys → ys ≤ zs → xs ≤ zs + ≤-trans [ x ] [ y ] [ z ] (single≤ x≤y) (single≤ y≤z) = single≤ (A.≤-trans x≤y y≤z) + ≤-trans (x ∷ xs) (y ∷ ys) (z ∷ zs) (tail≤ x≤y xs≤ys) (tail≤ y≤z ys≤zs) = + tail≤ (A.≤-trans x≤y y≤z) λ x=z → + ≤-trans xs ys zs (xs≤ys (A.≤-antisym'-l x≤y y≤z x=z)) (ys≤zs (A.≤-antisym'-r x≤y y≤z x=z)) + + ≤-antisym : ∀ (xs ys : List⁺ ⌞ A ⌟) → xs ≤ ys → ys ≤ xs → xs ≡ ys + ≤-antisym [ x ] [ y ] (single≤ x≤y) (single≤ y≤x) = ap [_] $ A.≤-antisym x≤y y≤x + ≤-antisym (x ∷ xs) (y ∷ ys) (tail≤ x≤y xs≤ys) (tail≤ y≤x ys≤xs) = + let x=y = A.≤-antisym x≤y y≤x in ap₂ _∷_ x=y $ ≤-antisym xs ys (xs≤ys x=y) (ys≤xs (sym x=y)) + + ≤-thin : ∀ (xs ys : List⁺ ⌞ A ⌟) → is-prop (xs ≤ ys) + ≤-thin [ x ] [ y ] (single≤ x≤y) (single≤ x≤y') = ap single≤ (A.≤-thin x≤y x≤y') + ≤-thin (x ∷ xs) (y ∷ ys) (tail≤ x≤y xs≤ys) (tail≤ x≤y' xs≤ys') = ap₂ tail≤ (A.≤-thin x≤y x≤y') $ + funext λ p → ≤-thin xs ys (xs≤ys p) (xs≤ys' p) + + -------------------------------------------------------------------------------- + -- Poset Bundle + + Fractal : Poset o (o ⊔ r) + Fractal = poset where + poset : Poset o (o ⊔ r) + poset .Poset.Ob = List⁺ ⌞ A ⌟ + poset .Poset._≤_ = _≤_ + poset .Poset.≤-thin = ≤-thin _ _ + poset .Poset.≤-refl = ≤-refl _ + poset .Poset.≤-trans = ≤-trans _ _ _ + poset .Poset.≤-antisym = ≤-antisym _ _ diff --git a/src/Mugen/Order/Instances/Int.agda b/src/Mugen/Order/Instances/Int.agda new file mode 100644 index 0000000..4edafef --- /dev/null +++ b/src/Mugen/Order/Instances/Int.agda @@ -0,0 +1,27 @@ +module Mugen.Order.Instances.Int where + +open import Mugen.Prelude +open import Mugen.Data.Int +open import Mugen.Order.Lattice + +------------------------------------------------------------------------------- +-- Bundles + +Int-poset : Poset lzero lzero +Int-poset = poset where + poset : Poset _ _ + poset .Poset.Ob = Int + poset .Poset._≤_ = _≤ℤ_ + poset .Poset.≤-refl = ≤ℤ-refl _ + poset .Poset.≤-trans = ≤ℤ-trans _ _ _ + poset .Poset.≤-thin = ≤ℤ-is-prop _ _ + poset .Poset.≤-antisym = ≤ℤ-antisym _ _ + +-------------------------------------------------------------------------------- +-- Joins + +Int-has-joins : has-joins Int-poset +Int-has-joins .has-joins.join = maxℤ +Int-has-joins .has-joins.joinl {x} {y} = maxℤ-≤l x y +Int-has-joins .has-joins.joinr {x} {y} = maxℤ-≤r x y +Int-has-joins .has-joins.universal {x} {y} {z} = maxℤ-is-lub x y z diff --git a/src/Mugen/Order/Instances/LeftInvariantRightCentered.agda b/src/Mugen/Order/Instances/LeftInvariantRightCentered.agda new file mode 100644 index 0000000..f7a7d6b --- /dev/null +++ b/src/Mugen/Order/Instances/LeftInvariantRightCentered.agda @@ -0,0 +1,76 @@ +module Mugen.Order.Instances.LeftInvariantRightCentered where + +open import Mugen.Prelude + +import Mugen.Order.Reasoning as Reasoning + +module _ {o o' r r'} (A : Poset o r) (B : Poset o' r') (b : ⌞ B ⌟) where + private + module A = Reasoning A + module B = Reasoning B + + data RawLeftInvariantRightCentered≤ (x y : ⌞ A ⌟ × ⌞ B ⌟) : Type (o ⊔ r ⊔ r') where + biased : fst x ≡ fst y → snd x B.≤ snd y → RawLeftInvariantRightCentered≤ x y + centred : fst x A.≤ fst y → snd x B.≤ b → b B.≤ snd y → RawLeftInvariantRightCentered≤ x y + + LeftInvariantRightCentered≤ : (x y : ⌞ A ⌟ × ⌞ B ⌟) → Type (o ⊔ r ⊔ r') + LeftInvariantRightCentered≤ x y = ∥ RawLeftInvariantRightCentered≤ x y ∥ + + private + ⋉-thin : ∀ (x y : ⌞ A ⌟ × ⌞ B ⌟) → is-prop (LeftInvariantRightCentered≤ x y) + ⋉-thin x y = squash + + ⋉-refl : ∀ (x : ⌞ A ⌟ × ⌞ B ⌟) → LeftInvariantRightCentered≤ x x + ⋉-refl (a , b1) = pure $ biased refl B.≤-refl + + ⋉-trans : ∀ (x y z : ⌞ A ⌟ × ⌞ B ⌟) + → LeftInvariantRightCentered≤ x y + → LeftInvariantRightCentered≤ y z + → LeftInvariantRightCentered≤ x z + ⋉-trans x y z = ∥-∥-map₂ λ where + (biased a1=a2 b1≤b2) (biased a2=a3 b2≤b3) → biased (a1=a2 ∙ a2=a3) (B.≤-trans b1≤b2 b2≤b3) + (biased a1=a2 b1≤b2) (centred a2≤a3 b2≤b b≤b3) → centred (A.=+≤→≤ a1=a2 a2≤a3) (B.≤-trans b1≤b2 b2≤b) b≤b3 + (centred a1≤a2 b1≤b b≤b2) (biased a2=a3 b2≤b3) → centred (A.≤+=→≤ a1≤a2 a2=a3) b1≤b (B.≤-trans b≤b2 b2≤b3) + (centred a1≤a2 b1≤b b≤b2) (centred a2≤a3 b2≤b b≤b3) → centred (A.≤-trans a1≤a2 a2≤a3) b1≤b b≤b3 + + ⋉-antisym : ∀ (x y : ⌞ A ⌟ × ⌞ B ⌟) + → LeftInvariantRightCentered≤ x y + → LeftInvariantRightCentered≤ y x + → x ≡ y + ⋉-antisym x y = ∥-∥-rec₂ (×-is-hlevel 2 A.Ob-is-set B.Ob-is-set _ _) λ where + (biased a1=a2 b1≤b2) (biased a2=a1 b2≤b1) → + ap₂ _,_ a1=a2 (B.≤-antisym b1≤b2 b2≤b1) + (biased a1=a2 b1≤b2) (centred a2≤a1 b2≤b b≤b1) → + ap₂ _,_ a1=a2 (B.≤-antisym b1≤b2 $ B.≤-trans b2≤b b≤b1) + (centred a1≤a2 b1≤b b≤b2) (biased a2=a1 b2≤b1) → + ap₂ _,_ (sym a2=a1) (B.≤-antisym (B.≤-trans b1≤b b≤b2) b2≤b1) + (centred a1≤a2 b1≤b b≤b2) (centred a2≤a1 b2≤b b≤b1) → + ap₂ _,_ (A.≤-antisym a1≤a2 a2≤a1) (B.≤-antisym (B.≤-trans b1≤b b≤b2) (B.≤-trans b2≤b b≤b1)) + + LeftInvariantRightCentered : Poset (o ⊔ o') (o ⊔ r ⊔ r') + LeftInvariantRightCentered .Poset.Ob = ⌞ A ⌟ × ⌞ B ⌟ + LeftInvariantRightCentered .Poset._≤_ x y = LeftInvariantRightCentered≤ x y + LeftInvariantRightCentered .Poset.≤-thin = ⋉-thin _ _ + LeftInvariantRightCentered .Poset.≤-refl {x} = ⋉-refl x + LeftInvariantRightCentered .Poset.≤-trans {x} {y} {z} = ⋉-trans x y z + LeftInvariantRightCentered .Poset.≤-antisym {x} {y} = ⋉-antisym x y + + syntax RawLeftInvariantRightCentered≤ A B b x y = A ⋉[ b ] B [ x raw≤ y ] + syntax LeftInvariantRightCentered≤ A B b x y = A ⋉[ b ] B [ x ≤ y ] + syntax LeftInvariantRightCentered A B b = A ⋉[ b ] B + +module _ {o o' r r'} {A : Poset o' r'} {B : Poset o r} {b : ⌞ B ⌟} where + private + module A = Reasoning A + module B = Reasoning B + module A⋉B = Reasoning (A ⋉[ b ] B) + + ⋉-fst-invariant : ∀ {x y : A⋉B.Ob} → A ⋉[ b ] B [ x ≤ y ] → fst x A.≤ fst y + ⋉-fst-invariant = ∥-∥-rec A.≤-thin λ where + (biased a1=a2 b1≤b2) → A.=→≤ a1=a2 + (centred a1≤a2 b1≤b b≤b2) → a1≤a2 + + ⋉-snd-invariant : ∀ {x y : ⌞ A ⌟ × ⌞ B ⌟} → A ⋉[ b ] B [ x ≤ y ] → snd x B.≤ snd y + ⋉-snd-invariant = ∥-∥-rec B.≤-thin λ where + (biased a1=a2 b1≤b2) → b1≤b2 + (centred a1≤a2 b1≤b b≤b2) → B.≤-trans b1≤b b≤b2 diff --git a/src/Mugen/Order/Instances/Lexicographic.agda b/src/Mugen/Order/Instances/Lexicographic.agda new file mode 100644 index 0000000..41cff5e --- /dev/null +++ b/src/Mugen/Order/Instances/Lexicographic.agda @@ -0,0 +1,118 @@ +module Mugen.Order.Instances.Lexicographic where + +open import Mugen.Prelude +open import Mugen.Order.Lattice + +import Mugen.Order.Reasoning as Reasoning + +private variable + o o' r r' : Level + +-------------------------------------------------------------------------------- +-- Lexicographic Products +-- Section 3.3.4 +-- +-- The lexicographic product of 2 posets consists of their product +-- as monoids, as well as their lexicographic product as orders. + +module _ (A : Poset o r) (B : Poset o' r') where + private + module A = Reasoning A + module B = Reasoning B + + Lexicographic : Poset (o ⊔ o') (o ⊔ r ⊔ r') + Lexicographic = poset where + + _≤_ : ∀ (x y : ⌞ A ⌟ × ⌞ B ⌟) → Type (o ⊔ r ⊔ r') + _≤_ x y = x .fst A.≤[ x .snd B.≤ y .snd ] y .fst + + abstract + ≤-thin : ∀ x y → is-prop (x ≤ y) + ≤-thin x y = hlevel! + + ≤-refl : ∀ x → x ≤ x + ≤-refl x = A.≤-refl , λ _ → B.≤-refl + + ≤-trans : ∀ x y z → x ≤ y → y ≤ z → x ≤ z + ≤-trans x y z (x1≤y1 , x2≤y2) (y1≤z1 , y2≤z2) = + A.≤-trans x1≤y1 y1≤z1 , λ x1=z1 → + B.≤-trans + (x2≤y2 (A.≤-antisym'-l x1≤y1 y1≤z1 x1=z1)) + (y2≤z2 (A.≤-antisym'-r x1≤y1 y1≤z1 x1=z1)) + + ≤-antisym : ∀ x y → x ≤ y → y ≤ x → x ≡ y + ≤-antisym x y (x1≤y1 , x2≤y2) (y1≤x1 , y2≤x2) i = + let x1=y1 = A.≤-antisym x1≤y1 y1≤x1 in + x1=y1 i , B.≤-antisym (x2≤y2 x1=y1) (y2≤x2 (sym x1=y1)) i + + poset : Poset (o ⊔ o') (o ⊔ r ⊔ r') + poset .Poset.Ob = ⌞ A ⌟ × ⌞ B ⌟ + poset .Poset._≤_ = _≤_ + poset .Poset.≤-thin = ≤-thin _ _ + poset .Poset.≤-refl = ≤-refl _ + poset .Poset.≤-trans = ≤-trans _ _ _ + poset .Poset.≤-antisym = ≤-antisym _ _ + +module _ {A : Poset o r} {B : Poset o' r'} where + private + module A = Reasoning A + module B = Reasoning B + + -------------------------------------------------------------------------------- + -- Joins + + -- If the following conditions are true, then 'Lex 𝒟₁ 𝒟₂' has joins: + -- (1) Both 𝒟₁ and 𝒟₂ have joins. + -- (2) 𝒟₂ has a bottom. + -- (3) It's decidable in 𝒟₁ whether an element is equal to its join with another element. + lex-has-joins + : (A-joins : has-joins A) (let module A-joins = has-joins A-joins) + → (∀ x y → Dec (x ≡ A-joins.join x y) × Dec (y ≡ A-joins.join x y)) + → (B-joins : has-joins B) → has-bottom B + → has-joins (Lexicographic A B) + + lex-has-joins A-joins _≡∨₁?_ B-joins B-bottom = joins + where + module A-joins = has-joins A-joins + module B-joins = has-joins B-joins + module B-bottom = has-bottom B-bottom + + joins : has-joins (Lexicographic A B) + joins .has-joins.join (x1 , x2) (y1 , y2) with x1 ≡∨₁? y1 + ... | yes _ , yes _ = A-joins.join x1 y1 , B-joins.join x2 y2 + ... | yes _ , no _ = A-joins.join x1 y1 , x2 + ... | no _ , yes _ = A-joins.join x1 y1 , y2 + ... | no _ , no _ = A-joins.join x1 y1 , B-bottom.bot + joins .has-joins.joinl {x1 , _} {y1 , _} with x1 ≡∨₁? y1 + ... | yes x1=x1∨y1 , yes _ = A-joins.joinl , λ _ → B-joins.joinl + ... | yes x1=x1∨y1 , no _ = A-joins.joinl , λ _ → B.≤-refl + ... | no x1≠x1∨y1 , yes _ = A-joins.joinl , λ x1≡x1∨y1 → absurd (x1≠x1∨y1 x1≡x1∨y1) + ... | no x1≠x1∨y1 , no _ = A-joins.joinl , λ x1≡x1∨y1 → absurd (x1≠x1∨y1 x1≡x1∨y1) + joins .has-joins.joinr {x1 , _} {y1 , _} with x1 ≡∨₁? y1 + ... | yes _ , yes y1=x1∨y1 = A-joins.joinr , λ _ → B-joins.joinr + ... | yes _ , no y1≠x1∨y1 = A-joins.joinr , λ y1≡x1∨y1 → absurd (y1≠x1∨y1 y1≡x1∨y1) + ... | no _ , yes y1=x1∨y1 = A-joins.joinr , λ _ → B.≤-refl + ... | no _ , no y1≠x1∨y1 = A-joins.joinr , λ y1≡x1∨y1 → absurd (y1≠x1∨y1 y1≡x1∨y1) + joins .has-joins.universal {x1 , _} {y1 , _} {_ , z2} x≤z y≤z with x1 ≡∨₁? y1 + ... | yes x1=x1∨y1 , yes y1=x1∨y1 = + A-joins.universal (x≤z .fst) (y≤z .fst) , λ x1vy1=z1 → + B-joins.universal (x≤z .snd (x1=x1∨y1 ∙ x1vy1=z1)) (y≤z .snd (y1=x1∨y1 ∙ x1vy1=z1)) + ... | yes x1=x1∨y1 , no y1≠x1∨y1 = + A-joins.universal (x≤z .fst) (y≤z .fst) , λ x1vy1=z1 → x≤z .snd (x1=x1∨y1 ∙ x1vy1=z1) + ... | no x1≠x1∨y1 , yes y1=x1∨y1 = + A-joins.universal (x≤z .fst) (y≤z .fst) , λ x1vy1=z1 → y≤z .snd (y1=x1∨y1 ∙ x1vy1=z1) + ... | no x1≠x1∨y1 , no y1≠x1∨y1 = + A-joins.universal (x≤z .fst) (y≤z .fst) , λ x1vy1=z1 → B-bottom.is-bottom + + -------------------------------------------------------------------------------- + -- Bottoms + + lex-has-bottom : has-bottom A → has-bottom B → has-bottom (Lexicographic A B) + lex-has-bottom A-bottom B-bottom = bottom + where + module A-bottom = has-bottom (A-bottom) + module B-bottom = has-bottom (B-bottom) + + bottom : has-bottom (Lexicographic A B) + bottom .has-bottom.bot = A-bottom.bot , B-bottom.bot + bottom .has-bottom.is-bottom = A-bottom.is-bottom , λ _ → B-bottom.is-bottom diff --git a/src/Mugen/Order/Instances/Nat.agda b/src/Mugen/Order/Instances/Nat.agda new file mode 100644 index 0000000..64bc26e --- /dev/null +++ b/src/Mugen/Order/Instances/Nat.agda @@ -0,0 +1,54 @@ +module Mugen.Order.Instances.Nat where + +open import Data.Nat + +open import Mugen.Prelude +open import Mugen.Data.Int +open import Mugen.Order.StrictOrder +open import Mugen.Order.Lattice +open import Mugen.Order.Instances.Int + +-------------------------------------------------------------------------------- +-- Bundles + +Nat-poset : Poset lzero lzero +Nat-poset .Poset.Ob = Nat +Nat-poset .Poset._≤_ = _≤_ +Nat-poset .Poset.≤-thin = ≤-is-prop +Nat-poset .Poset.≤-refl = ≤-refl +Nat-poset .Poset.≤-trans = ≤-trans +Nat-poset .Poset.≤-antisym = ≤-antisym + +-------------------------------------------------------------------------------- +-- Inclusion to Int-poset + +Nat→Int : Strictly-monotone Nat-poset Int-poset +Nat→Int .Strictly-monotone.hom = pos +Nat→Int .Strictly-monotone.pres-< p .fst = p +Nat→Int .Strictly-monotone.pres-< p .snd = pos-injective + +abstract + Nat→Int-is-full-subposet : is-full-subposet Nat→Int + Nat→Int-is-full-subposet .is-full-subposet.injective = pos-injective + Nat→Int-is-full-subposet .is-full-subposet.full p = p + +-------------------------------------------------------------------------------- +-- Joins + +Nat-has-joins : has-joins Nat-poset +Nat-has-joins .has-joins.join = max +Nat-has-joins .has-joins.joinl = max-≤l _ _ +Nat-has-joins .has-joins.joinr = max-≤r _ _ +Nat-has-joins .has-joins.universal = max-is-lub _ _ _ + +abstract + Nat→Int-is-subsemilattice : is-full-subsemilattice Nat-has-joins Int-has-joins Nat→Int + Nat→Int-is-subsemilattice .is-full-subsemilattice.has-is-full-subposet = Nat→Int-is-full-subposet + Nat→Int-is-subsemilattice .is-full-subsemilattice.pres-join = refl + +-------------------------------------------------------------------------------- +-- Bottoms + +Nat-has-bottom : has-bottom Nat-poset +Nat-has-bottom .has-bottom.bot = zero +Nat-has-bottom .has-bottom.is-bottom = 0≤x diff --git a/src/Mugen/Order/Instances/NonPositive.agda b/src/Mugen/Order/Instances/NonPositive.agda new file mode 100644 index 0000000..59bfdf3 --- /dev/null +++ b/src/Mugen/Order/Instances/NonPositive.agda @@ -0,0 +1,52 @@ +module Mugen.Order.Instances.NonPositive where + +open import Data.Nat + +open import Mugen.Prelude + +open import Mugen.Order.StrictOrder +open import Mugen.Order.Lattice +open import Mugen.Order.Instances.Nat +open import Mugen.Order.Instances.Int +open import Mugen.Order.Instances.Opposite + +open import Mugen.Data.Int + +-------------------------------------------------------------------------------- +-- The Non-Positive Integers +-- Section 3.3.1 +-- +-- These have a terse definition as the opposite order of Nat+, +-- so we just use that. + +NonPositive : Poset lzero lzero +NonPositive = Opposite Nat-poset + +-------------------------------------------------------------------------------- +-- Inclusion to Int-poset + +NonPositive→Int : Strictly-monotone NonPositive Int-poset +NonPositive→Int .Strictly-monotone.hom x = - x +NonPositive→Int .Strictly-monotone.pres-< p .fst = negate-anti-mono _ _ p +NonPositive→Int .Strictly-monotone.pres-< p .snd = negate-injective _ _ + +abstract + NonPositive→Int-is-full-subposet : is-full-subposet NonPositive→Int + NonPositive→Int-is-full-subposet .is-full-subposet.injective = negate-injective _ _ + NonPositive→Int-is-full-subposet .is-full-subposet.full {_} {zero} _ = 0≤x + NonPositive→Int-is-full-subposet .is-full-subposet.full {zero} {suc _} () + NonPositive→Int-is-full-subposet .is-full-subposet.full {suc _} {suc _} p = s≤s p + +-------------------------------------------------------------------------------- +-- Joins + +NonPositive-has-joins : has-joins NonPositive +NonPositive-has-joins .has-joins.join = min +NonPositive-has-joins .has-joins.joinl {x} {y} = min-≤l x y +NonPositive-has-joins .has-joins.joinr {x} {y} = min-≤r x y +NonPositive-has-joins .has-joins.universal {x} {y} {z} = min-is-glb x y z + +abstract + NonPositive→Int-is-full-subsemilattice : is-full-subsemilattice NonPositive-has-joins Int-has-joins NonPositive→Int + NonPositive→Int-is-full-subsemilattice .is-full-subsemilattice.has-is-full-subposet = NonPositive→Int-is-full-subposet + NonPositive→Int-is-full-subsemilattice .is-full-subsemilattice.pres-join = negate-min _ _ diff --git a/src/Mugen/Order/Instances/Opposite.agda b/src/Mugen/Order/Instances/Opposite.agda new file mode 100644 index 0000000..7858634 --- /dev/null +++ b/src/Mugen/Order/Instances/Opposite.agda @@ -0,0 +1,14 @@ +module Mugen.Order.Instances.Opposite where + +open import Mugen.Prelude + +module _ {o r} (A : Poset o r) where + open Poset A + + Opposite : Poset o r + Opposite .Poset.Ob = Ob + Opposite .Poset._≤_ x y = y ≤ x + Opposite .Poset.≤-refl = ≤-refl + Opposite .Poset.≤-trans p q = ≤-trans q p + Opposite .Poset.≤-thin = ≤-thin + Opposite .Poset.≤-antisym p q = ≤-antisym q p diff --git a/src/Mugen/Order/Instances/Pointwise.agda b/src/Mugen/Order/Instances/Pointwise.agda new file mode 100644 index 0000000..13fafd7 --- /dev/null +++ b/src/Mugen/Order/Instances/Pointwise.agda @@ -0,0 +1,50 @@ +module Mugen.Order.Instances.Pointwise where + +open import Order.Instances.Pointwise using (Pointwise) public + +open import Mugen.Prelude +open import Mugen.Order.Lattice + +import Mugen.Order.Reasoning as Reasoning + +private variable + o o' o'' o''' r r' r'' r''' : Level + +-------------------------------------------------------------------------------- +-- Product of Indexed Posets +-- POPL 2023 Section 3.3.5 discussed the special case where I = Nat and A is a constant family + +pointwise-map₂ + : {A : Type o} {B : A → Type o'} {C : A → Type o''} {D : A → Type o'''} + → (∀ (x : A) → B x → C x → D x) → (∀ x → B x) → (∀ x → C x) → (∀ x → D x) +pointwise-map₂ m f g i = m i (f i) (g i) + +module _ (I : Type o) {A : I → Poset o' r'} where + private + module A (i : I) = Poset (A i) + + -------------------------------------------------------------------------------- + -- Joins + + Pointwise-has-joins : (∀ i → has-joins (A i)) → has-joins (Pointwise I A) + Pointwise-has-joins 𝒟-joins = joins + where + open module J (i : I) = has-joins (𝒟-joins i) + + joins : has-joins (Pointwise I A) + joins .has-joins.join = pointwise-map₂ join + joins .has-joins.joinl i = joinl i + joins .has-joins.joinr i = joinr i + joins .has-joins.universal f≤h g≤h = λ i → universal i (f≤h i) (g≤h i) + + -------------------------------------------------------------------------------- + -- Bottom + + Pointwise-has-bottom : (∀ i → has-bottom (A i)) → has-bottom (Pointwise I A) + Pointwise-has-bottom A-bottom = bottom + where + open module B (i : I) = has-bottom (A-bottom i) + + bottom : has-bottom (Pointwise I A) + bottom .has-bottom.bot i = bot i + bottom .has-bottom.is-bottom i = is-bottom i diff --git a/src/Mugen/Order/Instances/Prefix.agda b/src/Mugen/Order/Instances/Prefix.agda new file mode 100644 index 0000000..0e38d39 --- /dev/null +++ b/src/Mugen/Order/Instances/Prefix.agda @@ -0,0 +1,52 @@ +module Mugen.Order.Instances.Prefix where + +open import Data.List +open import Mugen.Order.Lattice + +open import Mugen.Prelude + +private variable + o : Level + A : Type o + +module _ where + + data Prefix[_≤_] {A : Type o} : List A → List A → Type o where + pre[] : ∀ {xs} → Prefix[ [] ≤ xs ] + -- '_pre∷_' is taking the extra argument of type 'x ≡ y' to work around --without-K + _pre∷_ : ∀ {x y xs ys} → x ≡ y → Prefix[ xs ≤ ys ] → Prefix[ (x ∷ xs) ≤ (y ∷ ys) ] + + private abstract + prefix-refl : (xs : List A) → Prefix[ xs ≤ xs ] + prefix-refl [] = pre[] + prefix-refl (x ∷ xs) = refl pre∷ prefix-refl xs + + prefix-trans : (xs ys zs : List A) → Prefix[ xs ≤ ys ] → Prefix[ ys ≤ zs ] → Prefix[ xs ≤ zs ] + prefix-trans _ _ _ pre[] _ = pre[] + prefix-trans (x ∷ xs) (y ∷ ys) (z ∷ zs) (x≡y pre∷ xs≤ys) (y≡z pre∷ ys≤zs) = + (x≡y ∙ y≡z) pre∷ (prefix-trans xs ys zs xs≤ys ys≤zs) + + prefix-antisym : ∀ (xs ys : List A) → Prefix[ xs ≤ ys ] → Prefix[ ys ≤ xs ] → xs ≡ ys + prefix-antisym _ _ pre[] pre[] = refl + prefix-antisym (x ∷ xs) (y ∷ ys) (x≡y pre∷ xs≤ys) (y≡x pre∷ ys≤xs) = + ap₂ _∷_ x≡y (prefix-antisym xs ys xs≤ys ys≤xs) + + prefix-is-prop : ∀ {xs ys : List A} → is-set A → is-prop (Prefix[ xs ≤ ys ]) + prefix-is-prop {xs = []} aset pre[] pre[] = refl + prefix-is-prop {xs = x ∷ xs} {ys = y ∷ ys} aset (x≡y pre∷ xs