From 8b5414c7f5e1ade7a9d82c9cfe65439802ccef1c Mon Sep 17 00:00:00 2001 From: favonia Date: Sun, 26 Nov 2023 09:01:15 -0600 Subject: [PATCH] wip --- Dockerfile | 2 +- src/Mugen/Algebra/Displacement.agda | 92 ++-- src/Mugen/Algebra/Displacement/Constant.agda | 56 +- .../Algebra/Displacement/Endomorphism.agda | 101 ++-- .../Algebra/Displacement/FiniteSupport.agda | 45 +- src/Mugen/Algebra/Displacement/Fractal.agda | 91 ++-- .../Algebra/Displacement/InfiniteProduct.agda | 135 ++--- src/Mugen/Algebra/Displacement/Int.agda | 17 +- .../Algebra/Displacement/Lexicographic.agda | 182 +++---- src/Mugen/Algebra/Displacement/Nat.agda | 22 +- .../Algebra/Displacement/NearlyConstant.agda | 125 ++--- .../Algebra/Displacement/NonPositive.agda | 12 +- src/Mugen/Algebra/Displacement/Opposite.agda | 14 +- src/Mugen/Algebra/Displacement/Prefix.agda | 20 +- src/Mugen/Algebra/Displacement/Product.agda | 119 ++--- src/Mugen/Algebra/OrderedMonoid.agda | 16 +- src/Mugen/Axioms/WLPO.agda | 27 - src/Mugen/Cat/HierarchyTheory.agda | 80 ++- src/Mugen/Cat/HierarchyTheory/Properties.agda | 117 ++-- src/Mugen/Cat/StrictOrders.agda | 26 +- src/Mugen/Data/Int.agda | 505 ++++++------------ src/Mugen/Data/List.agda | 24 +- src/Mugen/Data/Nat.agda | 61 +-- src/Mugen/Data/NonEmpty.agda | 5 +- src/Mugen/Everything.agda | 4 +- src/Mugen/Order/Coproduct.agda | 90 ++-- src/Mugen/Order/Discrete.agda | 16 +- .../Order/LeftInvariantRightCentered.agda | 104 ++-- src/Mugen/Order/Opposite.agda | 35 +- src/Mugen/Order/Poset.agda | 195 ++++++- src/Mugen/Order/Prefix.agda | 58 +- src/Mugen/Order/Reasoning.agda | 49 ++ src/Mugen/Order/Singleton.agda | 17 +- src/Mugen/Order/StrictOrder.agda | 250 --------- src/Mugen/Order/StrictOrder/Reasoning.agda | 50 -- src/Mugen/Prelude.agda | 2 +- 36 files changed, 1224 insertions(+), 1540 deletions(-) delete mode 100644 src/Mugen/Axioms/WLPO.agda create mode 100644 src/Mugen/Order/Reasoning.agda delete mode 100644 src/Mugen/Order/StrictOrder.agda delete mode 100644 src/Mugen/Order/StrictOrder/Reasoning.agda diff --git a/Dockerfile b/Dockerfile index 2263e35..ffea40f 100644 --- a/Dockerfile +++ b/Dockerfile @@ -4,7 +4,7 @@ ARG GHC_VERSION=9.4.7 ARG AGDA_VERSION=5c8116227e2d9120267aed43f0e545a65d9c2fe2 -ARG ONELAB_VERSION=3f461009858d64a93d5d2b687ecf02504b9848a7 +ARG ONELAB_VERSION=a84319a523d866afc828535ce669ed114fbb5fd1 #################################################################################################### # Stage 1: building everything except agda-mugen diff --git a/src/Mugen/Algebra/Displacement.agda b/src/Mugen/Algebra/Displacement.agda index dec3653..1e4d87c 100644 --- a/src/Mugen/Algebra/Displacement.agda +++ b/src/Mugen/Algebra/Displacement.agda @@ -6,7 +6,7 @@ open import Algebra.Semigroup open import Mugen.Prelude open import Mugen.Algebra.OrderedMonoid -open import Mugen.Order.StrictOrder +open import Mugen.Order.Poset import Mugen.Data.Nat as Nat @@ -22,24 +22,33 @@ private variable -- over an order. record is-displacement-algebra - {o r} (A : Strict-order o r) + {o r} (A : Poset o r) (ε : ⌞ A ⌟) (_⊗_ : ⌞ A ⌟ → ⌞ A ⌟ → ⌞ A ⌟) : Type (o ⊔ r) where no-eta-equality - open Strict-order A + open Poset A field has-is-monoid : is-monoid ε _⊗_ - left-invariant : ∀ {x y z} → y < z → (x ⊗ y) < (x ⊗ z) + + -- These two properties are constructively MUCH NICER than + -- ∀ {x y z} → y < z → (x ⊗ y) < (x ⊗ z) + -- The reason is that the second part of '_<_' is a negation, + -- and a function between two negated types '(A → ⊥) → (B → ⊥)' + -- is constructively very annoying when proving that InfProd + -- is a displacement algebra. What we need is a slightly more + -- constructive version of type 'B → A' instead. + ≤-left-invariant : ∀ {x y z} → y ≤ z → (x ⊗ y) ≤ (x ⊗ z) + injr-on-≤ : ∀ {x y z} → y ≤ z → (x ⊗ y) ≡ (x ⊗ z) → y ≡ z open is-monoid has-is-monoid hiding (has-is-set) public - ≤-left-invariant : ∀ {x y z} → y ≤ z → (x ⊗ y) ≤ (x ⊗ z) - ≤-left-invariant {x = x} (inl p) = inl (ap (x ⊗_) p) - ≤-left-invariant (inr y 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 $ ext λ α → + H⟨Δ⟩.≤-antisym (σ≤δ α) (δ≤σ α) -------------------------------------------------------------------------------- -- Left Invariance - ∘-left-invariant : ∀ (σ δ τ : Endomorphism) → endo[ δ < τ ] → endo[ σ ∘ δ < σ ∘ τ ] - ∘-left-invariant σ δ τ δ<τ = ∘-lt - where - module σ = Strictly-monotone (σ .morphism) + ∘-left-invariant : ∀ (σ δ τ : Endomorphism) → endo[ δ ≤ τ ] → endo[ σ ∘ δ ≤ σ ∘ τ ] + ∘-left-invariant σ δ τ δ≤τ = lift λ α → σ .morphism .Strictly-monotone.mono (δ≤τ .Lift.lower α) - ∘-lt : endo[ σ ∘ δ < σ ∘ τ ] - ∘-lt .endo-≤ α = σ.mono (δ<τ .endo-≤ α) - ∘-lt .endo-< = ∥-∥-map (λ lt → lt .fst , σ.strict-mono (lt .snd)) (δ<τ .endo-<) + ∘-injr-on-≤ : ∀ (σ δ τ : Endomorphism) → endo[ δ ≤ τ ] → σ ∘ δ ≡ σ ∘ τ → δ ≡ τ + ∘-injr-on-≤ σ δ τ (lift δ≤τ) p = free-algebra-hom-path $ ext λ α → + σ .morphism .Strictly-monotone.inj-on-related (δ≤τ α) (ap (_# (unit.η Δ # α)) p) -------------------------------------------------------------------------------- -- Bundles -- -- We do this with copatterns for performance reasons. - Endo< : Strict-order (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) - Endo< .Strict-order.Ob = Endomorphism - Endo< .Strict-order.strict-order-on .Strict-order-on._<_ = endo[_<_] - Endo< .Strict-order.strict-order-on .Strict-order-on.has-is-strict-order .is-strict-order.<-irrefl = endo-<-irrefl - Endo< .Strict-order.strict-order-on .Strict-order-on.has-is-strict-order .is-strict-order.<-trans = endo-<-trans - Endo< .Strict-order.strict-order-on .Strict-order-on.has-is-strict-order .is-strict-order.<-thin = hlevel! - Endo< .Strict-order.strict-order-on .Strict-order-on.has-is-strict-order .is-strict-order.has-is-set = Hom-set _ _ + 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.strict-order = Endo< + 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-invariant = ∘-left-invariant _ _ _ + Endo∘ .Displacement-algebra.displacement-algebra-on .Displacement-algebra-on.has-is-displacement-algebra .is-displacement-algebra.≤-left-invariant {σ} {δ} {τ} = ∘-left-invariant σ δ τ + Endo∘ .Displacement-algebra.displacement-algebra-on .Displacement-algebra-on.has-is-displacement-algebra .is-displacement-algebra.injr-on-≤ = ∘-injr-on-≤ _ _ _ diff --git a/src/Mugen/Algebra/Displacement/FiniteSupport.agda b/src/Mugen/Algebra/Displacement/FiniteSupport.agda index 78ab06c..565f682 100644 --- a/src/Mugen/Algebra/Displacement/FiniteSupport.agda +++ b/src/Mugen/Algebra/Displacement/FiniteSupport.agda @@ -7,14 +7,11 @@ 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.InfiniteProduct open import Mugen.Algebra.Displacement.NearlyConstant open import Mugen.Algebra.OrderedMonoid -open import Mugen.Order.StrictOrder - -open import Mugen.Data.List -------------------------------------------------------------------------------- @@ -75,8 +72,8 @@ module FinSupport {o r} (𝒟 : Displacement-algebra o r) (_≡?_ : Discrete ⌞ -------------------------------------------------------------------------------- -- Order - _<_ : FinSupportList → FinSupportList → Type (o ⊔ r) - _<_ xs ys = (xs .support) supp< (ys .support) + _≤_ : FinSupportList → FinSupportList → Type r + _≤_ xs ys = (xs .support) supp≤ (ys .support) -------------------------------------------------------------------------------- -- Displacement Algebra @@ -86,26 +83,29 @@ module _ {o r} (𝒟 : Displacement-algebra o r) (_≡?_ : Discrete ⌞ 𝒟 ⌟ open FinSupportList private module 𝒩 = Displacement-algebra (NearlyConstant 𝒟 _≡?_) - FiniteSupport : Displacement-algebra o (o ⊔ r) + FiniteSupport : Displacement-algebra o r FiniteSupport = to-displacement-algebra mk where - mk-strict : make-strict-order (o ⊔ r) FinSupportList - mk-strict .make-strict-order._<_ = _<_ - mk-strict .make-strict-order.<-irrefl {xs} = - 𝒩.<-irrefl {xs .support} - mk-strict .make-strict-order.<-trans {xs} {ys} {zs} = - 𝒩.<-trans {xs .support} {ys .support} {zs .support} - mk-strict .make-strict-order.<-thin {xs} {ys} = - 𝒩.<-thin {xs .support} {ys .support} - mk-strict .make-strict-order.has-is-set = FinSupportList-is-set - - mk : make-displacement-algebra (to-strict-order mk-strict) + 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-invariant {xs} {ys} {zs} = - 𝒩.left-invariant {xs .support} {ys .support} {zs .support} + mk .make-displacement-algebra.≤-left-invariant {xs} {ys} {zs} = + 𝒩.≤-left-invariant {xs .support} {ys .support} {zs .support} + mk .make-displacement-algebra.injr-on-≤ {xs} {ys} p q = + fin-support-list-path $ 𝒩.injr-on-≤ {xs .support} {ys .support} p (ap support q) -------------------------------------------------------------------------------- -- Subalgebra Structure @@ -124,7 +124,7 @@ module _ mk .make-displacement-subalgebra.into = FinSupportList.support mk .make-displacement-subalgebra.pres-ε = refl mk .make-displacement-subalgebra.pres-⊗ _ _ = refl - mk .make-displacement-subalgebra.strictly-mono _ _ xs M unit .η L .hom l = l , ε - unit .η L .strict-mono l M mult .η L .hom ((l , x) , y) = l , (x ⊗ y) - mult .η L .strict-mono {_ , d2} (biased α≡β d2 Uᴹᴰ F∘ T - ν pt = nt + ν pt = ? where ℓ̅ : ⌞ H.M₀ Δ ⌟ → Hom Δ⁺ (H.M₀ Δ⁺) ℓ̅ ℓ .hom (ι₀ _) = H.M₁ ι₁-hom # ℓ ℓ̅ ℓ .hom (ι₁ α) = H.unit.η _ # ι₂ α ℓ̅ ℓ .hom (ι₂ α) = H.unit.η _ # ι₂ α - ℓ̅ ℓ .strict-mono {ι₀ α} {ι₀ β} (lift ff) = absurd ff - ℓ̅ ℓ .strict-mono {ι₁ α} {ι₁ β} α<β = H.unit.η _ .strict-mono α<β - ℓ̅ ℓ .strict-mono {ι₂ α} {ι₂ β} α<β = H.unit.η _ .strict-mono α<β - - ℓ̅-mono : ∀ {ℓ ℓ′} → ℓ′ H⟨Δ⟩.< ℓ → ∀ (α : ⌞ Δ⁺ ⌟) → ℓ̅ ℓ′ # α H⟨Δ⁺⟩.≤ ℓ̅ ℓ # α - ℓ̅-mono ℓ′<ℓ (ι₀ _) = inr (H.M₁ ι₁-hom .strict-mono ℓ′<ℓ) - ℓ̅-mono ℓ′<ℓ (ι₁ _) = inl refl - ℓ̅-mono ℓ′<ℓ (ι₂ _) = inl refl + ℓ̅ ℓ .mono {ι₀ ⋆} {ι₀ ⋆} _ = H⟨Δ⁺⟩.≤-refl + ℓ̅ ℓ .mono {ι₁ α} {ι₁ β} α≤β = H.unit.η _ .mono α≤β + ℓ̅ ℓ .mono {ι₂ α} {ι₂ β} α≤β = H.unit.η _ .mono α≤β + ℓ̅ ℓ .inj-on-related {ι₀ ⋆} {ι₀ ⋆} α≤β _ = refl + ℓ̅ ℓ .inj-on-related {ι₁ α} {ι₁ β} α≤β p = ap ι₁ $ ι₂-inj $ H.unit.η _ .inj-on-related α≤β p + ℓ̅ ℓ .inj-on-related {ι₂ α} {ι₂ β} α≤β p = H.unit.η _ .inj-on-related α≤β p + + ℓ̅-mono : ∀ {ℓ ℓ′} → ℓ′ H⟨Δ⟩.≤ ℓ → ∀ (α : ⌞ Δ⁺ ⌟) → ℓ̅ ℓ′ # α H⟨Δ⁺⟩.≤ ℓ̅ ℓ # α + ℓ̅-mono ℓ′≤ℓ (ι₀ _) = (H.M₁ ι₁-hom .mono ℓ′≤ℓ) + ℓ̅-mono ℓ′≤ℓ (ι₁ _) = H⟨Δ⁺⟩.≤-refl + ℓ̅-mono ℓ′≤ℓ (ι₂ _) = H⟨Δ⁺⟩.≤-refl ν′ : ⌞ H.M₀ Δ ⌟ → Algebra-hom _ H Fᴴ⟨ Δ⁺ ⟩ Fᴴ⟨ Δ⁺ ⟩ ν′ ℓ .morphism = H.mult.η _ ∘ H.M₁ (ℓ̅ ℓ) @@ -220,25 +237,29 @@ module _ {o r} (H : Hierarchy-theory o r) (Δ : Strict-order o r) (Ψ : Set (lsu H.mult.η _ # (H.M₁ (H.mult.η _) # (H.M₁ (H.M₁ (ℓ̅ ℓ)) # α)) ≡˘⟨ ap (H.mult.η _ #_) (H.M-∘ _ _ #ₚ α) ⟩ H.mult.η _ # (H.M₁ (H.mult.η _ ∘ H.M₁ (ℓ̅ ℓ)) # α) ∎ - ν′-strictly-mono : ∀ {ℓ′ ℓ : ⌞ H.M₀ Δ ⌟} → ℓ′ H⟨Δ⟩.< ℓ → ν′ ℓ′ H⟨Δ⁺⟩→.< ν′ ℓ - ν′-strictly-mono {ℓ′} {ℓ} ℓ′<ℓ .endo[_<_].endo-≤ α = begin-≤ - H.mult.η _ # (H.M₁ (ℓ̅ ℓ′) # (H.unit.η _ # α)) ≡̇⟨ ap (H.mult.η _ #_) (sym $ H.unit.is-natural _ _ (ℓ̅ ℓ′) #ₚ α) ⟩ - H.mult.η _ # (H.unit.η _ # (ℓ̅ ℓ′ # α)) ≤⟨ mono (H.mult.η _ ∘ H.unit.η _) (ℓ̅-mono ℓ′<ℓ α) ⟩ - H.mult.η _ # (H.unit.η _ # (ℓ̅ ℓ # α)) ≡̇⟨ ap (H.mult.η _ #_) (H.unit.is-natural _ _ (ℓ̅ ℓ) #ₚ α) ⟩ - H.mult.η _ # (H.M₁ (ℓ̅ ℓ) # (H.unit.η _ # α)) <∎ + ν′-mono : ∀ {ℓ′ ℓ : ⌞ H.M₀ Δ ⌟} → ℓ′ H⟨Δ⟩.≤ ℓ → ν′ ℓ′ H⟨Δ⁺⟩→.≤ ν′ ℓ + ν′-mono {ℓ′} {ℓ} ℓ′≤ℓ .Lift.lower α = + H.mult.η _ # (H.M₁ (ℓ̅ ℓ′) # (H.unit.η _ # α)) ≐⟨ ap (H.mult.η _ #_) (sym $ H.unit.is-natural _ _ (ℓ̅ ℓ′) #ₚ α) ⟩ + H.mult.η _ # (H.unit.η _ # (ℓ̅ ℓ′ # α)) ≤⟨ mono (H.mult.η _ ∘ H.unit.η _) (ℓ̅-mono ℓ′≤ℓ α) ⟩ + H.mult.η _ # (H.unit.η _ # (ℓ̅ ℓ # α)) ≐⟨ ap (H.mult.η _ #_) (H.unit.is-natural _ _ (ℓ̅ ℓ) #ₚ α) ⟩ + H.mult.η _ # (H.M₁ (ℓ̅ ℓ) # (H.unit.η _ # α)) ≤∎ where - open Mugen.Order.StrictOrder.Reasoning (H.M₀ Δ⁺) - ν′-strictly-mono {ℓ′} {ℓ} ℓ′<ℓ .endo[_<_].endo-< = + open Mugen.Order.Reasoning (H.M₀ Δ⁺) + +{- + ν′-mono : ∀ {ℓ′ ℓ : ⌞ H.M₀ Δ ⌟} → ℓ′ H⟨Δ⟩.≤ ℓ → ν′ ℓ′ H⟨Δ⁺⟩→.≤ ν′ ℓ + ν′-mono {ℓ′} {ℓ} ℓ′≤ℓ .Lift.lower = inc (ι₀ ⋆ , ν′⟨ℓ′⟩⟨⋆⟩<ν′⟨ℓ⟩⟨⋆⟩) where - open Mugen.Order.StrictOrder.Reasoning (H.M₀ Δ⁺) + open Mugen.Order.Reasoning (H.M₀ Δ⁺) - ν′⟨ℓ′⟩⟨⋆⟩<ν′⟨ℓ⟩⟨⋆⟩ : H.mult.η _ # (H.M₁ (ℓ̅ ℓ′) # (H.unit.η _ # (ι₀ ⋆))) H⟨Δ⁺⟩.< H.mult.η _ # (H.M₁ (ℓ̅ ℓ) # (H.unit.η _ # (ι₀ ⋆))) - ν′⟨ℓ′⟩⟨⋆⟩<ν′⟨ℓ⟩⟨⋆⟩ = begin-< - H.mult.η _ # (H.M₁ (ℓ̅ ℓ′) # (H.unit.η _ # ι₀ ⋆)) ≡̇⟨ ap (H.mult.η _ #_) (sym $ H.unit.is-natural _ _ (ℓ̅ ℓ′) #ₚ _) ⟩ - H.mult.η _ # (H.unit.η _ # (H.M₁ ι₁-hom # ℓ′)) <⟨ (H.mult.η _ ∘ H.unit.η _ ∘ H.M₁ ι₁-hom) .strict-mono ℓ′<ℓ ⟩ - H.mult.η _ # (H.unit.η _ # (H.M₁ ι₁-hom # ℓ)) ≡̇⟨ ap (H.mult.η _ #_) (H.unit.is-natural _ _ (ℓ̅ ℓ) #ₚ _) ⟩ - H.mult.η _ # (H.M₁ (ℓ̅ ℓ) # (H.unit.η _ # ι₀ ⋆)) <∎ + ν′⟨ℓ′⟩⟨⋆⟩<ν′⟨ℓ⟩⟨⋆⟩ : H.mult.η _ # (H.M₁ (ℓ̅ ℓ′) # (H.unit.η _ # (ι₀ ⋆))) H⟨Δ⁺⟩.≤ H.mult.η _ # (H.M₁ (ℓ̅ ℓ) # (H.unit.η _ # (ι₀ ⋆))) + ν′⟨ℓ′⟩⟨⋆⟩<ν′⟨ℓ⟩⟨⋆⟩ = + H.mult.η _ # (H.M₁ (ℓ̅ ℓ′) # (H.unit.η _ # ι₀ ⋆)) ≐⟨ ap (H.mult.η _ #_) (sym $ H.unit.is-natural _ _ (ℓ̅ ℓ′) #ₚ _) ⟩ + H.mult.η _ # (H.unit.η _ # (H.M₁ ι₁-hom # ℓ′)) ≤⟨ (H.mult.η _ ∘ H.unit.η _ ∘ H.M₁ ι₁-hom) .mono ℓ′≤ℓ ⟩ + H.mult.η _ # (H.unit.η _ # (H.M₁ ι₁-hom # ℓ)) ≐⟨ ap (H.mult.η _ #_) (H.unit.is-natural _ _ (ℓ̅ ℓ) #ₚ _) ⟩ + H.mult.η _ # (H.M₁ (ℓ̅ ℓ) # (H.unit.η _ # ι₀ ⋆)) ≤∎ +-} ℓ̅-σ̅ : ∀ {ℓ : ⌞ fst Fᴴ⟨ Δ ⟩ ⌟} (σ : Algebra-hom _ _ Fᴴ⟨ Δ ⟩ Fᴴ⟨ Δ ⟩) → ℓ̅ (σ # ℓ) ≡ H.mult.η _ ∘ H.M₁ (σ̅ σ) ∘ ℓ̅ ℓ ℓ̅-σ̅ {ℓ} σ = ext λ where @@ -259,8 +280,8 @@ module _ {o r} (H : Hierarchy-theory o r) (Δ : Strict-order o r) (Ψ : Set (lsu nt : Uᴴ => Uᴹᴰ F∘ T nt ._=>_.η _ .hom (lift ℓ) = pt , ν′ ℓ - nt ._=>_.η _ .strict-mono (lift ℓ<ℓ′) = biased refl (ν′-strictly-mono ℓ<ℓ′) - nt ._=>_.is-natural _ _ σ = ext λ ℓ → + nt ._=>_.η _ .mono (lift ℓ≤ℓ′) = inc (biased refl (ν′-mono ℓ≤ℓ′)) + nt ._=>_.is-natural _ _ σ = ext λ ℓ → refl , λ α → H.mult.η _ # (H.M₁ (ℓ̅ (σ # ℓ .Lift.lower)) # α) ≡⟨ ap (λ e → (H.mult.η _ ∘ H.M₁ e) # α) (ℓ̅-σ̅ σ) ⟩ H.mult.η _ # (H.M₁ (H.mult.η _ ∘ H.M₁ (σ̅ σ) ∘ ℓ̅ (ℓ .Lift.lower)) # α) ≡⟨ ap (H.mult.η _ #_) ((H.M-∘ _ _ ∙ ((refl⟩∘⟨ H.M-∘ _ _))) #ₚ α) ⟩ diff --git a/src/Mugen/Cat/StrictOrders.agda b/src/Mugen/Cat/StrictOrders.agda index c9a7a90..a8fab0a 100644 --- a/src/Mugen/Cat/StrictOrders.agda +++ b/src/Mugen/Cat/StrictOrders.agda @@ -1,11 +1,11 @@ module Mugen.Cat.StrictOrders where open import Mugen.Prelude -open import Mugen.Order.StrictOrder +open import Mugen.Order.Poset private variable o r : Level - X Y Z : Strict-order o r + X Y Z : Poset o r -------------------------------------------------------------------------------- -- The Category of Strict Orders @@ -13,7 +13,7 @@ private variable open Precategory Strict-orders : ∀ (o r : Level) → Precategory (lsuc o ⊔ lsuc r) (o ⊔ r) -Strict-orders o r .Ob = Strict-order o r +Strict-orders o r .Ob = Poset o r 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 @@ -25,14 +25,14 @@ Strict-orders o r .assoc f g h = ext (λ _ → refl) Lift< : ∀ {o r} → (o′ r′ : Level) - → Strict-order o r - → Strict-order (o ⊔ o′) (r ⊔ r′) -Lift< o' r' X = to-strict-order mk where - open Strict-order X + → Poset o r + → Poset (o ⊔ o′) (r ⊔ r′) +Lift< o' r' X = to-poset mk where + open Poset X - mk : make-strict-order _ (Lift o' ⌞ X ⌟) - mk .make-strict-order._<_ x y = Lift r' (Lift.lower x < Lift.lower y) - mk .make-strict-order.<-irrefl (lift p) = <-irrefl p - mk .make-strict-order.<-trans (lift p) (lift q) = lift (<-trans p q) - mk .make-strict-order.<-thin = Lift-is-hlevel 1 <-thin - mk .make-strict-order.has-is-set = Lift-is-hlevel 2 has-is-set + 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) diff --git a/src/Mugen/Data/Int.agda b/src/Mugen/Data/Int.agda index d17086f..ed3290c 100644 --- a/src/Mugen/Data/Int.agda +++ b/src/Mugen/Data/Int.agda @@ -1,12 +1,7 @@ module Mugen.Data.Int where -open import Algebra.Magma -open import Algebra.Monoid -open import Algebra.Semigroup - open import Mugen.Prelude -open import Mugen.Algebra.Displacement -open import Mugen.Order.StrictOrder +open import Mugen.Order.Poset open import Mugen.Data.Nat data Int : Type where @@ -32,6 +27,9 @@ pos≠negsuc p = subst distinguish p tt where distinguish (pos _) = ⊤ distinguish (negsuc _) = ⊥ +negsuc≠pos : ∀ {m n} → negsuc m ≡ pos n → ⊥ +negsuc≠pos = pos≠negsuc ⊙ sym + pos-inj : ∀ {m n} → pos m ≡ pos n → m ≡ n pos-inj = ap abs @@ -54,27 +52,22 @@ instance -------------------------------------------------------------------------------- -- Algebra -diff : Nat → Nat → Int -diff zero zero = 0ℤ -diff zero (suc n) = negsuc n -diff (suc m) zero = pos (suc m) -diff (suc m) (suc n) = diff m n - -1+ℤ : Int → Int -1+ℤ (pos n) = pos (suc n) -1+ℤ (negsuc zero) = 0ℤ -1+ℤ (negsuc (suc n)) = negsuc n +succℤ : Int → Int +succℤ (pos n) = pos (suc n) +succℤ (negsuc zero) = 0ℤ +succℤ (negsuc (suc n)) = negsuc n -_-1ℤ : Int → Int -0ℤ -1ℤ = negsuc zero -pos (suc n) -1ℤ = pos n -negsuc n -1ℤ = negsuc (suc n) +predℤ : Int → Int +predℤ 0ℤ = negsuc zero +predℤ (pos (suc n)) = pos n +predℤ (negsuc n) = negsuc (suc n) +infixr 5 _+ℤ_ _+ℤ_ : Int → Int → Int -pos m +ℤ pos n = pos (m + n) -pos m +ℤ negsuc n = diff m (suc n) -negsuc m +ℤ pos n = diff n (suc m) -negsuc m +ℤ negsuc n = negsuc (suc (m + n)) +pos zero +ℤ y = y +pos (suc x) +ℤ y = succℤ (pos x +ℤ y) +negsuc zero +ℤ y = predℤ y +negsuc (suc x) +ℤ y = predℤ (negsuc x +ℤ y) maxℤ : Int → Int → Int maxℤ (pos x) (pos y) = pos (max x y) @@ -82,108 +75,74 @@ maxℤ (pos x) (negsuc _) = pos x maxℤ (negsuc _) (pos y) = pos y maxℤ (negsuc x) (negsuc y) = negsuc (min x y) +-- Properties + +succℤ-predℤ : ∀ x → x ≡ succℤ (predℤ x) +succℤ-predℤ (pos (suc _)) = refl +succℤ-predℤ (pos zero) = refl +succℤ-predℤ (negsuc _) = refl + +predℤ-succℤ : ∀ x → x ≡ predℤ (succℤ x) +predℤ-succℤ (pos _) = refl +predℤ-succℤ (negsuc zero) = refl +predℤ-succℤ (negsuc (suc _)) = refl + +ℤ-idl : ∀ x → 0ℤ +ℤ x ≡ x -+ℤ-idl (pos n) = refl -+ℤ-idl (negsuc n) = refl ++ℤ-idl x = refl +ℤ-idr : ∀ x → x +ℤ 0ℤ ≡ x -+ℤ-idr (pos x) = ap pos (+-zeror x) -+ℤ-idr (negsuc n) = refl - -diff-0ℤl : ∀ x → diff 0 x ≡ 1+ℤ (negsuc x) -diff-0ℤl zero = refl -diff-0ℤl (suc x) = refl - -diff-0ℤr : ∀ x → diff x 0 ≡ pos x -diff-0ℤr zero = refl -diff-0ℤr (suc x) = refl - -diff-sucl : ∀ x y → diff (suc x) y ≡ 1+ℤ (diff x y) -diff-sucl zero zero = refl -diff-sucl zero (suc y) = diff-0ℤl y -diff-sucl (suc x) zero = refl -diff-sucl (suc x) (suc y) = diff-sucl x y - -diff-sucr : ∀ x y → diff x (suc y) ≡ (diff x y) -1ℤ -diff-sucr zero zero = refl -diff-sucr zero (suc y) = refl -diff-sucr (suc x) zero = diff-0ℤr x -diff-sucr (suc x) (suc y) = diff-sucr x y - -+ℤ-sucl : ∀ x y → pos (suc x) +ℤ y ≡ 1+ℤ (pos x +ℤ y) -+ℤ-sucl zero (pos y) = refl -+ℤ-sucl zero (negsuc y) = diff-0ℤl y -+ℤ-sucl (suc x) (pos n) = refl -+ℤ-sucl (suc x) (negsuc y) = diff-sucl x y - -+ℤ-sucr : ∀ x y → x +ℤ (pos (suc y)) ≡ 1+ℤ (x +ℤ pos y) -+ℤ-sucr (pos x) y = ap pos (+-sucr x y) -+ℤ-sucr (negsuc x) zero = diff-0ℤl x -+ℤ-sucr (negsuc x) (suc y) = diff-sucl y x - -+ℤ-diff-posl : ∀ x y z → pos x +ℤ (diff y z) ≡ diff (x + y) z -+ℤ-diff-posl zero y z = +ℤ-idl (diff y z) -+ℤ-diff-posl (suc x) y z = - pos (suc x) +ℤ diff y z ≡⟨ +ℤ-sucl x (diff y z) ⟩ - 1+ℤ (pos x +ℤ diff y z) ≡⟨ ap 1+ℤ (+ℤ-diff-posl x y z) ⟩ - 1+ℤ (diff (x + y) z) ≡˘⟨ diff-sucl (x + y) z ⟩ - diff (suc (x + y)) z ∎ - -+ℤ-diff-posr : ∀ x y z → diff x y +ℤ pos z ≡ diff (x + z) y -+ℤ-diff-posr zero zero z = sym (diff-0ℤr z) -+ℤ-diff-posr zero (suc y) z = refl -+ℤ-diff-posr (suc x) zero z = refl -+ℤ-diff-posr (suc x) (suc y) z = +ℤ-diff-posr x y z - -+ℤ-diff-negl : ∀ x y z → negsuc x +ℤ diff y z ≡ diff y (suc (x + z)) -+ℤ-diff-negl x zero zero = ap negsuc (sym $ +-zeror x) -+ℤ-diff-negl x zero (suc z) = ap negsuc (sym $ +-sucr x z) -+ℤ-diff-negl x (suc y) zero = ap (diff y) (sym $ +-zeror x) -+ℤ-diff-negl x (suc y) (suc z) = - negsuc x +ℤ diff y z ≡⟨ +ℤ-diff-negl x y z ⟩ - diff y (suc (x + z)) ≡˘⟨ ap (diff y) (+-sucr x z) ⟩ - diff y (x + suc z) ∎ - -+ℤ-diff-negr : ∀ x y z → diff x y +ℤ negsuc z ≡ diff x (suc (y + z)) -+ℤ-diff-negr zero zero z = refl -+ℤ-diff-negr zero (suc y) z = refl -+ℤ-diff-negr (suc x) zero z = refl -+ℤ-diff-negr (suc x) (suc y) z = +ℤ-diff-negr x y z - -infixr 5 _+ℤ_ ++ℤ-idr (pos zero) = refl ++ℤ-idr (pos (suc n)) = ap succℤ $ +ℤ-idr (pos n) ++ℤ-idr (negsuc zero) = refl ++ℤ-idr (negsuc (suc n)) = ap predℤ $ +ℤ-idr (negsuc n) + ++ℤ-succl : ∀ x y → succℤ x +ℤ y ≡ succℤ (x +ℤ y) ++ℤ-succl (pos x) y = refl ++ℤ-succl (negsuc zero) y = succℤ-predℤ y ++ℤ-succl (negsuc (suc x)) y = succℤ-predℤ (negsuc x +ℤ y) + ++ℤ-succr : ∀ x y → x +ℤ succℤ y ≡ succℤ (x +ℤ y) ++ℤ-succr (pos zero) y = refl ++ℤ-succr (pos (suc x)) y = ap succℤ $ +ℤ-succr (pos x) y ++ℤ-succr (negsuc zero) y = sym (predℤ-succℤ y) ∙ succℤ-predℤ y ++ℤ-succr (negsuc (suc x)) y = + ap predℤ (+ℤ-succr (negsuc x) y) ∙ sym (predℤ-succℤ (negsuc x +ℤ y)) ∙ succℤ-predℤ (negsuc x +ℤ y) + ++ℤ-predl : ∀ x y → predℤ x +ℤ y ≡ predℤ (x +ℤ y) ++ℤ-predl (pos zero) y = refl ++ℤ-predl (pos (suc x)) y = predℤ-succℤ (pos x +ℤ y) ++ℤ-predl (negsuc zero) y = refl ++ℤ-predl (negsuc (suc _)) y = refl + ++ℤ-predr : ∀ x y → x +ℤ predℤ y ≡ predℤ (x +ℤ y) ++ℤ-predr (pos zero) y = refl ++ℤ-predr (pos (suc x)) y = + ap succℤ (+ℤ-predr (pos x) y) ∙ sym (succℤ-predℤ (pos x +ℤ y)) ∙ predℤ-succℤ (pos x +ℤ y) ++ℤ-predr (negsuc zero) y = refl ++ℤ-predr (negsuc (suc x)) y = + ap predℤ (+ℤ-predr (negsuc x) y) +ℤ-associative : ∀ x y z → x +ℤ (y +ℤ z) ≡ (x +ℤ y) +ℤ z -+ℤ-associative (pos x) (pos y) (pos z) = - ap pos (+-associative x y z) -+ℤ-associative (pos x) (pos y) (negsuc z) = - +ℤ-diff-posl x y (suc z) -+ℤ-associative (pos x) (negsuc y) (pos z) = - pos x +ℤ diff z (suc y) ≡⟨ +ℤ-diff-posl x z (suc y) ⟩ - diff (x + z) (suc y) ≡˘⟨ +ℤ-diff-posr x (suc y) z ⟩ - diff x (suc y) +ℤ pos z ∎ -+ℤ-associative (pos x) (negsuc y) (negsuc z) = - sym (+ℤ-diff-negr x (suc y) z) -+ℤ-associative (negsuc x) (pos y) (pos z) = - sym (+ℤ-diff-posr y (suc x) z) -+ℤ-associative (negsuc x) (pos y) (negsuc z) = - negsuc x +ℤ diff y (suc z) ≡⟨ +ℤ-diff-negl x y (suc z) ⟩ - diff y (suc x + suc z) ≡⟨ ap (diff y) (+-sucr (suc x) z) ⟩ - diff y (suc (suc x) + z) ≡˘⟨ +ℤ-diff-negr y (suc x) z ⟩ - diff y (suc x) +ℤ negsuc z ∎ -+ℤ-associative (negsuc x) (negsuc y) (pos z) = - negsuc x +ℤ diff z (suc y) ≡⟨ +ℤ-diff-negl x z (suc y) ⟩ - diff z (suc x + suc y) ≡⟨ ap (diff z) (+-sucr (suc x) y) ⟩ - diff z (suc (suc x) + y) ∎ -+ℤ-associative (negsuc x) (negsuc y) (negsuc z) = - negsuc (suc (x + suc (y + z))) ≡⟨ ap negsuc (+-sucr (suc x) (y + z)) ⟩ - negsuc (suc (suc (x + (y + z)))) ≡⟨ ap negsuc (+-associative (suc (suc x)) y z) ⟩ - negsuc (suc (suc (x + y + z))) ∎ ++ℤ-associative (pos zero) y z = refl ++ℤ-associative (pos (suc x)) y z = + succℤ (pos x +ℤ (y +ℤ z)) ≡⟨ ap succℤ (+ℤ-associative (pos x) y z) ⟩ + succℤ ((pos x +ℤ y) +ℤ z) ≡˘⟨ +ℤ-succl (pos x +ℤ y) z ⟩ + (succℤ (pos x +ℤ y) +ℤ z) ∎ ++ℤ-associative (negsuc zero) y z = sym $ +ℤ-predl y z ++ℤ-associative (negsuc (suc x)) y z = + predℤ (negsuc x +ℤ (y +ℤ z)) ≡⟨ ap predℤ (+ℤ-associative (negsuc x) y z) ⟩ + predℤ ((negsuc x +ℤ y) +ℤ z) ≡˘⟨ +ℤ-predl (negsuc x +ℤ y) z ⟩ + (predℤ (negsuc x +ℤ y) +ℤ z) ∎ +ℤ-negate : ∀ x y → - (x + y) ≡ (- x) +ℤ (- y) -+ℤ-negate zero zero = refl -+ℤ-negate zero (suc y) = refl -+ℤ-negate (suc x) zero = ap negsuc (+-zeror x) -+ℤ-negate (suc x) (suc y) = ap negsuc (+-sucr x y) ++ℤ-negate zero y = refl ++ℤ-negate (suc zero) zero = refl ++ℤ-negate (suc zero) (suc y) = refl ++ℤ-negate (suc (suc x)) y = ap predℤ $ +ℤ-negate (suc x) y + ++ℤ-pos : ∀ x y → pos (x + y) ≡ pos x +ℤ pos y ++ℤ-pos zero y = refl ++ℤ-pos (suc x) y = ap succℤ $ +ℤ-pos x y negate-inj : ∀ x y → (- x) ≡ (- y) → x ≡ y negate-inj zero zero p = refl @@ -191,31 +150,47 @@ 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-inj p) +succℤ-inj : ∀ x y → succℤ x ≡ succℤ y → x ≡ y +succℤ-inj (pos _) (pos _) p = ap predℤ p +succℤ-inj (pos _) (negsuc zero) p = ap predℤ p +succℤ-inj (pos _) (negsuc (suc _)) p = ap predℤ p +succℤ-inj (negsuc zero) (pos _) p = ap predℤ p +succℤ-inj (negsuc zero) (negsuc zero) p = ap predℤ p +succℤ-inj (negsuc zero) (negsuc (suc _)) p = ap predℤ p +succℤ-inj (negsuc (suc _)) (pos _) p = ap predℤ p +succℤ-inj (negsuc (suc _)) (negsuc zero) p = ap predℤ p +succℤ-inj (negsuc (suc _)) (negsuc (suc _)) p = ap predℤ p + +predℤ-inj : ∀ x y → predℤ x ≡ predℤ y → x ≡ y +predℤ-inj (pos zero) (pos zero) p = ap succℤ p +predℤ-inj (pos zero) (pos (suc _)) p = ap succℤ p +predℤ-inj (pos zero) (negsuc _) p = ap succℤ p +predℤ-inj (pos (suc _)) (pos zero) p = ap succℤ p +predℤ-inj (pos (suc _)) (pos (suc _)) p = ap succℤ p +predℤ-inj (pos (suc _)) (negsuc _) p = ap succℤ p +predℤ-inj (negsuc _) (pos zero) p = ap succℤ p +predℤ-inj (negsuc _) (pos (suc _)) p = ap succℤ p +predℤ-inj (negsuc _) (negsuc _) p = ap succℤ 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 $ succℤ-inj (pos k +ℤ x) (pos k +ℤ y) p ++ℤ-injr (negsuc zero) x y p = predℤ-inj x y p ++ℤ-injr (negsuc (suc k)) x y p = + +ℤ-injr (negsuc k) x y $ predℤ-inj (negsuc k +ℤ x) (negsuc k +ℤ y) p + -------------------------------------------------------------------------------- -- Order -_<ℤ_ : Int → Int → Type -pos x <ℤ pos y = x < y -pos x <ℤ negsuc y = ⊥ -negsuc x <ℤ pos y = ⊤ -negsuc x <ℤ negsuc y = y < x - _≤ℤ_ : Int → Int → Type pos x ≤ℤ pos y = x ≤ y pos x ≤ℤ negsuc y = ⊥ negsuc x ≤ℤ pos y = ⊤ negsuc x ≤ℤ negsuc y = y ≤ x - -<ℤ-irrefl : ∀ x → x <ℤ x → ⊥ -<ℤ-irrefl (pos x) = <-irrefl refl -<ℤ-irrefl (negsuc x) = <-irrefl refl - -<ℤ-trans : ∀ x y z → x <ℤ y → y <ℤ z → x <ℤ z -<ℤ-trans (pos x) (pos y) (pos z) x