open import Lattice

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 Data.Nat using (ℕ; suc)
open import Data.Product using (_×_)
open import Utils using (iterate)

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.

private module _ where
    ALattice : Lattice A
    ALattice = record
        { _≈_ = _≈₁_
        ; _⊔_ = _⊔₁_
        ; _⊓_ = _⊓₁_
        ; isLattice = lA
        }

    BLattice : Lattice B
    BLattice = record
        { _≈_ = _≈₂_
        ; _⊔_ = _⊔₂_
        ; _⊓_ = _⊓₂_
        ; isLattice = lB
        }

    IterProdLattice : ∀ {k : ℕ} → Lattice (IterProd k)
    IterProdLattice {0} = BLattice
    IterProdLattice {suc k'} = record
        { _≈_ = _≈_
        ; _⊔_ = _⊔_
        ; _⊓_ = _⊓_
        ; isLattice = isLattice
        }
        where
            RightLattice : Lattice (IterProd k')
            RightLattice = IterProdLattice {k'}

            open import Lattice.Prod
                _≈₁_ (Lattice._≈_ RightLattice)
                _⊔₁_ (Lattice._⊔_ RightLattice)
                _⊓₁_ (Lattice._⊓_ RightLattice)
                lA  (Lattice.isLattice RightLattice)

-- Expose the computed definition in public.
module _ (k : ℕ) where
    open Lattice.Lattice (IterProdLattice {k}) public