Prove that iterated products are finite height

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

Lattice/IterProd.agda

@@ -6,10 +6,14 @@ module Lattice.IterProd {a} {A B : Set a}
     (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B)
     (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
-open import Data.Nat using (ℕ; suc)
+open import Agda.Primitive using (lsuc)
+open import Data.Nat using (ℕ; suc; _+_)
 open import Data.Product using (_×_)
 open import Utils using (iterate)
 
+open IsLattice lA renaming (FixedHeight to FixedHeight₁)
+open IsLattice lB renaming (FixedHeight to FixedHeight₂)
+
 IterProd : ℕ → Set a
 IterProd k = iterate k (λ t → A × t) B
 
@@ -17,14 +21,6 @@ IterProd k = iterate k (λ t → A × t) B
 -- records, perform the recursion, and unpackage.
 
 private module _ where
-    ALattice : Lattice A
-    ALattice = record
-        { _≈_ = _≈₁_
-        ; _⊔_ = _⊔₁_
-        ; _⊓_ = _⊓₁_
-        ; isLattice = lA
-        }
-
     BLattice : Lattice B
     BLattice = record
         { _≈_ = _≈₂_
@@ -42,14 +38,69 @@ private module _ where
         ; isLattice = isLattice
         }
         where
-            RightLattice : Lattice (IterProd k')
-            RightLattice = IterProdLattice {k'}
+            Right : Lattice (IterProd k')
+            Right = IterProdLattice {k'}
 
             open import Lattice.Prod
-                _≈₁_ (Lattice._≈_ RightLattice)
-                _⊔₁_ (Lattice._⊔_ RightLattice)
-                _⊓₁_ (Lattice._⊓_ RightLattice)
-                lA  (Lattice.isLattice RightLattice)
+                _≈₁_ (Lattice._≈_ Right)
+                _⊔₁_ (Lattice._⊔_ Right)
+                _⊓₁_ (Lattice._⊓_ Right)
+                lA  (Lattice.isLattice Right)
+
+module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
+         (h₁ h₂ : ℕ)
+         (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
+
+    private module _ where
+        record FiniteHeightAndDecEq (A : Set a) : Set (lsuc a) where
+            field
+                height : ℕ
+                _≈_ : A → A → Set a
+                _⊔_ : A → A → A
+                _⊓_ : A → A → A
+
+                isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
+                ≈-dec : IsDecidable _≈_
+
+            open IsFiniteHeightLattice isFiniteHeightLattice public
+
+        BFiniteHeightLattice : FiniteHeightAndDecEq B
+        BFiniteHeightLattice = record
+            { height = h₂
+            ; _≈_ = _≈₂_
+            ; _⊔_ = _⊔₂_
+            ; _⊓_ = _⊓₂_
+            ; isFiniteHeightLattice = record
+                { isLattice = lB
+                ; fixedHeight = fhB
+                }
+            ; ≈-dec = ≈₂-dec
+            }
+
+        IterProdFiniteHeightLattice : ∀ {k : ℕ} → FiniteHeightAndDecEq (IterProd k)
+        IterProdFiniteHeightLattice {0} = BFiniteHeightLattice
+        IterProdFiniteHeightLattice {suc k'} = record
+            { height = h₁ + FiniteHeightAndDecEq.height Right
+            ; _≈_ = _≈_
+            ; _⊔_ = _⊔_
+            ; _⊓_ = _⊓_
+            ; isFiniteHeightLattice = isFiniteHeightLattice
+                ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
+                h₁ (FiniteHeightAndDecEq.height Right)
+                fhA (IsFiniteHeightLattice.fixedHeight (FiniteHeightAndDecEq.isFiniteHeightLattice Right))
+            ; ≈-dec = ≈-dec ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
+            }
+            where
+                Right = IterProdFiniteHeightLattice {k'}
+
+                open import Lattice.Prod
+                    _≈₁_ (FiniteHeightAndDecEq._≈_ Right)
+                    _⊔₁_ (FiniteHeightAndDecEq._⊔_ Right)
+                    _⊓₁_ (FiniteHeightAndDecEq._⊓_ Right)
+                    lA  (FiniteHeightAndDecEq.isLattice Right)
+
+    module _ (k : ℕ) where
+        open FiniteHeightAndDecEq (IterProdFiniteHeightLattice {k}) using (fixedHeight) public
 
 -- Expose the computed definition in public.
 module _ (k : ℕ) where