Skip to content

Lattices.Product

Finite products of lattices

This is the Lattices.Product module of the agda-lattices library.

This module constructs the product of lattices and records the properties of products that the library uses, as follows.

  • The binary direct product 𝑳₁ Γ—Λ‘ 𝑳₂ of lattices 𝑳₁ and 𝑳₂ over Sig-Lattice: the lattice on the product setoid whose meet and join act componentwise (LatticeProduct). The construction mirrors the group case of agda-algebras (Classical.Structures.Group.Product) but is assembled through the setoid-level builder setoidEqsToLattice of Classical.Structures.Lattice.Basic, whose interpretation clauses reduce definitionally; consequently each of the eight lattice equations for the product is literally the pair of the component equations, and no term-induction lemma is needed. The induced meet order of Classical.Properties.Lattice is the componentwise order, definitionally, and the three accessors ≀ₓ-fst, ≀ₓ-snd and ≀ₓ-pair name the two projections and the pairing.
  • The one-element lattice 𝟏ˑ, the empty product.
  • The binary product is finite when its factors are (Γ—Λ‘-finite: the enumeration is the standard library's bijection between Fin (m * n) and Fin m Γ— Fin n), semidistributive when its factors are (Γ—Λ‘-semidistributive: the laws are universal Horn sentences, read componentwise), and its two projections are homomorphisms (fst-hom, snd-hom).
  • The product Ξ  m 𝓛 of a family of lattices indexed by Fin m, as nested binary products, with the same three properties, the projections proj as homomorphisms, tuples (tuple) from families of coordinates, and the order read coordinatewise (Ξ -≀).

The binary product came from agda-algebras, where it was the module Classical.Structures.Lattice.Product, with its history. Following agda-algebras' discipline for an eventual Cubical port, the underlying equivalence of the product is isolated in AΓ—B, the pointwise pair of the component equivalences, so that it can be mechanically substituted on the port.

{-# OPTIONS --without-K --exact-split --safe #-}

module Lattices.Product where

-- Imports from the Agda Standard Library ---------------------------------------
open import Data.Fin.Base                          using ( Fin ; zero ; suc ; combine ; remQuot )
open import Data.Fin.Patterns                      using ( 0F ; 1F )
open import Data.Fin.Properties                    using ( remQuot-combine )
open import Data.Nat.Base                          using ( β„• ; zero ; suc ; _*_ )
open import Data.Product                           using ( Ξ£-syntax ; _,_ ; _Γ—_ ; proj₁ ; projβ‚‚ )
open import Data.Unit                              using ( ⊀ ; tt )
open import Function                               using ( Func ; _∘_ )
open import Level                                  using ( Level ; 0β„“ ; _βŠ”_ )
open import Relation.Binary                        using ( Setoid )
open import Relation.Binary.PropositionalEquality  using ( _≑_ ; refl ; sym ; subst )
open import Relation.Nullary.Decidable             using ( yes ; _Γ—-dec_ )

-- Imports from the Agda Universal Algebra Library ------------------------------
open import Classical.Operations                    using ( pair )
open import Classical.Properties.Lattice            using ( module Lattice-Order )
open import Classical.Signatures.Lattice            using ( ∧-Op ; ∨-Op )
open import Classical.Structures.Interpret          using ( interp-cong )
open import Classical.Structures.Lattice.Basic      using ( Lattice ; module Lattice-Op ; eqsToLattice
                                                          ; setoidEqsToLattice )
open import Lattices.Semidistributive               using ( IsSemidistributive )
open import Setoid.Algebras.Basic                   using ( 𝔻[_] ; π•Œ[_] )
open import Setoid.Algebras.Finite                  using ( FiniteAlgebra )
open import Setoid.Homomorphisms.Basic              using ( hom ; mkhom ; compatible-map ; IsHom )

open Func renaming ( to to _⟨$⟩_ )

private variable Ξ± Ξ² ρ Οƒ : Level

The product construction

LatticeProduct 𝑳₁ 𝑳₂ packages the whole development for a fixed pair of lattices; opening it provides the product setoid, the componentwise operations with their congruences and equations, the product lattice, and the characterization of its order.

module LatticeProduct (𝑳₁ : Lattice Ξ± ρ) (𝑳₂ : Lattice Ξ² Οƒ) where
  private
    𝑨 = proj₁ 𝑳₁
    𝑩 = proj₁ 𝑳₂

  open Setoid 𝔻[ 𝑨 ] using ()
    renaming ( _β‰ˆ_ to _β‰ˆβ‚_ ; refl to refl₁ ; sym to sym₁ ; trans to trans₁ )
  open Setoid 𝔻[ 𝑩 ] using ()
    renaming ( _β‰ˆ_ to _β‰ˆβ‚‚_ ; refl to reflβ‚‚ ; sym to symβ‚‚ ; trans to transβ‚‚ )

  open Lattice-Op 𝑳₁ using ()
    renaming ( _∧_ to _βˆ§β‚_ ; _∨_ to _βˆ¨β‚_ ; ∧-cong to βˆ§β‚-cong ; ∨-cong to βˆ¨β‚-cong
             ; ∧-assoc-law to βˆ§β‚-assoc ; ∧-comm-law to βˆ§β‚-comm ; ∧-idem-law to βˆ§β‚-idem
             ; ∨-assoc-law to βˆ¨β‚-assoc ; ∨-comm-law to βˆ¨β‚-comm ; ∨-idem-law to βˆ¨β‚-idem
             ; absorbΛ‘-law to absorbˑ₁ ; absorbΚ³-law to absorbʳ₁ )
  open Lattice-Op 𝑳₂ using ()
    renaming ( _∧_ to _βˆ§β‚‚_ ; _∨_ to _βˆ¨β‚‚_ ; ∧-cong to βˆ§β‚‚-cong ; ∨-cong to βˆ¨β‚‚-cong
             ; ∧-assoc-law to βˆ§β‚‚-assoc ; ∧-comm-law to βˆ§β‚‚-comm ; ∧-idem-law to βˆ§β‚‚-idem
             ; ∨-assoc-law to βˆ¨β‚‚-assoc ; ∨-comm-law to βˆ¨β‚‚-comm ; ∨-idem-law to βˆ¨β‚‚-idem
             ; absorbΛ‘-law to absorbΛ‘β‚‚ ; absorbΚ³-law to absorbΚ³β‚‚ )

The carrier of the product is the pair type, and its equivalence is the pointwise pair of the component equivalences, the isolated-equality locus for the Cubical port.

  AΓ—B : Setoid (Ξ± βŠ” Ξ²) (ρ βŠ” Οƒ)
  AΓ—B = record
    { Carrier        = π•Œ[ 𝑨 ] Γ— π•Œ[ 𝑩 ]
    ; _β‰ˆ_            = Ξ» p q β†’ (proj₁ p β‰ˆβ‚ proj₁ q) Γ— (projβ‚‚ p β‰ˆβ‚‚ projβ‚‚ q)
    ; isEquivalence  = record
        { refl   = refl₁ , reflβ‚‚
        ; sym    = Ξ» e β†’ sym₁ (proj₁ e) , symβ‚‚ (projβ‚‚ e)
        ; trans  = Ξ» (d₁ , dβ‚‚) (e₁ , eβ‚‚) β†’ trans₁ d₁ e₁ , transβ‚‚ dβ‚‚ eβ‚‚
        }
    }

  open Setoid AΓ—B using () renaming ( _β‰ˆ_ to _β‰ˆβ‚“_ )

Meet and join act componentwise. The operations project rather than pattern-match their arguments, so they reduce on any pair expression, matched or not.

  _βˆ§β‚“_ : π•Œ[ 𝑨 ] Γ— π•Œ[ 𝑩 ] β†’ π•Œ[ 𝑨 ] Γ— π•Œ[ 𝑩 ] β†’ π•Œ[ 𝑨 ] Γ— π•Œ[ 𝑩 ]
  p βˆ§β‚“ q = (proj₁ p βˆ§β‚ proj₁ q) , (projβ‚‚ p βˆ§β‚‚ projβ‚‚ q)

  _βˆ¨β‚“_ : π•Œ[ 𝑨 ] Γ— π•Œ[ 𝑩 ] β†’ π•Œ[ 𝑨 ] Γ— π•Œ[ 𝑩 ] β†’ π•Œ[ 𝑨 ] Γ— π•Œ[ 𝑩 ]
  p βˆ¨β‚“ q = (proj₁ p βˆ¨β‚ proj₁ q) , (projβ‚‚ p βˆ¨β‚‚ projβ‚‚ q)

Congruence and the eight equations are all inherited componentwise: each proof is the pair of the component proofs, applied at the projections.

  βˆ§β‚“-cong : βˆ€ {p q u v} β†’ p β‰ˆβ‚“ q β†’ u β‰ˆβ‚“ v β†’ (p βˆ§β‚“ u) β‰ˆβ‚“ (q βˆ§β‚“ v)
  βˆ§β‚“-cong e f = βˆ§β‚-cong (proj₁ e) (proj₁ f) , βˆ§β‚‚-cong (projβ‚‚ e) (projβ‚‚ f)

  βˆ¨β‚“-cong : βˆ€ {p q u v} β†’ p β‰ˆβ‚“ q β†’ u β‰ˆβ‚“ v β†’ (p βˆ¨β‚“ u) β‰ˆβ‚“ (q βˆ¨β‚“ v)
  βˆ¨β‚“-cong e f = βˆ¨β‚-cong (proj₁ e) (proj₁ f) , βˆ¨β‚‚-cong (projβ‚‚ e) (projβ‚‚ f)

  βˆ§β‚“-assoc : βˆ€ {p q r} β†’ ((p βˆ§β‚“ q) βˆ§β‚“ r) β‰ˆβ‚“ (p βˆ§β‚“ (q βˆ§β‚“ r))
  βˆ§β‚“-assoc = βˆ§β‚-assoc , βˆ§β‚‚-assoc

  βˆ§β‚“-comm : βˆ€ {p q} β†’ (p βˆ§β‚“ q) β‰ˆβ‚“ (q βˆ§β‚“ p)
  βˆ§β‚“-comm = βˆ§β‚-comm , βˆ§β‚‚-comm

  βˆ§β‚“-idem : βˆ€ {p} β†’ (p βˆ§β‚“ p) β‰ˆβ‚“ p
  βˆ§β‚“-idem = βˆ§β‚-idem , βˆ§β‚‚-idem

  βˆ¨β‚“-assoc : βˆ€ {p q r} β†’ ((p βˆ¨β‚“ q) βˆ¨β‚“ r) β‰ˆβ‚“ (p βˆ¨β‚“ (q βˆ¨β‚“ r))
  βˆ¨β‚“-assoc = βˆ¨β‚-assoc , βˆ¨β‚‚-assoc

  βˆ¨β‚“-comm : βˆ€ {p q} β†’ (p βˆ¨β‚“ q) β‰ˆβ‚“ (q βˆ¨β‚“ p)
  βˆ¨β‚“-comm = βˆ¨β‚-comm , βˆ¨β‚‚-comm

  βˆ¨β‚“-idem : βˆ€ {p} β†’ (p βˆ¨β‚“ p) β‰ˆβ‚“ p
  βˆ¨β‚“-idem = βˆ¨β‚-idem , βˆ¨β‚‚-idem

  absorbΛ‘β‚“ : βˆ€ {p q} β†’ (p βˆ§β‚“ (p βˆ¨β‚“ q)) β‰ˆβ‚“ p
  absorbΛ‘β‚“ = absorbˑ₁ , absorbΛ‘β‚‚

  absorbΚ³β‚“ : βˆ€ {p q} β†’ ((p βˆ§β‚“ q) βˆ¨β‚“ p) β‰ˆβ‚“ p
  absorbΚ³β‚“ = absorbʳ₁ , absorbΚ³β‚‚

Assembling through the setoid-level builder yields the product lattice.

  Γ—Λ‘-Lattice : Lattice (Ξ± βŠ” Ξ²) (ρ βŠ” Οƒ)
  Γ—Λ‘-Lattice = setoidEqsToLattice AΓ—B _βˆ§β‚“_ _βˆ¨β‚“_ βˆ§β‚“-cong βˆ¨β‚“-cong
    βˆ§β‚“-assoc βˆ§β‚“-comm βˆ§β‚“-idem βˆ¨β‚“-assoc βˆ¨β‚“-comm βˆ¨β‚“-idem absorbΛ‘β‚“ absorbΚ³β‚“

The product order is the componentwise order

The meet order of Γ—Λ‘-Lattice at (p , q) unfolds definitionally to the pair of the component meet orders, because the builder's interpretation applies its argument tuple and the product setoid's equality is the pointwise pair. The three accessors below are therefore projections and pairing, but we name them: they are the interface through which consumers read the product order without unfolding the builder.

  open Lattice-Order Γ—Λ‘-Lattice using () renaming ( _≀_ to _≀ₓ_ )
  open Lattice-Order 𝑳₁ using () renaming ( _≀_ to _≀₁_ )
  open Lattice-Order 𝑳₂ using () renaming ( _≀_ to _≀₂_ )

  -- The product order projects to the first factor's order.
  ≀ₓ-fst : βˆ€ {p q} β†’ p ≀ₓ q β†’ proj₁ p ≀₁ proj₁ q
  ≀ₓ-fst = proj₁

  -- The product order projects to the second factor's order.
  ≀ₓ-snd : βˆ€ {p q} β†’ p ≀ₓ q β†’ projβ‚‚ p ≀₂ projβ‚‚ q
  ≀ₓ-snd = projβ‚‚

  -- Componentwise order proofs pair into a product order proof.
  ≀ₓ-pair : βˆ€ {p q} β†’ proj₁ p ≀₁ proj₁ q β†’ projβ‚‚ p ≀₂ projβ‚‚ q β†’ p ≀ₓ q
  ≀ₓ-pair e f = e , f

The product operator

The standalone binary operator, for consumers that need only the lattice.

infixr 7 _Γ—Λ‘_

_Γ—Λ‘_ : Lattice Ξ± ρ β†’ Lattice Ξ² Οƒ β†’ Lattice (Ξ± βŠ” Ξ²) (ρ βŠ” Οƒ)
𝑳₁ Γ—Λ‘ 𝑳₂ = LatticeProduct.Γ—Λ‘-Lattice 𝑳₁ 𝑳₂

The one-element lattice

-- The one-element lattice, finite and semidistributive.
𝟏ˑ : Lattice 0β„“ 0β„“
𝟏ˑ = eqsToLattice ⊀ (Ξ» _ _ β†’ tt) (Ξ» _ _ β†’ tt)
       (Ξ» _ _ _ β†’ refl) (Ξ» _ _ β†’ refl) (Ξ» _ β†’ refl) (Ξ» _ _ _ β†’ refl) (Ξ» _ _ β†’ refl) (Ξ» _ β†’ refl)
       (Ξ» _ _ β†’ refl) (Ξ» _ _ β†’ refl)

𝟏ˑ-finite : FiniteAlgebra (proj₁ 𝟏ˑ)
𝟏ˑ-finite = record { _β‰Ÿ_ = Ξ» _ _ β†’ yes refl ; card = 1 ; enum = Ξ» _ β†’ tt ; enum-sur = Ξ» _ β†’ zero , refl }

𝟏ˑ-semidistributive : IsSemidistributive 𝟏ˑ
𝟏ˑ-semidistributive = (Ξ» _ _ _ _ β†’ refl) , (Ξ» _ _ _ _ β†’ refl)

Properties of binary products

module Product (𝑳₁ : Lattice Ξ± ρ) (𝑳₂ : Lattice Ξ² Οƒ) where
  open LatticeProduct 𝑳₁ 𝑳₂ public using ( ≀ₓ-fst ; ≀ₓ-snd ; ≀ₓ-pair )
  open Setoid 𝔻[ proj₁ 𝑳₁ ]  using () renaming ( refl to refl₁ )
  open Setoid 𝔻[ proj₁ 𝑳₂ ]  using () renaming ( refl to reflβ‚‚ )

  -- The projections are homomorphisms.
  fst-hom : hom (proj₁ (𝑳₁ Γ—Λ‘ 𝑳₂)) (proj₁ 𝑳₁)
  fst-hom = mkhom (proj₁ (𝑳₁ Γ—Λ‘ 𝑳₂)) (proj₁ 𝑳₁) (record { to = proj₁ ; cong = proj₁ }) compatible
    where
    compatible : compatible-map (proj₁ (𝑳₁ Γ—Λ‘ 𝑳₂)) (proj₁ 𝑳₁) (record { to = proj₁ ; cong = proj₁ })
    compatible {∧-Op} {a} = interp-cong (proj₁ 𝑳₁) ∧-Op Ξ» { 0F β†’ refl₁ ; 1F β†’ refl₁ }
    compatible {∨-Op} {a} = interp-cong (proj₁ 𝑳₁) ∨-Op Ξ» { 0F β†’ refl₁ ; 1F β†’ refl₁ }

  snd-hom : hom (proj₁ (𝑳₁ Γ—Λ‘ 𝑳₂)) (proj₁ 𝑳₂)
  snd-hom = mkhom (proj₁ (𝑳₁ Γ—Λ‘ 𝑳₂)) (proj₁ 𝑳₂) (record { to = projβ‚‚ ; cong = projβ‚‚ }) compatible
    where
    compatible : compatible-map (proj₁ (𝑳₁ Γ—Λ‘ 𝑳₂)) (proj₁ 𝑳₂) (record { to = projβ‚‚ ; cong = projβ‚‚ })
    compatible {∧-Op} {a} = interp-cong (proj₁ 𝑳₂) ∧-Op Ξ» { 0F β†’ reflβ‚‚ ; 1F β†’ reflβ‚‚ }
    compatible {∨-Op} {a} = interp-cong (proj₁ 𝑳₂) ∨-Op Ξ» { 0F β†’ reflβ‚‚ ; 1F β†’ reflβ‚‚ }

  -- A product of finite lattices is finite.
  Γ—Λ‘-finite : FiniteAlgebra (proj₁ 𝑳₁) β†’ FiniteAlgebra (proj₁ 𝑳₂) β†’ FiniteAlgebra (proj₁ (𝑳₁ Γ—Λ‘ 𝑳₂))
  Γ—Λ‘-finite F₁ Fβ‚‚ = record
    { _β‰Ÿ_       = Ξ» (x₁ , xβ‚‚) (y₁ , yβ‚‚) β†’ (x₁ β‰Ÿβ‚ y₁) Γ—-dec (xβ‚‚ β‰Ÿβ‚‚ yβ‚‚)
    ; card      = card₁ * cardβ‚‚
    ; enum      = enum
    ; enum-sur  = sur
    }
    where
    open FiniteAlgebra F₁ renaming ( _β‰Ÿ_ to _β‰Ÿβ‚_ ; card to card₁ ; enum to enum₁ ; enum-sur to sur₁ )
    open FiniteAlgebra Fβ‚‚ renaming ( _β‰Ÿ_ to _β‰Ÿβ‚‚_ ; card to cardβ‚‚ ; enum to enumβ‚‚ ; enum-sur to surβ‚‚ )
    open Setoid 𝔻[ proj₁ (𝑳₁ Γ—Λ‘ 𝑳₂) ] using ( _β‰ˆ_ )

    enum : Fin (card₁ * cardβ‚‚) β†’ π•Œ[ proj₁ (𝑳₁ Γ—Λ‘ 𝑳₂) ]
    enum i = enum₁ (proj₁ (remQuot {m = card₁} cardβ‚‚ i)) , enumβ‚‚ (projβ‚‚ (remQuot {m = card₁} cardβ‚‚ i))

    sur : βˆ€ p β†’ Ξ£[ i ∈ Fin (card₁ * cardβ‚‚) ] enum i β‰ˆ p
    sur (x , y) with sur₁ x | surβ‚‚ y
    ... | j , e₁ | k , eβ‚‚ =
      combine j k , subst (Ξ» q β†’ (enum₁ (proj₁ q) , enumβ‚‚ (projβ‚‚ q)) β‰ˆ (x , y)) (sym (remQuot-combine {n = card₁} {k = cardβ‚‚} j k)) (e₁ , eβ‚‚)

  -- A product of semidistributive lattices is semidistributive.
  Γ—Λ‘-semidistributive : IsSemidistributive 𝑳₁ β†’ IsSemidistributive 𝑳₂ β†’ IsSemidistributive (𝑳₁ Γ—Λ‘ 𝑳₂)
  Γ—Λ‘-semidistributive (j₁ , m₁) (jβ‚‚ , mβ‚‚) =
      (Ξ» a b c (e₁ , eβ‚‚) β†’ j₁ _ _ _ e₁ , jβ‚‚ _ _ _ eβ‚‚)
    , (Ξ» a b c (e₁ , eβ‚‚) β†’ m₁ _ _ _ e₁ , mβ‚‚ _ _ _ eβ‚‚)

Products over Fin m

-- The product of a family indexed by Fin m, and its properties.
Ξ  : (m : β„•) β†’ (Fin m β†’ Lattice 0β„“ 0β„“) β†’ Lattice 0β„“ 0β„“
Ξ  zero     𝓛 = 𝟏ˑ
Ξ  (suc m)  𝓛 = 𝓛 zero Γ—Λ‘ Ξ  m (𝓛 ∘ suc)

Ξ -finite : βˆ€ m (𝓛 : Fin m β†’ Lattice 0β„“ 0β„“) β†’ (βˆ€ j β†’ FiniteAlgebra (proj₁ (𝓛 j))) β†’ FiniteAlgebra (proj₁ (Ξ  m 𝓛))
Ξ -finite zero     𝓛 F = 𝟏ˑ-finite
Ξ -finite (suc m)  𝓛 F = Product.Γ—Λ‘-finite (𝓛 zero) (Ξ  m (𝓛 ∘ suc)) (F zero) (Ξ -finite m (𝓛 ∘ suc) (F ∘ suc))

Ξ -semidistributive : βˆ€ m (𝓛 : Fin m β†’ Lattice 0β„“ 0β„“) β†’ (βˆ€ j β†’ IsSemidistributive (𝓛 j)) β†’ IsSemidistributive (Ξ  m 𝓛)
Ξ -semidistributive zero     𝓛 S = 𝟏ˑ-semidistributive
Ξ -semidistributive (suc m)  𝓛 S =
  Product.Γ—Λ‘-semidistributive (𝓛 zero) (Ξ  m (𝓛 ∘ suc)) (S zero) (Ξ -semidistributive m (𝓛 ∘ suc) (S ∘ suc))

-- The j-th projection, as a map.
projMap : βˆ€ m (𝓛 : Fin m β†’ Lattice 0β„“ 0β„“) (j : Fin m) β†’ π•Œ[ proj₁ (Ξ  m 𝓛) ] β†’ π•Œ[ proj₁ (𝓛 j) ]
projMap (suc m) 𝓛 zero     = proj₁
projMap (suc m) 𝓛 (suc j)  = projMap m (𝓛 ∘ suc) j ∘ projβ‚‚

-- A tuple from a family of coordinates.
tuple : βˆ€ m (𝓛 : Fin m β†’ Lattice 0β„“ 0β„“) β†’ (βˆ€ j β†’ π•Œ[ proj₁ (𝓛 j) ]) β†’ π•Œ[ proj₁ (Ξ  m 𝓛) ]
tuple zero     𝓛 f = tt
tuple (suc m)  𝓛 f = f zero , tuple m (𝓛 ∘ suc) (f ∘ suc)

projMap-tuple : βˆ€ m 𝓛 (f : βˆ€ j β†’ π•Œ[ proj₁ (𝓛 j) ]) j β†’ projMap m 𝓛 j (tuple m 𝓛 f) ≑ f j
projMap-tuple (suc m) 𝓛 f zero     = refl
projMap-tuple (suc m) 𝓛 f (suc j)  = projMap-tuple m (𝓛 ∘ suc) (f ∘ suc) j

-- The projections are homomorphisms.
proj : βˆ€ m (𝓛 : Fin m β†’ Lattice 0β„“ 0β„“) (j : Fin m) β†’ hom (proj₁ (Ξ  m 𝓛)) (proj₁ (𝓛 j))
proj (suc m) 𝓛 zero     = Product.fst-hom (𝓛 zero) (Ξ  m (𝓛 ∘ suc))
proj (suc m) 𝓛 (suc j)  = mkhom (proj₁ (Ξ  (suc m) 𝓛)) (proj₁ (𝓛 (suc j))) map compatible
  where
  inner = proj m (𝓛 ∘ suc) j
  map : Func 𝔻[ proj₁ (Ξ  (suc m) 𝓛) ] 𝔻[ proj₁ (𝓛 (suc j)) ]
  map = record { to = Ξ» x β†’ proj₁ inner ⟨$⟩ projβ‚‚ x ; cong = Ξ» e β†’ Func.cong (proj₁ inner) (projβ‚‚ e) }
  open Setoid 𝔻[ proj₁ (𝓛 (suc j)) ] using () renaming ( refl to β‰ˆrefl ; trans to β‰ˆtrans )
  compatible : compatible-map (proj₁ (Ξ  (suc m) 𝓛)) (proj₁ (𝓛 (suc j))) map
  compatible {∧-Op} {a} =
    β‰ˆtrans (IsHom.compatible (projβ‚‚ inner) {∧-Op} {pair (projβ‚‚ (a 0F)) (projβ‚‚ (a 1F))})
           (interp-cong (proj₁ (𝓛 (suc j))) ∧-Op Ξ» { 0F β†’ β‰ˆrefl ; 1F β†’ β‰ˆrefl })
  compatible {∨-Op} {a} =
    β‰ˆtrans (IsHom.compatible (projβ‚‚ inner) {∨-Op} {pair (projβ‚‚ (a 0F)) (projβ‚‚ (a 1F))})
           (interp-cong (proj₁ (𝓛 (suc j))) ∨-Op Ξ» { 0F β†’ β‰ˆrefl ; 1F β†’ β‰ˆrefl })

proj-map : βˆ€ m 𝓛 j x β†’ proj₁ (proj m 𝓛 j) ⟨$⟩ x ≑ projMap m 𝓛 j x
proj-map (suc m) 𝓛 zero     x = refl
proj-map (suc m) 𝓛 (suc j)  x = proj-map m (𝓛 ∘ suc) j (projβ‚‚ x)

-- The order of the product, from the coordinates.
Ξ -≀ : βˆ€ m 𝓛 x y β†’ (βˆ€ j β†’ Lattice-Order._≀_ (𝓛 j) (projMap m 𝓛 j x) (projMap m 𝓛 j y))
    β†’ Lattice-Order._≀_ (Ξ  m 𝓛) x y
Ξ -≀ zero     𝓛 x y h = refl
Ξ -≀ (suc m)  𝓛 x y h = h zero , Ξ -≀ m (𝓛 ∘ suc) (projβ‚‚ x) (projβ‚‚ y) (h ∘ suc)