diff --git a/Lattice/Bundles/FiniteValueMap.agda b/Lattice/Bundles/FiniteValueMap.agda
index 5eb8d0c..e67163b 100644
--- a/Lattice/Bundles/FiniteValueMap.agda
+++ b/Lattice/Bundles/FiniteValueMap.agda
@@ -19,8 +19,10 @@ module _ (fhB : FiniteHeightLattice B) where
     module _ {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) where
         import Lattice.FiniteValueMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂ as FVM
 
-        FiniteHeightType = FVM.FiniteMap
+        FiniteHeightType = FVM.FiniteMap ks
+
+        finiteHeightLattice = FVM.IterProdIsomorphism.finiteHeightLattice uks ≈₂-dec height₂ fixedHeight₂
+        open FiniteHeightLattice finiteHeightLattice public
 
         ≈-dec = FVM.≈-dec ks ≈₂-dec
 
-        finiteHeightLattice = FVM.IterProdIsomorphism.finiteHeightLattice uks ≈₂-dec height₂ fixedHeight₂
diff --git a/Main.agda b/Main.agda
index 99ae755..205968a 100644
--- a/Main.agda
+++ b/Main.agda
@@ -22,7 +22,7 @@ xyzw-Unique = push ((λ ()) ∷ (λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ (
 open import Lattice using (IsFiniteHeightLattice; FiniteHeightLattice; Monotonic)
 open import Lattice.AboveBelow ⊤ _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵘ_  as AB using () renaming (≈-dec to ≈ᵘ-dec)
 open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵘ)
-open import Lattice.Bundles.FiniteValueMap String AB.AboveBelow _≟ˢ_ renaming (finiteHeightLattice to finiteHeightLatticeᵐ; FiniteHeightType to FiniteHeightTypeᵐ; ≈-dec to ≈-dec)
+open import Lattice.Bundles.FiniteValueMap String AB.AboveBelow _≟ˢ_ using () renaming (finiteHeightLattice to finiteHeightLatticeᵐ; FiniteHeightType to FiniteHeightTypeᵐ; ≈-dec to ≈-dec)
 
 fhlᵘ = finiteHeightLatticeᵘ (Data.Unit.tt)
 
@@ -33,7 +33,7 @@ showAboveBelow AB.⊤ = "⊤"
 showAboveBelow AB.⊥ = "⊥"
 showAboveBelow (AB.[_] tt) = "()"
 
-showMap : ∀ {ks : List String} → FiniteHeightMap ks → String
+showMap : FiniteHeightMap → String
 showMap ((kvs , _) , _) = "{" ++ foldr (λ (x , y) rest → x ++ " ↦ " ++ showAboveBelow y ++ ", " ++ rest) "" kvs ++ "}"
 
 fhlⁱᵖ = finiteHeightLatticeᵐ fhlᵘ xyzw-Unique ≈ᵘ-dec
@@ -44,16 +44,16 @@ open import Relation.Binary.Reasoning.Base.Single _≈_ (λ {m} → ≈-refl {m}
 smallestMap = proj₁ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ)))
 largestMap = proj₂ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ)))
 
-dumb : FiniteHeightMap xyzw
+dumb : FiniteHeightMap
 dumb = ((("x" , AB.[_] tt) ∷ ("y" , AB.⊥) ∷ ("z" , AB.⊥) ∷ ("w" , AB.⊥) ∷ [] , xyzw-Unique) , refl)
 
-dumbFunction : FiniteHeightMap xyzw → FiniteHeightMap xyzw
+dumbFunction : FiniteHeightMap → FiniteHeightMap
 dumbFunction = _⊔_ dumb
 
 dumbFunction-Monotonic : Monotonic _≼_ _≼_ dumbFunction
 dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂ = ⊔-Monotonicˡ dumb {m₁} {m₂} m₁≼m₂
 
 
-open import Fixedpoint {0ℓ} {FiniteHeightMap xyzw} {8} {_≈_} {_⊔_} {_⊓_} (≈-dec fhlᵘ xyzw-Unique ≈ᵘ-dec) (FiniteHeightLattice.isFiniteHeightLattice fhlⁱᵖ) dumbFunction (λ {m₁} {m₂} m₁≼m₂ → dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂)
+open import Fixedpoint {0ℓ} {FiniteHeightMap} {8} {_≈_} {_⊔_} {_⊓_} (≈-dec fhlᵘ xyzw-Unique ≈ᵘ-dec) (FiniteHeightLattice.isFiniteHeightLattice fhlⁱᵖ) dumbFunction (λ {m₁} {m₂} m₁≼m₂ → dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂)
 
 main = run {0ℓ} (putStrLn (showMap aᶠ))