open import Lattice

-- Due to universe levels, it becomes relatively annoying to handle the case
-- where the levels of A and B are not the same. For the time being, constrain
-- them to be the same.

module Lattice.IterProd {a} {A B : Set a}
    (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
    (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
    (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B)
    (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where

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

-- To make iteration more convenient, package the definitions in Lattice
-- records, perform the recursion, and unpackage.

module _ where
    lattice : ∀ {k : ℕ} → Lattice (IterProd k)
    lattice {0} = record
        { _≈_ = _≈₂_
        ; _⊔_ = _⊔₂_
        ; _⊓_ = _⊓₂_
        ; isLattice = lB
        }
    lattice {suc k'} = record
        { _≈_ = _≈_
        ; _⊔_ = _⊔_
        ; _⊓_ = _⊓_
        ; isLattice = isLattice
        }
        where
            Right : Lattice (IterProd k')
            Right = lattice {k'}

            open import Lattice.Prod
                _≈₁_ (Lattice._≈_ Right)
                _⊔₁_ (Lattice._⊔_ Right)
                _⊓₁_ (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

    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

        finiteHeightAndDec : ∀ {k : ℕ} → FiniteHeightAndDecEq (IterProd k)
        finiteHeightAndDec {0} = record
            { height = h₂
            ; _≈_ = _≈₂_
            ; _⊔_ = _⊔₂_
            ; _⊓_ = _⊓₂_
            ; isFiniteHeightLattice = record
                { isLattice = lB
                ; fixedHeight = fhB
                }
            ; ≈-dec = ≈₂-dec
            }
        finiteHeightAndDec {suc k'} = record
            { height = h₁ + FiniteHeightAndDecEq.height Right
            ; _≈_ = P._≈_
            ; _⊔_ = P._⊔_
            ; _⊓_ = P._⊓_
            ; isFiniteHeightLattice = isFiniteHeightLattice
                ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
                h₁ (FiniteHeightAndDecEq.height Right)
                fhA (IsFiniteHeightLattice.fixedHeight (FiniteHeightAndDecEq.isFiniteHeightLattice Right))
            ; ≈-dec = ≈-dec ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
            }
            where
                Right = finiteHeightAndDec {k'}

                open import Lattice.Prod
                    _≈₁_ (FiniteHeightAndDecEq._≈_ Right)
                    _⊔₁_ (FiniteHeightAndDecEq._⊔_ Right)
                    _⊓₁_ (FiniteHeightAndDecEq._⊓_ Right)
                    lA  (FiniteHeightAndDecEq.isLattice Right) as P

    module _ (k : ℕ) where
        open FiniteHeightAndDecEq (finiteHeightAndDec {k}) using (isFiniteHeightLattice) public

        private
            FHD = finiteHeightAndDec {k}

        finiteHeightLattice : FiniteHeightLattice (IterProd k)
        finiteHeightLattice = record
            { height = FiniteHeightAndDecEq.height FHD
            ; _≈_ = FiniteHeightAndDecEq._≈_ FHD
            ; _⊔_ = FiniteHeightAndDecEq._⊔_ FHD
            ; _⊓_ = FiniteHeightAndDecEq._⊓_ FHD
            ; isFiniteHeightLattice = isFiniteHeightLattice
            }