Expose bundles from Unit

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Lattice/AboveBelow.agda

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

Lattice/FiniteMap.agda

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

Lattice/Map.agda

@@ -882,6 +882,14 @@ 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
+    ; isUnionSemilattice; isIntersectSemilattice; isLattice; lattice
     ) 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
 
-NatIsMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
-NatIsMaxSemilattice = record
+isMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
+isMaxSemilattice = record
     { ≈-equiv = record
         { ≈-refl = refl
         ; ≈-sym = sym
@@ -31,8 +31,8 @@ NatIsMaxSemilattice = record
     ; ⊔-idemp = ⊔-idem
     }
 
-NatIsMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
-NatIsMinSemilattice = record
+isMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
+isMinSemilattice = record
     { ≈-equiv = record
         { ≈-refl = refl
         ; ≈-sym = sym
@@ -74,10 +74,18 @@ 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
 
-NatIsLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
-NatIsLattice = record
-    { joinSemilattice = NatIsMaxSemilattice
-    ; meetSemilattice = NatIsMinSemilattice
+isLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
+isLattice = record
+    { joinSemilattice = isMaxSemilattice
+    ; meetSemilattice = isMinSemilattice
     ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
     ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
     }
+
+lattice : Lattice ℕ
+lattice = record
+    { _≈_ = _≡_
+    ; _⊔_ = _⊔_
+    ; _⊓_ = _⊓_
+    ; isLattice = isLattice
+    }

Lattice/Prod.agda

@@ -94,6 +94,13 @@ isLattice = record
         )
     }
 
+lattice : Lattice (A × B)
+lattice = record
+    { _≈_ = _≈_
+    ; _⊔_ = _⊔_
+    ; _⊓_ = _⊓_
+    ; isLattice = isLattice
+    }
 
 module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) where
     ≈-dec : IsDecidable _≈_
@@ -176,3 +183,12 @@ 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,6 +89,14 @@ isLattice = record
     ; absorb-⊓-⊔ = absorb-⊓-⊔
     }
 
+lattice : Lattice ⊤
+lattice = record
+    { _≈_ = _≈_
+    ; _⊔_ = _⊔_
+    ; _⊓_ = _⊓_
+    ; isLattice = isLattice
+    }
+
 open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice)
 
 private
@@ -104,3 +112,12 @@ isFiniteHeightLattice = record
     { isLattice = isLattice
     ; fixedHeight = (((tt , tt) , longestChain) , isLongest)
     }
+
+finiteHeightLattice : FiniteHeightLattice ⊤
+finiteHeightLattice = record
+    { height = 0
+    ; _≈_ = _≈_
+    ; _⊔_ = _⊔_
+    ; _⊓_ = _⊓_
+    ; isFiniteHeightLattice = isFiniteHeightLattice
+    }