From a920608bef038b8c990d08b2e0aaae43e469d49f Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 11 Feb 2024 20:45:14 -0800
Subject: [PATCH] Tweak IterProd to expose more (including a bundle)

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/IterProd.agda | 27 +++++++++++++++++++--------
 1 file changed, 19 insertions(+), 8 deletions(-)

diff --git a/Lattice/IterProd.agda b/Lattice/IterProd.agda
index fed3c43..e5d0856 100644
--- a/Lattice/IterProd.agda
+++ b/Lattice/IterProd.agda
@@ -47,6 +47,9 @@ private module _ where
                 _⊓₁_ (Lattice._⊓_ Right)
                 lA  (Lattice.isLattice Right)
 
+module _ (k : ℕ) where
+    open Lattice.Lattice (IterProdLattice {k}) public
+
 module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
          (h₁ h₂ : ℕ)
          (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
@@ -81,9 +84,9 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
         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)
@@ -97,11 +100,19 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
                     _≈₁_ (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 (IterProdFiniteHeightLattice {k}) using (isFiniteHeightLattice) public
 
--- Expose the computed definition in public.
-module _ (k : ℕ) where
-    open Lattice.Lattice (IterProdLattice {k}) public
+        private
+            FHD = IterProdFiniteHeightLattice {k}
+
+        finiteHeightLattice : FiniteHeightLattice (IterProd k)
+        finiteHeightLattice = record
+            { height = FiniteHeightAndDecEq.height FHD
+            ; _≈_ = FiniteHeightAndDecEq._≈_ FHD
+            ; _⊔_ = FiniteHeightAndDecEq._⊔_ FHD
+            ; _⊓_ = FiniteHeightAndDecEq._⊓_ FHD
+            ; isFiniteHeightLattice = isFiniteHeightLattice
+            }