diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index 3fa484e..330a53a 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -384,42 +384,75 @@ record Graph : Set where
     Pred : Node → Node → Node → Set
     Pred n₁ n₂ n = PathExists n n₁ × PathExists n n₂
 
+    Succ : Node → Node → Node → Set
+    Succ n₁ n₂ n = PathExists n₁ n × PathExists n₂ n
+
     Pred? : ∀ (n₁ n₂ : Node) → Decidable (Pred n₁ n₂)
     Pred? n₁ n₂ n = PathExists? n n₁ ×-dec PathExists? n n₂
 
+    Suc? : ∀ (n₁ n₂ : Node) → Decidable (Succ n₁ n₂)
+    Suc? n₁ n₂ n = PathExists? n₁ n ×-dec PathExists? n₂ n
+
     preds : Node → Node → List Node
     preds n₁ n₂ = filter (Pred? n₁ n₂) (proj₁ nodes)
 
+    sucs : Node → Node → List Node
+    sucs n₁ n₂ = filter (Suc? n₁ n₂) (proj₁ nodes)
+
     Have-⊔ : Node → Node → Set
     Have-⊔ n₁ n₂ = Σ Node (λ n →  Pred n₁ n₂ n × (∀ n' →  Pred n₁ n₂ n' → PathExists n' n))
 
+    Have-⊓ : Node → Node → Set
+    Have-⊓ n₁ n₂ = Σ Node (λ n →  Succ n₁ n₂ n × (∀ n' →  Succ n₁ n₂ n' → PathExists n n'))
+
+    -- when filtering nodes by a predicate P, then trying to find a universal
+    -- element according to another predicate Q, the universality can be
+    -- extended from "element of the filtered list for to which all other elements relate" to
+    -- "node satisfying P to which all other nodes satisfying P relate".
+    filter-nodes-universal : ∀ {P : Node → Set} (P? : Decidable P) -- e.g. Pred n₁ n₂
+                               {Q : Node → Node → Set} (Q? : Decidable² Q) -- e.g. PathExists? n' n
+                               → Dec (Σ Node λ n → P n × (∀ n' → P n' → Q n n'))
+    filter-nodes-universal {P = P} P? {Q = Q} Q?
+        with findUniversal (filter P? (proj₁ nodes)) Q?
+    ...   | yes founduni =
+            let idx = index founduni
+                n = Any.lookup founduni
+                n∈filter = ∈ˡ-lookup idx
+                (_ , Pn) = ∈ˡ-filter⁻ P? {xs = proj₁ nodes} n∈filter
+                nuni = lookup-result founduni
+            in yes (n , (Pn , λ n' Pn' →
+                                    let n'∈filter = ∈ˡ-filter⁺ P? (nodes-complete n') Pn'
+                                    in lookup nuni n'∈filter))
+    ...   | no nouni = no λ (n , (Pn , nuni')) →
+                           let n∈filter = ∈ˡ-filter⁺ P? (nodes-complete n) Pn
+                               nuni = tabulate {xs = filter P? (proj₁ nodes)} (λ {n'} n'∈filter →  nuni' n' (proj₂ (∈ˡ-filter⁻ P? {xs = proj₁ nodes} n'∈filter)))
+                           in nouni (lose n∈filter nuni)
+
     Have-⊔? : Decidable² Have-⊔
-    Have-⊔? n₁ n₂
-        with findUniversal (preds n₁ n₂) (λ n n' → PathExists? n' n) 
-    ...   | yes foundpred =
-            let idx = index foundpred
-                n = Any.lookup foundpred
-                n∈preds = ∈ˡ-lookup idx
-                (_ , n→n₁n₂) = ∈ˡ-filter⁻ (Pred? n₁ n₂) {xs = proj₁ nodes} n∈preds
-                nlast = lookup-result foundpred
-            in yes (n , (n→n₁n₂ , λ n' n'→n₁n₂ →
-                                    let n'∈preds = ∈ˡ-filter⁺ (Pred? n₁ n₂) (nodes-complete n') n'→n₁n₂
-                                    in lookup nlast n'∈preds))
-    ...   | no nopred = no λ (n , (n→n₁n₂ , nlast')) →
-                           let n∈preds = ∈ˡ-filter⁺ (Pred? n₁ n₂) (nodes-complete n) n→n₁n₂
-                               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)
+    Have-⊔? n₁ n₂ = filter-nodes-universal (Pred? n₁ n₂) (λ n₁ n₂ → PathExists? n₂ n₁)
+
+    Have-⊓? : Decidable² Have-⊓
+    Have-⊓? n₁ n₂ = filter-nodes-universal (Suc? n₁ n₂) PathExists?
 
     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₂ →
+    Total-⊓ : Set
+    Total-⊓ = ∀ n₁ n₂ → Have-⊓ n₁ n₂
+
+    P-Total? : ∀ {P : Node → Node → Set} (P? : Decidable² P) → Dec (∀ n₁ n₂ → P n₁ n₂)
+    P-Total? {P} P?
+        with all? (λ (n₁ , n₂) → P? n₁ n₂) (cartesianProduct (proj₁ nodes) (proj₁ nodes))
+    ...   | yes allP = 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₂) _)
+            in lookup allP n₁n₂∈prod
+    ...   | no ¬allP = no λ allP → ¬allP (universal (λ (n₁ , n₂) → allP n₁ n₂) _)
+
+    Total-⊔? : Dec Total-⊔
+    Total-⊔? = P-Total? Have-⊔?
+
+    Total-⊓? : Dec Total-⊓
+    Total-⊓? = P-Total? Have-⊓?
 
     module AssumeNoCycles (noCycles : NoCycles) where
         -- TODO: technically, the decidability of existing paths is separate