diff --git a/src/Mugen/Algebra/Displacement/FiniteSupport.agda b/src/Mugen/Algebra/Displacement/FiniteSupport.agda
index 565f682..4d8ee41 100644
--- a/src/Mugen/Algebra/Displacement/FiniteSupport.agda
+++ b/src/Mugen/Algebra/Displacement/FiniteSupport.agda
@@ -9,7 +9,7 @@ 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.IndexedProduct
 open import Mugen.Algebra.Displacement.NearlyConstant
 open import Mugen.Algebra.OrderedMonoid
 
@@ -127,11 +127,11 @@ module _
     mk .make-displacement-subalgebra.mono _ _ xs<ys = xs<ys
     mk .make-displacement-subalgebra.inj = fin-support-list-path
 
-  FinSupport⊆InfProd : is-displacement-subalgebra (FiniteSupport 𝒟 _≡?_) (InfProd 𝒟)
-  FinSupport⊆InfProd =
+  FinSupport⊆IndProd : is-displacement-subalgebra (FiniteSupport 𝒟 _≡?_) (IndProd Nat λ _ → 𝒟)
+  FinSupport⊆IndProd =
     is-displacement-subalgebra-trans
       FinSupport⊆NearlyConstant
-      (NearlyConstant⊆InfProd _≡?_)
+      (NearlyConstant⊆IndProd _≡?_)
 
 --------------------------------------------------------------------------------
 -- Ordered Monoid
diff --git a/src/Mugen/Algebra/Displacement/IndexedProduct.agda b/src/Mugen/Algebra/Displacement/IndexedProduct.agda
new file mode 100644
index 0000000..58c09c2
--- /dev/null
+++ b/src/Mugen/Algebra/Displacement/IndexedProduct.agda
@@ -0,0 +1,155 @@
+module Mugen.Algebra.Displacement.IndexedProduct where
+
+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.OrderedMonoid
+
+--------------------------------------------------------------------------------
+-- Functional Displacement
+-- XXX New Section: ???
+--
+-- The infinite product of a displacement algebra '𝒟' consists
+-- of functions 'A → 𝒟'. Multiplication is performed pointwise,
+-- and ordering is given by 'f ≤ g' if '∀ n. f n ≤ n'.
+
+module Ind {o o' r} (A : Type o) (𝒟 : A → Displacement-algebra o' r) where
+  private
+    module 𝒟 {a : A} = Displacement-algebra (𝒟 a)
+    open 𝒟 using (ε; _⊗_)
+
+  _fun⊗_ : (∀ a → ⌞ 𝒟 a ⌟) → (∀ a → ⌞ 𝒟 a ⌟) → (∀ a → ⌞ 𝒟 a ⌟)
+  f fun⊗ g = λ a → f a ⊗ g a
+
+  funε : (a : A) → ⌞ 𝒟 a ⌟
+  funε _ = ε
+
+  fun⊗-associative : ∀ {f g h : (a : A) → ⌞ 𝒟 a ⌟} → (f fun⊗ (g fun⊗ h)) ≡ ((f fun⊗ g) fun⊗ h)
+  fun⊗-associative = funext λ x → 𝒟.associative
+
+  fun⊗-idl : ∀ {f : (a : A) → ⌞ 𝒟 a ⌟} → (funε fun⊗ f) ≡ f
+  fun⊗-idl = funext λ x → 𝒟.idl
+
+  fun⊗-idr : ∀ {f : (a : A) → ⌞ 𝒟 a ⌟} → (f fun⊗ funε) ≡ f
+  fun⊗-idr = funext λ x → 𝒟.idr
+
+  --------------------------------------------------------------------------------
+  -- Algebra
+
+  fun⊗-is-magma : is-magma _fun⊗_
+  fun⊗-is-magma .has-is-set = Π-is-hlevel 2 (λ _ → 𝒟.has-is-set)
+
+  fun⊗-is-semigroup : is-semigroup _fun⊗_
+  fun⊗-is-semigroup .has-is-magma = fun⊗-is-magma
+  fun⊗-is-semigroup .associative = fun⊗-associative
+
+  fun⊗-is-monoid : is-monoid funε _fun⊗_
+  fun⊗-is-monoid .has-is-semigroup = fun⊗-is-semigroup
+  fun⊗-is-monoid .idl = fun⊗-idl
+  fun⊗-is-monoid .idr = fun⊗-idr
+
+  --------------------------------------------------------------------------------
+  -- Ordering
+
+  _fun≤_ : ∀ (f g : ∀ a → ⌞ 𝒟 a ⌟) → Type (o ⊔ r)
+  f fun≤ g = (n : A) → f n 𝒟.≤ g n
+
+  _fun<_ : ∀ (f g : ∀ a → ⌞ 𝒟 a ⌟) → Type (o ⊔ o' ⊔ r)
+  _fun<_ = strict _fun≤_
+
+  fun≤-thin : ∀ {f g} → is-prop (f fun≤ g)
+  fun≤-thin = hlevel 1
+
+  fun≤-refl : ∀ {f : ∀ a → ⌞ 𝒟 a ⌟} → f fun≤ f
+  fun≤-refl = λ _ → 𝒟.≤-refl
+
+  fun≤-trans : ∀ {f g h} → f fun≤ g → g fun≤ h → f fun≤ h
+  fun≤-trans f≤g g≤h n = 𝒟.≤-trans (f≤g n) (g≤h n)
+
+  fun≤-antisym : ∀ {f g} → f fun≤ g → g fun≤ f → f ≡ g
+  fun≤-antisym f≤g g≤f = funext λ n → 𝒟.≤-antisym (f≤g n) (g≤f n)
+
+  fun⊗-left-invariant : ∀ {f g h} → g fun≤ h → (f fun⊗ g) fun≤ (f fun⊗ h)
+  fun⊗-left-invariant g≤h n = 𝒟.≤-left-invariant (g≤h n)
+
+  fun⊗-injr-on-fun≤ : ∀ {f g h} → g fun≤ h → (f fun⊗ g) ≡ (f fun⊗ h) → g ≡ h
+  fun⊗-injr-on-fun≤ g≤h fg=fh = funext λ n → 𝒟.injr-on-≤ (g≤h n) (happly fg=fh n)
+
+Ind : ∀ {o o' r} (A : Type o) → (A → Displacement-algebra o' r) → Poset (o ⊔ o') (o ⊔ r)
+Ind {o = o} {o' = o'} {r = r} A 𝒟 = to-poset mk where
+  open Ind A 𝒟
+  open make-poset
+
+  mk : make-poset (o ⊔ r) (∀ a → ⌞ 𝒟 a ⌟)
+  mk ._≤_ = _fun≤_
+  mk .≤-refl = fun≤-refl
+  mk .≤-trans = fun≤-trans
+  mk .≤-thin = fun≤-thin
+  mk .≤-antisym = fun≤-antisym
+
+module _ {o o' r} (A : Type o) (𝒟 : A → Displacement-algebra o' r) where
+  open Ind A 𝒟
+  open make-displacement-algebra
+  private module 𝒟 {a : A} = Displacement-algebra (𝒟 a)
+
+  --------------------------------------------------------------------------------
+  -- Displacement Algebra
+
+  IndProd : Displacement-algebra (o ⊔ o') (o ⊔ r)
+  IndProd = to-displacement-algebra mk where
+    mk : make-displacement-algebra (Ind A 𝒟)
+    mk .ε = funε
+    mk ._⊗_ = _fun⊗_
+    mk .idl = fun⊗-idl
+    mk .idr = fun⊗-idr
+    mk .associative = fun⊗-associative
+    mk .≤-left-invariant = fun⊗-left-invariant
+    mk .injr-on-≤ = fun⊗-injr-on-fun≤
+
+  --------------------------------------------------------------------------------
+  -- Ordered Monoid
+
+  private module 𝒟∞ = Displacement-algebra IndProd
+
+  fun⊗-has-ordered-monoid : (∀ a → has-ordered-monoid (𝒟 a))
+    → has-ordered-monoid IndProd
+  fun⊗-has-ordered-monoid 𝒟-om =
+    right-invariant→has-ordered-monoid
+      IndProd
+      fun⊗-right-invariant
+    where
+      open module M {a : A} = is-ordered-monoid (𝒟-om a)
+
+      fun⊗-right-invariant : ∀ {f g h} → f 𝒟∞.≤ g → (f fun⊗ h) 𝒟∞.≤ (g fun⊗ h)
+      fun⊗-right-invariant f≤g n = right-invariant (f≤g n)
+
+  --------------------------------------------------------------------------------
+  -- Joins
+
+  fun⊗-has-joins : ((a : A) → has-joins (𝒟 a))
+    → has-joins IndProd
+  fun⊗-has-joins 𝒟-joins = joins
+    where
+      open module J {a : A} = has-joins (𝒟-joins a)
+
+      joins : has-joins IndProd
+      joins .has-joins.join f g n = join (f n) (g n)
+      joins .has-joins.joinl = λ _ → joinl
+      joins .has-joins.joinr = λ _ → joinr
+      joins .has-joins.universal f≤h g≤h = λ n → universal (f≤h n) (g≤h n)
+
+  --------------------------------------------------------------------------------
+  -- Bottom
+
+  fun⊗-has-bottom : (∀ a → has-bottom (𝒟 a)) → has-bottom IndProd
+  fun⊗-has-bottom 𝒟-bottom = bottom
+    where
+      open module B {a : A} = has-bottom (𝒟-bottom a)
+
+      bottom : has-bottom IndProd
+      bottom .has-bottom.bot _ = bot
+      bottom .has-bottom.is-bottom f = λ n → is-bottom (f n)
diff --git a/src/Mugen/Algebra/Displacement/InfiniteProduct.agda b/src/Mugen/Algebra/Displacement/InfiniteProduct.agda
deleted file mode 100644
index 1172667..0000000
--- a/src/Mugen/Algebra/Displacement/InfiniteProduct.agda
+++ /dev/null
@@ -1,154 +0,0 @@
-module Mugen.Algebra.Displacement.InfiniteProduct where
-
-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.OrderedMonoid
-
---------------------------------------------------------------------------------
--- Infinite Products
--- Section 3.3.5
---
--- The infinite product of a displacement algebra '𝒟' consists
--- of functions 'Nat → 𝒟'. Multiplication is performed pointwise,
--- and ordering is given by 'f ≤ g' if '∀ n. f n ≤ n'.
-
-module Inf {o r} (𝒟 : Displacement-algebra o r) where
-  private
-    module 𝒟 = Displacement-algebra 𝒟
-    open 𝒟 using (ε; _⊗_)
-
-  _⊗∞_ : (Nat → ⌞ 𝒟 ⌟) → (Nat → ⌞ 𝒟 ⌟) → (Nat → ⌞ 𝒟 ⌟)
-  f ⊗∞ g = λ n → f n ⊗ g n
-
-  ε∞ : Nat → ⌞ 𝒟 ⌟
-  ε∞ _ = ε
-
-  ⊗∞-associative : ∀ {f g h : Nat → ⌞ 𝒟 ⌟} → (f ⊗∞ (g ⊗∞ h)) ≡ ((f ⊗∞ g) ⊗∞ h)
-  ⊗∞-associative = funext λ x → 𝒟.associative
-
-  ⊗∞-idl : ∀ {f : Nat → ⌞ 𝒟 ⌟} → (ε∞ ⊗∞ f) ≡ f
-  ⊗∞-idl = funext λ x → 𝒟.idl
-
-  ⊗∞-idr : ∀ {f : Nat → ⌞ 𝒟 ⌟} → (f ⊗∞ ε∞) ≡ f
-  ⊗∞-idr = funext λ x → 𝒟.idr
-
-  --------------------------------------------------------------------------------
-  -- Algebra
-
-  ⊗∞-is-magma : is-magma _⊗∞_
-  ⊗∞-is-magma .has-is-set = Π-is-hlevel 2 (λ _ → 𝒟.has-is-set)
-
-  ⊗∞-is-semigroup : is-semigroup _⊗∞_
-  ⊗∞-is-semigroup .has-is-magma = ⊗∞-is-magma
-  ⊗∞-is-semigroup .associative = ⊗∞-associative
-
-  ⊗∞-is-monoid : is-monoid ε∞ _⊗∞_
-  ⊗∞-is-monoid .has-is-semigroup = ⊗∞-is-semigroup
-  ⊗∞-is-monoid .idl = ⊗∞-idl
-  ⊗∞-is-monoid .idr = ⊗∞-idr
-
-  --------------------------------------------------------------------------------
-  -- Ordering
-
-  _inf≤_ : ∀ (f g : Nat → ⌞ 𝒟 ⌟) → Type r
-  f inf≤ g = (n : Nat) → f n 𝒟.≤ g n
-
-  _inf<_ : ∀ (f g : Nat → ⌞ 𝒟 ⌟) → Type (o ⊔ r)
-  _inf<_ = strict _inf≤_
-
-  inf≤-thin : ∀ {f g} → is-prop (f inf≤ g)
-  inf≤-thin = hlevel 1
-
-  inf≤-refl : ∀ {f : Nat → ⌞ 𝒟 ⌟} → f inf≤ f
-  inf≤-refl = λ _ → 𝒟.≤-refl
-
-  inf≤-trans : ∀ {f g h} → f inf≤ g → g inf≤ h → f inf≤ h
-  inf≤-trans f≤g g≤h n = 𝒟.≤-trans (f≤g n) (g≤h n)
-
-  inf≤-antisym : ∀ {f g} → f inf≤ g → g inf≤ f → f ≡ g
-  inf≤-antisym f≤g g≤f = funext λ n → 𝒟.≤-antisym (f≤g n) (g≤f n)
-
-  ⊗∞-left-invariant : ∀ {f g h : Nat → ⌞ 𝒟 ⌟} → g inf≤ h → (f ⊗∞ g) inf≤ (f ⊗∞ h)
-  ⊗∞-left-invariant g≤h n = 𝒟.≤-left-invariant (g≤h n)
-
-  ⊗∞-injr-on-inf≤ : ∀ {f g h : Nat → ⌞ 𝒟 ⌟} → g inf≤ h → (f ⊗∞ g) ≡ (f ⊗∞ h) → g ≡ h
-  ⊗∞-injr-on-inf≤ g≤h fg=fh = funext λ n → 𝒟.injr-on-≤ (g≤h n) (happly fg=fh n)
-
-Inf : ∀ {o r} → Displacement-algebra o r → Poset o r
-Inf {o = o} {r = r} 𝒟 = to-poset mk where
-  open Inf 𝒟
-  open make-poset
-
-  mk : make-poset r (Nat → ⌞ 𝒟 ⌟)
-  mk ._≤_ = _inf≤_
-  mk .≤-refl = inf≤-refl
-  mk .≤-trans = inf≤-trans
-  mk .≤-thin = inf≤-thin
-  mk .≤-antisym = inf≤-antisym
-
-module _ {o r} (𝒟 : Displacement-algebra o r) where
-  open Inf 𝒟
-  open make-displacement-algebra
-
-  --------------------------------------------------------------------------------
-  -- Displacement Algebra
-
-  private module 𝒟 = Displacement-algebra 𝒟
-
-  InfProd : Displacement-algebra o r
-  InfProd = to-displacement-algebra mk where
-    mk : make-displacement-algebra (Inf 𝒟)
-    mk .ε = ε∞
-    mk ._⊗_ = _⊗∞_
-    mk .idl = ⊗∞-idl
-    mk .idr = ⊗∞-idr
-    mk .associative = ⊗∞-associative
-    mk .≤-left-invariant = ⊗∞-left-invariant
-    mk .injr-on-≤ = ⊗∞-injr-on-inf≤
-
-  --------------------------------------------------------------------------------
-  -- Ordered Monoid
-
-  private module 𝒟∞ = Displacement-algebra InfProd
-
-  ⊗∞-has-ordered-monoid : has-ordered-monoid 𝒟 → has-ordered-monoid InfProd
-  ⊗∞-has-ordered-monoid 𝒟-om =
-    right-invariant→has-ordered-monoid
-      InfProd
-      ⊗∞-right-invariant
-    where
-      open is-ordered-monoid 𝒟-om
-
-      ⊗∞-right-invariant : ∀ {f g h} → f 𝒟∞.≤ g → (f ⊗∞ h) 𝒟∞.≤ (g ⊗∞ h)
-      ⊗∞-right-invariant f≤g n = right-invariant (f≤g n)
-
-  --------------------------------------------------------------------------------
-  -- Joins
-
-  ⊗∞-has-joins : has-joins 𝒟 → has-joins InfProd
-  ⊗∞-has-joins 𝒟-joins = joins
-    where
-      open has-joins 𝒟-joins
-
-      joins : has-joins InfProd
-      joins .has-joins.join f g n = join (f n) (g n)
-      joins .has-joins.joinl = λ _ → joinl
-      joins .has-joins.joinr = λ _ → joinr
-      joins .has-joins.universal f≤h g≤h = λ n → universal (f≤h n) (g≤h n)
-
-  --------------------------------------------------------------------------------
-  -- Bottom
-
-  ⊗∞-has-bottom : has-bottom 𝒟 → has-bottom InfProd
-  ⊗∞-has-bottom 𝒟-bottom = bottom
-    where
-      open has-bottom 𝒟-bottom
-
-      bottom : has-bottom InfProd
-      bottom .has-bottom.bot _ = bot
-      bottom .has-bottom.is-bottom f = λ n → is-bottom (f n)
diff --git a/src/Mugen/Algebra/Displacement/NearlyConstant.agda b/src/Mugen/Algebra/Displacement/NearlyConstant.agda
index ae0d151..53238b0 100644
--- a/src/Mugen/Algebra/Displacement/NearlyConstant.agda
+++ b/src/Mugen/Algebra/Displacement/NearlyConstant.agda
@@ -10,7 +10,7 @@ open import Mugen.Prelude
 open import Mugen.Data.List
 open import Mugen.Order.Poset
 open import Mugen.Algebra.Displacement
-open import Mugen.Algebra.Displacement.InfiniteProduct
+open import Mugen.Algebra.Displacement.IndexedProduct
 open import Mugen.Algebra.OrderedMonoid
 
 --------------------------------------------------------------------------------
@@ -29,7 +29,7 @@ open import Mugen.Algebra.OrderedMonoid
 -- prefix list "the support".
 --
 -- However, there is a slight problem here when we go to show that
--- this is a subalgebra of 'InfProd': it's not injective! The problem
+-- this is a subalgebra of 'IndProd': it's not injective! The problem
 -- occurs when you have trailing base elements, meaning 2 lists can
 -- denote the same function!
 --
@@ -43,7 +43,7 @@ module NearlyConst
   (_≡?_ : Discrete ⌞ 𝒟 ⌟)
   where
   private module 𝒟 = Displacement-algebra 𝒟
-  open Inf 𝒟
+  open Ind Nat (λ _ → 𝒟)
 
   --------------------------------------------------------------------------------
   -- Raw Support Lists
@@ -215,7 +215,7 @@ module NearlyConst
     -- Order
 
     _raw≤_ : RawList → RawList → Type r
-    xs raw≤ ys = index xs inf≤ index ys
+    xs raw≤ ys = index xs fun≤ index ys
 
     index= : RawList → RawList → Type o
     index= xs ys = (n : Nat) → index xs n ≡ index ys n
@@ -334,8 +334,8 @@ module NearlyConst
   -- 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 → (λ n → index-merge xs ys n i) inf≤ (λ n → index-merge xs zs n i)) $
-    ⊗∞-left-invariant ys≤zs
+    coe1→0 (λ i → (λ n → index-merge xs ys n i) fun≤ (λ n → index-merge xs zs n i)) $
+    fun⊗-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
@@ -347,7 +347,7 @@ module NearlyConst
 
 module _ {o r} (𝒟 : Displacement-algebra o r) (_≡?_ : Discrete ⌞ 𝒟 ⌟) where
   private module 𝒟 = Displacement-algebra 𝒟
-  open Inf 𝒟
+  open Ind Nat (λ _ → 𝒟)
   open NearlyConst 𝒟 _≡?_
 
   NearlyConstant : Displacement-algebra o r
@@ -355,10 +355,10 @@ module _ {o r} (𝒟 : Displacement-algebra o r) (_≡?_ : Discrete ⌞ 𝒟 ⌟
     open make-poset
     mk-poset : make-poset r SupportList
     mk-poset ._≤_ = _supp≤_
-    mk-poset .≤-refl = inf≤-refl
-    mk-poset .≤-trans = inf≤-trans
-    mk-poset .≤-thin = inf≤-thin
-    mk-poset .≤-antisym p q = index-inj $ inf≤-antisym p q
+    mk-poset .≤-refl = fun≤-refl
+    mk-poset .≤-trans = fun≤-trans
+    mk-poset .≤-thin = fun≤-thin
+    mk-poset .≤-antisym p q = index-inj $ fun≤-antisym p q
 
     open make-displacement-algebra
     mk : make-displacement-algebra (to-poset mk-poset)
@@ -390,9 +390,9 @@ module _ {o r} (𝒟 : Displacement-algebra o r) (_≡?_ : Discrete ⌞ 𝒟 ⌟
 module _ {o r} {𝒟 : Displacement-algebra o r} (_≡?_ : Discrete ⌞ 𝒟 ⌟) where
   open NearlyConst 𝒟 _≡?_
 
-  NearlyConstant⊆InfProd : is-displacement-subalgebra (NearlyConstant 𝒟 _≡?_) (InfProd 𝒟)
-  NearlyConstant⊆InfProd = to-displacement-subalgebra mk where
-    mk : make-displacement-subalgebra (NearlyConstant 𝒟 _≡?_) (InfProd 𝒟)
+  NearlyConstant⊆IndProd : is-displacement-subalgebra (NearlyConstant 𝒟 _≡?_) (IndProd Nat λ _ → 𝒟)
+  NearlyConstant⊆IndProd = to-displacement-subalgebra mk where
+    mk : make-displacement-subalgebra (NearlyConstant 𝒟 _≡?_) (IndProd Nat λ _ → 𝒟)
     mk .make-displacement-subalgebra.into = index
     mk .make-displacement-subalgebra.pres-ε = refl
     mk .make-displacement-subalgebra.pres-⊗ xs ys = funext (index-merge xs ys)
@@ -451,8 +451,8 @@ module NearlyConstJoins
   index-preserves-join : ∀ xs ys n → index (join xs ys) n ≡ 𝒥.join (index xs n) (index ys n)
   index-preserves-join = index-merge-with 𝒥.join
 
-  nearly-constant-is-subsemilattice : is-displacement-subsemilattice nearly-constant-has-joins (⊗∞-has-joins 𝒟 𝒟-joins)
-  nearly-constant-is-subsemilattice .is-displacement-subsemilattice.has-displacement-subalgebra = NearlyConstant⊆InfProd _≡?_
+  nearly-constant-is-subsemilattice : is-displacement-subsemilattice nearly-constant-has-joins (fun⊗-has-joins Nat (λ _ → 𝒟) (λ _ → 𝒟-joins))
+  nearly-constant-is-subsemilattice .is-displacement-subsemilattice.has-displacement-subalgebra = NearlyConstant⊆IndProd _≡?_
   nearly-constant-is-subsemilattice .is-displacement-subsemilattice.pres-joins x y = funext (index-preserves-join x y)
 
 --------------------------------------------------------------------------------
@@ -472,8 +472,8 @@ module _
   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 (⊗∞-has-bottom 𝒟 𝒟-bottom)
-  nearly-constant-is-bounded-subalgebra .is-bounded-displacement-subalgebra.has-displacement-subalgebra = NearlyConstant⊆InfProd _≡?_
+  nearly-constant-is-bounded-subalgebra : is-bounded-displacement-subalgebra nearly-constant-has-bottom (fun⊗-has-bottom Nat (λ _ → 𝒟) (λ _ → 𝒟-bottom))
+  nearly-constant-is-bounded-subalgebra .is-bounded-displacement-subalgebra.has-displacement-subalgebra = NearlyConstant⊆IndProd _≡?_
   nearly-constant-is-bounded-subalgebra .is-bounded-displacement-subalgebra.pres-bottom = refl
 
 --------------------------------------------------------------------------------
diff --git a/src/Mugen/Everything.agda b/src/Mugen/Everything.agda
index bd751ff..8e2ed78 100644
--- a/src/Mugen/Everything.agda
+++ b/src/Mugen/Everything.agda
@@ -8,7 +8,7 @@ import Mugen.Algebra.Displacement.Constant
 import Mugen.Algebra.Displacement.Endomorphism
 import Mugen.Algebra.Displacement.FiniteSupport
 import Mugen.Algebra.Displacement.Fractal
-import Mugen.Algebra.Displacement.InfiniteProduct
+import Mugen.Algebra.Displacement.IndexedProduct
 import Mugen.Algebra.Displacement.Int
 import Mugen.Algebra.Displacement.Lexicographic
 import Mugen.Algebra.Displacement.Nat