Lattice/AboveBelow.agda

@@ -279,14 +279,6 @@ module Plain where
         ; absorb-⊓-⊔ = absorb-⊓-⊔
         }
 
-    lattice : Lattice AboveBelow
-    lattice = record
-        { _≈_ = _≈_
-        ; _⊔_ = _⊔_
-        ; _⊓_ = _⊓_
-        ; isLattice = isLattice
-        }
-
     open IsLattice isLattice using (_≼_; _≺_)
 
     ⊥≺[x] : ∀ (x : A) → ⊥ ≺ [ x ]
@@ -337,12 +329,3 @@ module Plain where
             { isLattice = isLattice
             ; fixedHeight = (((⊥ , ⊤) , longestChain) , isLongest)
             }
-
-        finiteHeightLattice : FiniteHeightLattice AboveBelow
-        finiteHeightLattice = record
-            { height = 2
-            ; _≈_ = _≈_
-            ; _⊔_ = _⊔_
-            ; _⊓_ = _⊓_
-            ; isFiniteHeightLattice = isFiniteHeightLattice
-            }

Lattice/FiniteMap.agda

@@ -76,11 +76,3 @@ module _ (ks : List A) where
         ; absorb-⊔-⊓ = λ (m₁ , _) (m₂ , _) → absorb-⊔ᵐ-⊓ᵐ m₁ m₂
         ; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂
         }
-
-    lattice : Lattice FiniteMap
-    lattice = record
-        { _≈_ = _≈_
-        ; _⊔_ = _⊔_
-        ; _⊓_ = _⊓_
-        ; isLattice = isLattice
-        }

Lattice/IterProd.agda

@@ -21,14 +21,17 @@ IterProd k = iterate k (λ t → A × t) B
 -- records, perform the recursion, and unpackage.
 
 private module _ where
-    lattice : ∀ {k : ℕ} → Lattice (IterProd k)
+    BLattice : Lattice B
-    lattice {0} = record
+    BLattice = record
         { _≈_ = _≈₂_
         ; _⊔_ = _⊔₂_
         ; _⊓_ = _⊓₂_
         ; isLattice = lB
         }
-    lattice {suc k'} = record
+
+    IterProdLattice : ∀ {k : ℕ} → Lattice (IterProd k)
+    IterProdLattice {0} = BLattice
+    IterProdLattice {suc k'} = record
         { _≈_ = _≈_
         ; _⊔_ = _⊔_
         ; _⊓_ = _⊓_
@@ -36,7 +39,7 @@ private module _ where
         }
         where
             Right : Lattice (IterProd k')
-            Right = lattice {k'}
+            Right = IterProdLattice {k'}
 
             open import Lattice.Prod
                 _≈₁_ (Lattice._≈_ Right)
@@ -44,9 +47,6 @@ private module _ where
                 _⊓₁_ (Lattice._⊓_ Right)
                 lA  (Lattice.isLattice Right)
 
-module _ (k : ℕ) where
-    open Lattice.Lattice (lattice {k}) public
-
 module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
          (h₁ h₂ : ℕ)
          (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
@@ -64,8 +64,8 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
 
             open IsFiniteHeightLattice isFiniteHeightLattice public
 
-        finiteHeightAndDec : ∀ {k : ℕ} → FiniteHeightAndDecEq (IterProd k)
+        BFiniteHeightLattice : FiniteHeightAndDecEq B
-        finiteHeightAndDec {0} = record
+        BFiniteHeightLattice = record
             { height = h₂
             ; _≈_ = _≈₂_
             ; _⊔_ = _⊔₂_
@@ -76,11 +76,14 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
                 }
             ; ≈-dec = ≈₂-dec
             }
-        finiteHeightAndDec {suc k'} = record
+
+        IterProdFiniteHeightLattice : ∀ {k : ℕ} → FiniteHeightAndDecEq (IterProd k)
+        IterProdFiniteHeightLattice {0} = BFiniteHeightLattice
+        IterProdFiniteHeightLattice {suc k'} = record
             { height = h₁ + FiniteHeightAndDecEq.height Right
-            ; _≈_ = P._≈_
+            ; _≈_ = _≈_
-            ; _⊔_ = P._⊔_
+            ; _⊔_ = _⊔_
-            ; _⊓_ = P._⊓_
+            ; _⊓_ = _⊓_
             ; isFiniteHeightLattice = isFiniteHeightLattice
                 ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
                 h₁ (FiniteHeightAndDecEq.height Right)
@@ -88,25 +91,17 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
             ; ≈-dec = ≈-dec ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
             }
             where
-                Right = finiteHeightAndDec {k'}
+                Right = IterProdFiniteHeightLattice {k'}
 
                 open import Lattice.Prod
                     _≈₁_ (FiniteHeightAndDecEq._≈_ Right)
                     _⊔₁_ (FiniteHeightAndDecEq._⊔_ Right)
                     _⊓₁_ (FiniteHeightAndDecEq._⊓_ Right)
-                    lA  (FiniteHeightAndDecEq.isLattice Right) as P
+                    lA  (FiniteHeightAndDecEq.isLattice Right)
 
     module _ (k : ℕ) where
-        open FiniteHeightAndDecEq (finiteHeightAndDec {k}) using (isFiniteHeightLattice) public
+        open FiniteHeightAndDecEq (IterProdFiniteHeightLattice {k}) using (fixedHeight) public
 
-        private
+-- Expose the computed definition in public.
-            FHD = finiteHeightAndDec {k}
+module _ (k : ℕ) where
-
+    open Lattice.Lattice (IterProdLattice {k}) public
-        finiteHeightLattice : FiniteHeightLattice (IterProd k)
-        finiteHeightLattice = record
-            { height = FiniteHeightAndDecEq.height FHD
-            ; _≈_ = FiniteHeightAndDecEq._≈_ FHD
-            ; _⊔_ = FiniteHeightAndDecEq._⊔_ FHD
-            ; _⊓_ = FiniteHeightAndDecEq._⊓_ FHD
-            ; isFiniteHeightLattice = isFiniteHeightLattice
-            }

Lattice/Map.agda

@@ -882,14 +882,6 @@ isLattice = record
     ; absorb-⊓-⊔ = absorb-⊓-⊔
     }
 
-lattice : Lattice Map
-lattice = record
-    { _≈_ = _≈_
-    ; _⊔_ = _⊔_
-    ; _⊓_ = _⊓_
-    ; isLattice = isLattice
-    }
-
 ⊔-equal-keys : ∀ {m₁ m₂ : Map} → keys m₁ ≡ keys m₂ → keys m₁ ≡ keys (m₁ ⊔ m₂)
 ⊔-equal-keys km₁≡km₂ = union-equal-keys km₁≡km₂
 

Lattice/MapSet.agda

@@ -12,7 +12,7 @@ private module UnitMap = Lattice.Map A ⊤ _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A
 open UnitMap using (Map)
 open UnitMap using
     ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_
-    ; isUnionSemilattice; isIntersectSemilattice; isLattice; lattice
+    ; isUnionSemilattice; isIntersectSemilattice; isLattice
     ) public
 
 MapSet : Set a

Lattice/Nat.agda

@@ -18,8 +18,8 @@ private
     ≡-⊓-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊓ a₃) ≡ (a₂ ⊓ a₄)
     ≡-⊓-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl
 
-isMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
+NatIsMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
-isMaxSemilattice = record
+NatIsMaxSemilattice = record
     { ≈-equiv = record
         { ≈-refl = refl
         ; ≈-sym = sym
@@ -31,8 +31,8 @@ isMaxSemilattice = record
     ; ⊔-idemp = ⊔-idem
     }
 
-isMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
+NatIsMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
-isMinSemilattice = record
+NatIsMinSemilattice = record
     { ≈-equiv = record
         { ≈-refl = refl
         ; ≈-sym = sym
@@ -74,18 +74,10 @@ private
             helper : x ⊔ (x ⊓ y) ≤ x ⊔ x  → x ⊔ x ≡ x → x ⊔ (x ⊓ y) ≤ x
             helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x
 
-isLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
+NatIsLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
-isLattice = record
+NatIsLattice = record
-    { joinSemilattice = isMaxSemilattice
+    { joinSemilattice = NatIsMaxSemilattice
-    ; meetSemilattice = isMinSemilattice
+    ; meetSemilattice = NatIsMinSemilattice
     ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
     ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
     }
-
-lattice : Lattice ℕ
-lattice = record
-    { _≈_ = _≡_
-    ; _⊔_ = _⊔_
-    ; _⊓_ = _⊓_
-    ; isLattice = isLattice
-    }

Lattice/Prod.agda

@@ -94,13 +94,6 @@ isLattice = record
         )
     }
 
-lattice : Lattice (A × B)
-lattice = record
-    { _≈_ = _≈_
-    ; _⊔_ = _⊔_
-    ; _⊓_ = _⊓_
-    ; isLattice = isLattice
-    }
 
 module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) where
     ≈-dec : IsDecidable _≈_
@@ -183,12 +176,3 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
                            in ≤-trans n≤n₁+n₂ (+-mono-≤ (proj₂ fhA a₁a₂) (proj₂ fhB b₁b₂))
             )
         }
-
-    finiteHeightLattice : FiniteHeightLattice (A × B)
-    finiteHeightLattice = record
-        { height = h₁ + h₂
-        ; _≈_ = _≈_
-        ; _⊔_ = _⊔_
-        ; _⊓_ = _⊓_
-        ; isFiniteHeightLattice = isFiniteHeightLattice
-        }

Lattice/Unit.agda

@@ -89,14 +89,6 @@ isLattice = record
     ; absorb-⊓-⊔ = absorb-⊓-⊔
     }
 
-lattice : Lattice ⊤
-lattice = record
-    { _≈_ = _≈_
-    ; _⊔_ = _⊔_
-    ; _⊓_ = _⊓_
-    ; isLattice = isLattice
-    }
-
 open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice)
 
 private
@@ -112,12 +104,3 @@ isFiniteHeightLattice = record
     { isLattice = isLattice
     ; fixedHeight = (((tt , tt) , longestChain) , isLongest)
     }
-
-finiteHeightLattice : FiniteHeightLattice ⊤
-finiteHeightLattice = record
-    { height = 0
-    ; _≈_ = _≈_
-    ; _⊔_ = _⊔_
-    ; _⊓_ = _⊓_
-    ; isFiniteHeightLattice = isFiniteHeightLattice
-    }