diff --git a/Lattice/Prod.agda b/Lattice/Prod.agda
index 4b6d330..5218848 100644
--- a/Lattice/Prod.agda
+++ b/Lattice/Prod.agda
@@ -143,17 +143,17 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
         ∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶  _≈_
         ∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl)
 
-        amin : A
-        amin = proj₁ (proj₁ (proj₁ fhA))
+        ⊥₁ : A
+        ⊥₁ = proj₁ (proj₁ (proj₁ fhA))
 
-        amax : A
-        amax = proj₂ (proj₁ (proj₁ fhA))
+        ⊤₁ : A
+        ⊤₁ = proj₂ (proj₁ (proj₁ fhA))
 
-        bmin : B
-        bmin = proj₁ (proj₁ (proj₁ fhB))
+        ⊥₂ : B
+        ⊥₂ = proj₁ (proj₁ (proj₁ fhB))
 
-        bmax : B
-        bmax = proj₂ (proj₁ (proj₁ fhB))
+        ⊤₂ : B
+        ⊤₂ = proj₂ (proj₁ (proj₁ fhB))
 
         unzip : ∀ {a₁ a₂ : A} {b₁ b₂ : B} {n : ℕ} → Chain (a₁ , b₁) (a₂ , b₂) n → Σ (ℕ × ℕ) (λ (n₁ , n₂) → ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n ≤ n₁ + n₂)))
         unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl))
@@ -173,10 +173,10 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
 
     fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)
     fixedHeight =
-      ( ( ((amin , bmin) , (amax , bmax))
+      ( ( ((⊥₁ , ⊥₂) , (⊤₁ , ⊤₂))
         , concat
-            (ChainMapping₁.Chain-map (λ a → (a , bmin)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) (proj₂ (proj₁ fhA)))
-            (ChainMapping₂.Chain-map (λ b → (amax , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) (proj₂ (proj₁ fhB)))
+            (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) (proj₂ (proj₁ fhA)))
+            (ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) (proj₂ (proj₁ fhB)))
         )
       , λ a₁b₁a₂b₂ → let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
                      in ≤-trans n≤n₁+n₂ (+-mono-≤ (proj₂ fhA a₁a₂) (proj₂ fhB b₁b₂))