diff --git a/Isomorphism.agda b/Isomorphism.agda
index 59e37ff..454bf93 100644
--- a/Isomorphism.agda
+++ b/Isomorphism.agda
@@ -60,3 +60,12 @@ module TransportFiniteHeight
             { isLattice = lB
             ; fixedHeight = (((f a₁ , f a₂), portChain₁ c) , λ c' → bounded₁ (portChain₂ c'))
             }
+
+    finiteHeightLattice : FiniteHeightLattice B
+    finiteHeightLattice = record
+        { height = height
+        ; _≈_ = _≈₂_
+        ; _⊔_ = _⊔₂_
+        ; _⊓_ = _⊓₂_
+        ; isFiniteHeightLattice = isFiniteHeightLattice
+        }
diff --git a/Lattice/FiniteValueMap.agda b/Lattice/FiniteValueMap.agda
index d5eb4d1..a62184e 100644
--- a/Lattice/FiniteValueMap.agda
+++ b/Lattice/FiniteValueMap.agda
@@ -271,4 +271,4 @@ module IterProdIsomorphism where
             (to-preserves-≈ uks) (from-preserves-≈ {ks})
             (to-⊔-distr uks) (from-⊔-distr {ks})
             (from-to-inverseʳ uks) (from-to-inverseˡ uks)
-            using (isFiniteHeightLattice) public
+            using (isFiniteHeightLattice; finiteHeightLattice) public