diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index 7457f6f..3fa484e 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -2,7 +2,7 @@ module Lattice.Builder where
 
 open import Lattice
 open import Equivalence
-open import Utils using (Unique; push; empty; Unique-append; Unique-++⁻ˡ; Unique-++⁻ʳ; Unique-narrow; All¬-¬Any; ¬Any-map; fins; fins-complete; findUniversal; Decidable-¬)
+open import Utils using (Unique; push; empty; Unique-append; Unique-++⁻ˡ; Unique-++⁻ʳ; Unique-narrow; All¬-¬Any; ¬Any-map; fins; fins-complete; findUniversal; Decidable-¬; ∈-cartesianProduct)
 open import Data.Nat as Nat using (ℕ)
 open import Data.Fin as Fin using (Fin; suc; zero; _≟_)
 open import Data.Maybe as Maybe using (Maybe; just; nothing; _>>=_; maybe)
@@ -13,7 +13,7 @@ open import Data.List.Membership.Propositional as MemProp using (lose) renaming
 open import Data.List.Membership.Propositional.Properties using () renaming (∈-++⁺ʳ to ∈ˡ-++⁺ʳ; ∈-++⁺ˡ to ∈ˡ-++⁺ˡ; ∈-cartesianProductWith⁺ to ∈ˡ-cartesianProductWith⁺; ∈-filter⁻ to ∈ˡ-filter⁻; ∈-filter⁺ to ∈ˡ-filter⁺; ∈-lookup to ∈ˡ-lookup)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there; any?; satisfied; index)
 open import Data.List.Relation.Unary.Any.Properties using (¬Any[]; lookup-result)
-open import Data.List.Relation.Unary.All using (All; []; _∷_; map; lookup; zipWith; tabulate; all?)
+open import Data.List.Relation.Unary.All using (All; []; _∷_; map; lookup; zipWith; tabulate; universal; all?)
 open import Data.List.Relation.Unary.All.Properties using () renaming (++⁺ to ++ˡ⁺; ++⁻ʳ to ++ˡ⁻ʳ)
 open import Data.List using (List; _∷_; []; cartesianProduct; cartesianProductWith; foldr; filter) renaming (_++_ to _++ˡ_)
 open import Data.List.Properties using () renaming (++-conicalʳ to ++ˡ-conicalʳ; ++-identityʳ to ++ˡ-identityʳ; ++-assoc to ++ˡ-assoc)
@@ -410,6 +410,17 @@ record Graph : Set where
                                nlast = tabulate {xs = (preds n₁ n₂)} (λ {n'} n'∈preds →  nlast' n' (proj₂ (∈ˡ-filter⁻ (Pred? n₁ n₂) {xs = proj₁ nodes} n'∈preds)))
                            in nopred (lose n∈preds nlast)
 
+    Total-⊔ : Set
+    Total-⊔ = ∀ n₁ n₂ → Have-⊔ n₁ n₂
+
+    Total-⊔? : Dec Total-⊔
+    Total-⊔?
+        with all? (λ (n₁ , n₂) → Have-⊔? n₁ n₂) (cartesianProduct (proj₁ nodes) (proj₁ nodes))
+    ...   | yes all⊔ = yes λ n₁ n₂ →
+            let n₁n₂∈prod = ∈-cartesianProduct (nodes-complete n₁) (nodes-complete n₂)
+            in lookup all⊔ n₁n₂∈prod
+    ...   | no ¬all⊔ = no λ all⊔ → ¬all⊔ (universal (λ (n₁ , n₂) → all⊔ n₁ n₂) _)
+
     module AssumeNoCycles (noCycles : NoCycles) where
         -- TODO: technically, the decidability of existing paths is separate
         --       from cycles. Because, for every non-simple path, we can construct