diff --git a/Lattice/Bundles/FiniteValueMap.agda b/Lattice/Bundles/FiniteValueMap.agda
deleted file mode 100644
index 41ecf30..0000000
--- a/Lattice/Bundles/FiniteValueMap.agda
+++ /dev/null
@@ -1,30 +0,0 @@
-open import Relation.Binary.PropositionalEquality using (_≡_)
-open import Relation.Binary.Definitions using (Decidable)
-
-module Lattice.Bundles.FiniteValueMap (A B : Set) (≡-dec-A : Decidable (_≡_ {_} {A})) where
-
-open import Lattice
-open import Data.List using (List)
-open import Data.Nat using (ℕ)
-open import Utils using (Unique)
-
-module FromFiniteHeightLattice (fhB : FiniteHeightLattice B)
-                               {ks : List A} (uks : Unique ks)
-                               (≈₂-dec : Decidable (FiniteHeightLattice._≈_ fhB)) where
-
-    open Lattice.FiniteHeightLattice fhB using () renaming
-        ( _≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_
-        ; height to height₂
-        ; isLattice to isLattice₂
-        ; fixedHeight to fixedHeight₂
-        )
-
-    import Lattice.FiniteMap
-    module FM = Lattice.FiniteMap ≡-dec-A isLattice₂
-    open FM.WithKeys ks public
-
-    import Lattice.FiniteValueMap
-    module FVM = Lattice.FiniteValueMap ≡-dec-A isLattice₂
-    open FVM.IterProdIsomorphism.WithUniqueKeysAndFixedHeight uks ≈₂-dec height₂ fixedHeight₂ public
-
-    ≈-dec = ≈₂-dec⇒≈-dec ≈₂-dec
diff --git a/Lattice/Bundles/IterProd.agda b/Lattice/Bundles/IterProd.agda
deleted file mode 100644
index 3071d0a..0000000
--- a/Lattice/Bundles/IterProd.agda
+++ /dev/null
@@ -1,38 +0,0 @@
-open import Lattice
-
-module Lattice.Bundles.IterProd {a} (A B : Set a) where
-open import Data.Nat using (ℕ)
-
-module _ (lA : Lattice A) (lB : Lattice B) where
-    open Lattice.Lattice lA using () renaming
-        ( _≈_ to _≈₁_; _⊔_ to _⊔₁_; _⊓_ to _⊓₁_
-        ; isLattice to isLattice₁
-        )
-
-    open Lattice.Lattice lB using () renaming
-        ( _≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_
-        ; isLattice to isLattice₂
-        )
-
-    module _ (k : ℕ) where
-        open import Lattice.IterProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ _⊓₁_ _⊓₂_ isLattice₁ isLattice₂ using (lattice) public
-
-module _ (fhA : FiniteHeightLattice A) (fhB : FiniteHeightLattice B) where
-    open Lattice.FiniteHeightLattice fhA using () renaming
-        ( _≈_ to _≈₁_; _⊔_ to _⊔₁_; _⊓_ to _⊓₁_
-        ; height to height₁
-        ; isLattice to isLattice₁
-        ; fixedHeight to fixedHeight₁
-        )
-
-    open Lattice.FiniteHeightLattice fhB using () renaming
-        ( _≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_
-        ; height to height₂
-        ; isLattice to isLattice₂
-        ; fixedHeight to fixedHeight₂
-        )
-
-    module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) (k : ℕ) where
-        import Lattice.IterProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ _⊓₁_ _⊓₂_ isLattice₁ isLattice₂ as IP
-
-        finiteHeightLattice = IP.finiteHeightLattice k ≈₁-dec ≈₂-dec height₁ height₂ fixedHeight₁ fixedHeight₂