------------------------------------------------------------------------
-- The Agda standard library
--
-- Instances of algebraic structures made by taking two other instances
-- A and B, and having elements of the new instance be pairs |A| × |B|.
-- In mathematics, this would usually be written A × B or A ⊕ B.
--
-- From semigroups up, these new instances are products of the relevant
-- category. For structures with commutative addition (commutative
-- monoids, Abelian groups, semirings, rings), the direct product is
-- also the coproduct, making it a biproduct.
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Algebra.Lattice.Construct.DirectProduct where

open import Algebra using (Band)
open import Algebra.Lattice using (Semilattice)
import Algebra.Construct.DirectProduct as DirectProduct
open import Data.Product.Base using (_,_; _<*>_)
open import Level using (Level; _⊔_)

private
  variable
    a b ℓ₁ ℓ₂ : Level

------------------------------------------------------------------------
-- Bundles

semilattice : Semilattice a ℓ₁ → Semilattice b ℓ₂ →
              Semilattice (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
semilattice L M = record
  { isSemilattice = record
    { isBand = Band.isBand (DirectProduct.band L.band M.band)
    ; comm   = λ x y → (L.comm , M.comm) <*> x <*> y
    }
  } where module L = Semilattice L; module M = Semilattice M