From da2b6dd5c647d95a2e05f6c6cc4791796ef0b3ee Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Mon, 16 Feb 2026 19:43:10 -0800
Subject: [PATCH] Make code less brittle for when \McL changes

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/Builder.agda | 46 +++++++++++++++++++++++++-------------------
 1 file changed, 26 insertions(+), 20 deletions(-)

diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index ed4ccf9..bea2a8a 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -615,37 +615,43 @@ record Graph : Set where
         Elem : Set
         Elem = Σ Node λ n → (proj₁ (𝓛 n))
 
+        LatticeT : Node → Set
+        LatticeT n = proj₁ (𝓛 n)
+
+        FHL : (n : Node) → FiniteHeightLattice (LatticeT n)
+        FHL n = proj₂ (𝓛 n)
+
         data _≈_ : Elem → Elem → Set where
-            ≈-lift : ∀ {n : Node} {l₁ l₂ : proj₁ (𝓛 n)} →
-                     FiniteHeightLattice._≈_ (proj₂ (𝓛 n)) l₁ l₂ →
+            ≈-lift : ∀ {n : Node} {l₁ l₂ : LatticeT n} →
+                     FiniteHeightLattice._≈_ (FHL n) l₁ l₂ →
                      (n , l₁) ≈ (n , l₂)
 
         ≈-refl : ∀ {e : Elem} → e ≈ e
-        ≈-refl {n , l} = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n)))
+        ≈-refl {n , l} = ≈-lift (FiniteHeightLattice.≈-refl (FHL n))
 
         ≈-sym : ∀ {e₁ e₂ : Elem} → e₁ ≈ e₂ → e₂ ≈ e₁
-        ≈-sym {n₁ , l₁} (≈-lift l₁≈l₂) = ≈-lift (FiniteHeightLattice.≈-sym (proj₂ (𝓛 n₁)) l₁≈l₂)
+        ≈-sym {n₁ , l₁} (≈-lift l₁≈l₂) = ≈-lift (FiniteHeightLattice.≈-sym (FHL n₁) l₁≈l₂)
 
         ≈-trans : ∀ {e₁ e₂ e₃ : Elem} → e₁ ≈ e₂ → e₂ ≈ e₃ → e₁ ≈ e₃
-        ≈-trans {n₁ , l₁} (≈-lift l₁≈l₂) (≈-lift l₂≈l₃) = ≈-lift (FiniteHeightLattice.≈-trans (proj₂ (𝓛 n₁)) l₁≈l₂ l₂≈l₃)
+        ≈-trans {n₁ , l₁} (≈-lift l₁≈l₂) (≈-lift l₂≈l₃) = ≈-lift (FiniteHeightLattice.≈-trans (FHL n₁) l₁≈l₂ l₂≈l₃)
 
         _⊔_ : Elem → Elem → Elem
         _⊔_ e₁ e₂
             using n₁ ← proj₁ e₁ using n₂ ← proj₁ e₂
             using n' ← n₁ ⊔ᵇ n₂ = (n' , select n' e₁ e₂)
             where
-                select : ∀ n' e₁ e₂ → proj₁ (𝓛 n')
+                select : ∀ n' e₁ e₂ → LatticeT n'
                 select n' (n₁ , l₁) (n₂ , l₂)
                     with n' ≟ n₁ | n' ≟ n₂
-                ...   | yes refl | yes refl = FiniteHeightLattice._⊔_ (proj₂ (𝓛 n')) l₁ l₂
+                ...   | yes refl | yes refl = FiniteHeightLattice._⊔_ (FHL n') l₁ l₂
                 ...   | yes refl | _ = l₁
                 ...   | _ | yes refl = l₂
-                ...   | no _ | no _ = FiniteHeightLattice.⊥ (proj₂ (𝓛 n'))
+                ...   | no _ | no _ = FiniteHeightLattice.⊥ (FHL n')
 
         ⊔-idemp : ∀ e → (e ⊔ e) ≈ e
         ⊔-idemp (n , l) rewrite ⊔ᵇ-idemp n
             with n ≟ n
-        ...   | yes refl = ≈-lift (FiniteHeightLattice.⊔-idemp (proj₂ (𝓛 n)) l)
+        ...   | yes refl = ≈-lift (FiniteHeightLattice.⊔-idemp (FHL n) l)
         ...   | no n≢n = ⊥-elim (n≢n refl)
 
         ⊔-comm : ∀ (e₁ e₂ : Elem) → (e₁ ⊔ e₂) ≈ (e₂ ⊔ e₁)
@@ -653,10 +659,10 @@ record Graph : Set where
             rewrite ⊔ᵇ-comm n₁ n₂
             with n ← n₂ ⊔ᵇ n₁
             with n ≟ n₁ | n ≟ n₂
-        ...   | yes refl | yes refl = ≈-lift (FiniteHeightLattice.⊔-comm (proj₂ (𝓛 n)) l₁ l₂)
-        ...   | no _ | yes refl = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n)))
-        ...   | yes refl | no _ = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n)))
-        ...   | no _ | no _ = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n)))
+        ...   | yes refl | yes refl = ≈-lift (FiniteHeightLattice.⊔-comm (FHL n) l₁ l₂)
+        ...   | no _ | yes refl = ≈-lift (FiniteHeightLattice.≈-refl (FHL n))
+        ...   | yes refl | no _ = ≈-lift (FiniteHeightLattice.≈-refl (FHL n))
+        ...   | no _ | no _ = ≈-lift (FiniteHeightLattice.≈-refl (FHL n))
 
         private
             scary : ∀ (n₁ n₂ : Node) → (p : n₁ ≡ n₂) → (n₁ ≟ n₂) ≡ subst (λ n → Dec (n₁ ≡ n)) p (yes refl)
@@ -665,10 +671,10 @@ record Graph : Set where
             ... | no n₁≢n₂ = ⊥-elim (n₁≢n₂ refl)
 
             payloadˡ : ∀ e₁ e₂ e₃ → let n = proj₁ ((e₁ ⊔ e₂) ⊔ e₃)
-                                    in proj₁ (𝓛 n)
+                                    in LatticeT n
             payloadˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
                 with n ← (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃
-                using _⊔ⁿ_ ← FiniteHeightLattice._⊔_ (proj₂ (𝓛 n))
+                using _⊔ⁿ_ ← FiniteHeightLattice._⊔_ (FHL n)
                 with n ≟ n₁ | n ≟ n₂ | n ≟ n₃
             ...   | yes refl | yes refl | yes refl = (l₁ ⊔ⁿ l₂) ⊔ⁿ l₃
             ...   | yes refl | yes refl | no _ = l₁ ⊔ⁿ l₂
@@ -677,13 +683,13 @@ record Graph : Set where
             ...   | no _ | yes refl | yes refl = l₂ ⊔ⁿ l₃
             ...   | no _ | yes refl | no _ = l₂
             ...   | no _ | no _ | yes refl = l₃
-            ...   | no _ | no _ | no _ = FiniteHeightLattice.⊥ (proj₂ (𝓛 n))
+            ...   | no _ | no _ | no _ = FiniteHeightLattice.⊥ (FHL n)
 
             payloadʳ : ∀ e₁ e₂ e₃ → let n = proj₁ (e₁ ⊔ (e₂ ⊔ e₃))
-                                    in proj₁ (𝓛 n)
+                                    in LatticeT n
             payloadʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
                 with n ← n₁ ⊔ᵇ (n₂ ⊔ᵇ n₃)
-                using _⊔ⁿ_ ← FiniteHeightLattice._⊔_ (proj₂ (𝓛 n))
+                using _⊔ⁿ_ ← FiniteHeightLattice._⊔_ (FHL n)
                 with n ≟ n₁ | n ≟ n₂ | n ≟ n₃
             ...   | yes refl | yes refl | yes refl = l₁ ⊔ⁿ (l₂ ⊔ⁿ l₃)
             ...   | yes refl | yes refl | no _ = l₁ ⊔ⁿ l₂
@@ -692,7 +698,7 @@ record Graph : Set where
             ...   | no _ | yes refl | yes refl = l₂ ⊔ⁿ l₃
             ...   | no _ | yes refl | no _ = l₂
             ...   | no _ | no _ | yes refl = l₃
-            ...   | no _ | no _ | no _ = FiniteHeightLattice.⊥ (proj₂ (𝓛 n))
+            ...   | no _ | no _ | no _ = FiniteHeightLattice.⊥ (FHL n)
 
             ⊔ᵇ-prop : ∀ n₁ n₂ n₃ → (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃ ≡ n₁ →
                                    (n₁ ⊔ᵇ n₂ ≡ n₁) × (n₁ ⊔ᵇ n₃ ≡ n₁)
@@ -865,7 +871,7 @@ record Graph : Set where
             rewrite trans (sym pˡ ) pʳ
             with nʳ ≟ n₁ | nʳ ≟ n₂ | nʳ ≟ n₃
         ...   | yes refl | yes refl | yes refl =
-            let l-assoc = FiniteHeightLattice.⊔-assoc (proj₂ (𝓛 n₁)) l₁ l₂ l₃
+            let l-assoc = FiniteHeightLattice.⊔-assoc (FHL n₁) l₁ l₂ l₃
             in ≈-trans final₁ (≈-trans (≈-lift l-assoc) (≈-sym final₂))
         ...   | yes refl | yes refl | no _ = ≈-trans final₁ (≈-sym final₂)
         ...   | yes refl | no _ | yes refl = ≈-trans final₁ (≈-sym final₂)