fix(NearlyConstant): major rewrite and cleanup: stage 4 (#30)

src/Mugen/Algebra/Displacement/FiniteSupport.agda

@@ -30,8 +30,8 @@ open import Mugen.Data.List
 module FinSupport {o r} (𝒟 : Displacement-algebra o r) (cmp : ∀ x y → Tri (Displacement-algebra._<_ 𝒟) x y) where
   private
     module 𝒟 = Displacement-algebra 𝒟
-    open 𝒟 using (ε; _⊗_; _<_; _≤_)
-  open NearlyConst 𝒟 cmp public
+    open 𝒟 using (ε; _⊗_)
+    module 𝒩 = NearlyConst 𝒟 cmp
 
   --------------------------------------------------------------------------------
   -- Finite Support Lists
@@ -42,9 +42,9 @@ module FinSupport {o r} (𝒟 : Displacement-algebra o r) (cmp : ∀ x y → Tri
   record FinSupportList : Type o where
     no-eta-equality
     field
-      support : SupportList
+      support : 𝒩.SupportList
 
-    open SupportList support public
+    open 𝒩.SupportList support public
 
     field
       is-ε : base ≡ ε
@@ -55,65 +55,59 @@ module FinSupport {o r} (𝒟 : Displacement-algebra o r) (cmp : ∀ x y → Tri
   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
+    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) ε
+      Σ-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-ε = ap₂ _⊗_ (xs .is-ε) (ys .is-ε) ∙ 𝒟.idl
+  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 .support = 𝒩.empty
   empty-fin .is-ε = refl
 
-  --------------------------------------------------------------------------------
-  -- Algebra
-
-
   --------------------------------------------------------------------------------
   -- Order
 
-  _merge-fin<_ : FinSupportList → FinSupportList → Type (o ⊔ r)
-  _merge-fin<_ xs ys = (xs .support) slist< (ys .support)
-
+  _<_ : FinSupportList → FinSupportList → Type (o ⊔ r)
+  _<_ xs ys = (xs .support) 𝒩.< (ys .support)
 
 --------------------------------------------------------------------------------
 -- Displacement Algebra
 
 module _ {o r} (𝒟 : Displacement-algebra o r) (cmp : ∀ x y → Tri (Displacement-algebra._<_ 𝒟) x y) where
   open FinSupport 𝒟 cmp
   open FinSupportList
+  private module 𝒩𝒟 = Displacement-algebra (NearlyConstant 𝒟 cmp)
 
   FiniteSupport : Displacement-algebra o (o ⊔ r)
   FiniteSupport = to-displacement-algebra mk where
     mk-strict : make-strict-order (o ⊔ r) FinSupportList
-    mk-strict .make-strict-order._<_ = _merge-fin<_
+    mk-strict .make-strict-order._<_ = _<_
     mk-strict .make-strict-order.<-irrefl {xs} =
-      list<-irrefl (base xs) (elts xs)
+      𝒩𝒟.<-irrefl {xs .support}
     mk-strict .make-strict-order.<-trans {xs} {ys} {zs} =
-      list<-trans (base xs) (elts xs) (base ys) (elts ys) (base zs) (elts zs)
+      𝒩𝒟.<-trans {xs .support} {ys .support} {zs .support}
     mk-strict .make-strict-order.<-thin {xs} {ys} =
-      list<-is-prop (base xs) (elts xs) (base ys) (elts 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 .make-displacement-algebra.ε = empty-fin
     mk .make-displacement-algebra._⊗_ = merge-fin
-    mk .make-displacement-algebra.idl {xs} =
-      fin-support-list-path (merge-idl (xs .support))
-    mk .make-displacement-algebra.idr {xs} =
-      fin-support-list-path (merge-idr (xs .support))
-    mk .make-displacement-algebra.associative {xs} {ys} {zs} =
-      fin-support-list-path (merge-assoc (xs .support) (ys .support) (zs .support))
+    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} =
-      slist<-left-invariant (support xs) (support ys) (support zs)
+      𝒩𝒟.left-invariant {xs .support} {ys .support} {zs .support}
 
 --------------------------------------------------------------------------------
 -- Subalgebra Structure
@@ -125,24 +119,21 @@ module _
   (cmp : ∀ x y → Tri 𝒟._<_ x y)
   where
   open FinSupport 𝒟 cmp
-  open FinSupportList
 
   FinSupport⊆NearlyConstant : is-displacement-subalgebra (FiniteSupport 𝒟 cmp) (NearlyConstant 𝒟 cmp)
   FinSupport⊆NearlyConstant = to-displacement-subalgebra mk where
     mk : make-displacement-subalgebra _ _
-    mk .make-displacement-subalgebra.into = support
+    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<ys = xs<ys
     mk .make-displacement-subalgebra.inj = fin-support-list-path
 
-{- TODO
   FinSupport⊆InfProd : is-displacement-subalgebra (FiniteSupport 𝒟 cmp) (InfProd 𝒟)
   FinSupport⊆InfProd =
     is-displacement-subalgebra-trans
       FinSupport⊆NearlyConstant
       (NearlyConstant⊆InfProd cmp)
--}
 
 --------------------------------------------------------------------------------
 -- Ordered Monoid
@@ -155,10 +146,7 @@ module _
   (cmp : ∀ x y → Tri 𝒟._<_ x y)
   where
   open FinSupport 𝒟 cmp
-  open FinSupportList
-  open NearlyConst 𝒟 cmp
-  open is-ordered-monoid 𝒟-ordered-monoid
 
   fin-support-ordered-monoid : has-ordered-monoid (FiniteSupport 𝒟 cmp)
   fin-support-ordered-monoid = right-invariant→has-ordered-monoid (FiniteSupport 𝒟 cmp) λ {xs} {ys} {zs} xs≤ys →
-    ⊎-mapl fin-support-list-path (merge-right-invariant 𝒟-ordered-monoid cmp (support xs) (support ys) (support zs) (⊎-mapl (ap support) xs≤ys))
+    ⊎-mapl fin-support-list-path (≤-right-invariant 𝒟-ordered-monoid cmp (⊎-mapl (ap FinSupportList.support) xs≤ys))

src/Mugen/Algebra/Displacement/InfiniteProduct.agda

@@ -30,14 +30,14 @@ module Inf {o r} (𝒟 : Displacement-algebra o r) where
   ε∞ : Nat → ⌞ 𝒟 ⌟
   ε∞ _ = ε
 
-  ⊗∞-associative : ∀ (f g h : Nat → ⌞ 𝒟 ⌟) → (f ⊗∞ (g ⊗∞ h)) ≡ ((f ⊗∞ g) ⊗∞ h)
-  ⊗∞-associative f g h = funext λ x → 𝒟.associative
+  ⊗∞-associative : ∀ {f g h : Nat → ⌞ 𝒟 ⌟} → (f ⊗∞ (g ⊗∞ h)) ≡ ((f ⊗∞ g) ⊗∞ h)
+  ⊗∞-associative = funext λ x → 𝒟.associative
 
-  ⊗∞-idl : ∀ (f : Nat → ⌞ 𝒟 ⌟) → (ε∞ ⊗∞ f) ≡ f
-  ⊗∞-idl f = funext λ x → 𝒟.idl
+  ⊗∞-idl : ∀ {f : Nat → ⌞ 𝒟 ⌟} → (ε∞ ⊗∞ f) ≡ f
+  ⊗∞-idl = funext λ x → 𝒟.idl
 
-  ⊗∞-idr : ∀ (f : Nat → ⌞ 𝒟 ⌟) → (f ⊗∞ ε∞) ≡ f
-  ⊗∞-idr f = funext λ x → 𝒟.idr
+  ⊗∞-idr : ∀ {f : Nat → ⌞ 𝒟 ⌟} → (f ⊗∞ ε∞) ≡ f
+  ⊗∞-idr = funext λ x → 𝒟.idr
 
   --------------------------------------------------------------------------------
   -- Algebra
@@ -47,47 +47,47 @@ module Inf {o r} (𝒟 : Displacement-algebra o r) where
 
   ⊗∞-is-semigroup : is-semigroup _⊗∞_
   ⊗∞-is-semigroup .has-is-magma = ⊗∞-is-magma
-  ⊗∞-is-semigroup .associative {f} {g} {h} = ⊗∞-associative f g h
+  ⊗∞-is-semigroup .associative = ⊗∞-associative
 
   ⊗∞-is-monoid : is-monoid ε∞ _⊗∞_
   ⊗∞-is-monoid .has-is-semigroup = ⊗∞-is-semigroup
-  ⊗∞-is-monoid .idl {f} = ⊗∞-idl f
-  ⊗∞-is-monoid .idr {f} = ⊗∞-idr f
+  ⊗∞-is-monoid .idl = ⊗∞-idl
+  ⊗∞-is-monoid .idr = ⊗∞-idr
 
   --------------------------------------------------------------------------------
   -- Ordering
 
   record _inf<_ (f g : Nat → ⌞ 𝒟 ⌟) : Type (o ⊔ r) where
     constructor inf-<
     field
-      ≤-everywhere : ∀ n →  f n 𝒟.≤ g n
-      not-equal    : ¬ ∀ (n : Nat) → f n ≡ g n
+      ≤-pointwise : ∀ n →  f n 𝒟.≤ g n
+      not-equal   : ¬ ∀ (n : Nat) → f n ≡ g n
 
   open _inf<_ public
 
-  inf≤-everywhere : ∀ {f g} → non-strict _inf<_ f g → ∀ n → f n 𝒟.≤ g n
-  inf≤-everywhere (inl f≡g) n = inl (happly f≡g n)
-  inf≤-everywhere (inr f<g) n = ≤-everywhere f<g n
+  inf≤-pointwise : ∀ {f g} → non-strict _inf<_ f g → ∀ n → f n 𝒟.≤ g n
+  inf≤-pointwise (inl f≡g) n = inl (happly f≡g n)
+  inf≤-pointwise (inr f<g) n = f<g .≤-pointwise n
 
-  inf<-irrefl : ∀ (f : Nat → ⌞ 𝒟 ⌟) → f inf< f → ⊥
-  inf<-irrefl f f<f = not-equal f<f λ _ → refl
+  inf<-irrefl : ∀ {f : Nat → ⌞ 𝒟 ⌟} → f inf< f → ⊥
+  inf<-irrefl f<f = f<f .not-equal λ _ → refl
 
-  inf<-trans : ∀ (f g h : Nat → ⌞ 𝒟 ⌟) → f inf< g → g inf< h → f inf< h
-  inf<-trans f g h f<g g<h .≤-everywhere n = 𝒟.≤-trans (≤-everywhere f<g n) (≤-everywhere g<h n)
-  inf<-trans f g h f<g g<h .not-equal f=h =
-    g<h .not-equal λ n → 𝒟.≤-antisym (g<h .≤-everywhere n) $ subst (𝒟._≤ _) (f=h n) (f<g .≤-everywhere n)
+  inf<-trans : ∀ {f g h} → f inf< g → g inf< h → f inf< h
+  inf<-trans f<g g<h .≤-pointwise n = 𝒟.≤-trans (f<g .≤-pointwise n) (g<h .≤-pointwise n)
+  inf<-trans f<g g<h .not-equal f=h =
+    g<h .not-equal λ n → 𝒟.≤-antisym (g<h .≤-pointwise n) $ 𝒟.≡+≤→≤ (sym $ f=h n) (f<g .≤-pointwise n)
 
-  inf<-is-prop : ∀ f g → is-prop (f inf< g)
-  inf<-is-prop f g f<g f<g′ i .≤-everywhere n = 𝒟.≤-thin (≤-everywhere f<g n) (≤-everywhere f<g′ n) i
-  inf<-is-prop f g f<g f<g′ i .not-equal = hlevel 1 (f<g .not-equal) (f<g′ .not-equal) i
+  inf<-is-prop : ∀ {f g} → is-prop (f inf< g)
+  inf<-is-prop f<g f<g′ i .≤-pointwise n = 𝒟.≤-thin (≤-pointwise f<g n) (≤-pointwise f<g′ n) i
+  inf<-is-prop f<g f<g′ i .not-equal = hlevel 1 (f<g .not-equal) (f<g′ .not-equal) i
 
   --------------------------------------------------------------------------------
   -- Left Invariance
 
-  ⊗∞-left-invariant : ∀ (f g h : Nat → ⌞ 𝒟 ⌟) → g inf< h → (f ⊗∞ g) inf< (f ⊗∞ h)
-  ⊗∞-left-invariant f g h g<h .≤-everywhere n = 𝒟.≤-left-invariant (≤-everywhere g<h n)
-  ⊗∞-left-invariant f g h g<h .not-equal p =
-    g<h .not-equal λ n → 𝒟.≤+≮→= (g<h .≤-everywhere n) (λ gn<hn → 𝒟.<→≠ (𝒟.left-invariant gn<hn) (p n))
+  ⊗∞-left-invariant : ∀ {f g h : Nat → ⌞ 𝒟 ⌟} → g inf< h → (f ⊗∞ g) inf< (f ⊗∞ h)
+  ⊗∞-left-invariant g<h .≤-pointwise n = 𝒟.≤-left-invariant (≤-pointwise g<h n)
+  ⊗∞-left-invariant g<h .not-equal p =
+    g<h .not-equal λ n → 𝒟.≤+≮→= (g<h .≤-pointwise n) λ gn<hn → 𝒟.<→≠ (𝒟.left-invariant gn<hn) (p n)
 
 
 Inf : ∀ {o r} → Displacement-algebra o r → Strict-order o (o ⊔ r)
@@ -98,9 +98,9 @@ Inf {o = o} {r = r} 𝒟 = to-strict-order mk where
 
   mk : make-strict-order (o ⊔ r) (Nat → ⌞ 𝒟 ⌟)
   mk ._<_ = _inf<_
-  mk .<-irrefl {x} = inf<-irrefl x
-  mk .<-trans {x} {y} {z} = inf<-trans x y z
-  mk .<-thin {x} {y} = inf<-is-prop x y
+  mk .<-irrefl = inf<-irrefl
+  mk .<-trans = inf<-trans
+  mk .<-thin = inf<-is-prop
   mk .has-is-set = Π-is-hlevel 2 λ _ → 𝒟.has-is-set
 
 InfProd : ∀ {o r} → Displacement-algebra o r → Displacement-algebra o (o ⊔ r)
@@ -112,10 +112,10 @@ InfProd {o = o} {r = r} 𝒟 = to-displacement-algebra mk where
   mk : make-displacement-algebra (Inf 𝒟)
   mk .ε = ε∞
   mk ._⊗_ = _⊗∞_
-  mk .idl {x} = ⊗∞-idl x
-  mk .idr {x} = ⊗∞-idr x
-  mk .associative {x} {y} {z} = ⊗∞-associative x y z
-  mk .left-invariant {x} {y} {z} = ⊗∞-left-invariant x y z
+  mk .idl = ⊗∞-idl
+  mk .idr = ⊗∞-idr
+  mk .associative = ⊗∞-associative
+  mk .left-invariant = ⊗∞-left-invariant
 
 -- All of the following results require a form of the Weak Limited Principle of Omniscience,
 -- which states that '∀ n. f n ≡ g n' is a decidable property.
@@ -130,7 +130,7 @@ module InfProperties
     module 𝒟∞ = Displacement-algebra (InfProd 𝒟)
 
     wlpo : ∀ {f g} → (∀ n → f n 𝒟.≤ g n) → f 𝒟∞.≤ g
-    wlpo p = Dec-rec (λ f=g → inl $ funext f=g) (λ neq → inr $ Inf.inf-< p neq) (𝒟-wlpo p)
+    wlpo p = Dec-rec (inl ⊙ funext) (inr ⊙ Inf.inf-< p) (𝒟-wlpo p)
 
   --------------------------------------------------------------------------------
   -- Ordered Monoid
@@ -144,7 +144,7 @@ module InfProperties
       open is-ordered-monoid 𝒟-om
 
       ⊗∞-right-invariant : ∀ {f g h} → f 𝒟∞.≤ g → (f ⊗∞ h) 𝒟∞.≤ (g ⊗∞ h)
-      ⊗∞-right-invariant f≤g = wlpo (λ n → right-invariant (inf≤-everywhere f≤g n))
+      ⊗∞-right-invariant f≤g = wlpo λ n → right-invariant (inf≤-pointwise f≤g n)
 
   --------------------------------------------------------------------------------
   -- Joins
@@ -158,7 +158,7 @@ module InfProperties
       joins .has-joins.join f g n = join (f n) (g n)
       joins .has-joins.joinl = wlpo λ _ → joinl
       joins .has-joins.joinr = wlpo λ _ → joinr
-      joins .has-joins.universal f≤h g≤h = wlpo λ n → universal (inf≤-everywhere f≤h n) (inf≤-everywhere g≤h n)
+      joins .has-joins.universal f≤h g≤h = wlpo λ n → universal (inf≤-pointwise f≤h n) (inf≤-pointwise g≤h n)
 
   --------------------------------------------------------------------------------
   -- Bottom