Prove that a lattice of height h1+h2 exists for products

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

Lattice.agda

@@ -4,11 +4,11 @@ import Data.Nat.Properties as NatProps
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
 open import Relation.Binary.Definitions
 open import Relation.Nullary using (Dec; ¬_)
-open import Data.Nat as Nat using (ℕ; _≤_)
+open import Data.Nat as Nat using (ℕ; _≤_; _+_)
-open import Data.Product using (_×_; Σ; _,_)
+open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
-open import Chain using (Chain; Height; done; step)
+open import Chain using (Chain; Height; done; step; concat)
 open import Function.Definitions using (Injective)
 
 record IsEquivalence {a} (A : Set a) (_≈_ : A → A → Set a) : Set a where
@@ -38,6 +38,9 @@ record IsSemilattice {a} (A : Set a)
         ⊔-comm : (x y : A) → (x ⊔ y) ≈ (y ⊔ x)
         ⊔-idemp : (x : A) → (x ⊔ x) ≈ x
 
+    ≼-refl : ∀ (a : A) → a ≼ a
+    ≼-refl a = (a , ⊔-idemp a)
+
     open IsEquivalence ≈-equiv public
 
 record IsLattice {a} (A : Set a)
@@ -57,6 +60,9 @@ record IsLattice {a} (A : Set a)
         ( ⊔-assoc to ⊓-assoc
         ; ⊔-comm to ⊓-comm
         ; ⊔-idemp to ⊓-idemp
+        ; _≼_ to _≽_
+        ; _≺_ to _≻_
+        ; ≼-refl to ≽-refl
         )
 
 record IsFiniteHeightLattice {a} (A : Set a)
@@ -72,17 +78,20 @@ record IsFiniteHeightLattice {a} (A : Set a)
     open IsLattice isLattice public
 
 module _ {a b} {A : Set a} {B : Set b}
-    (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b)
+    (_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) where
-    (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
+
+    Monotonic : (A → B) → Set (a ⊔ℓ b)
+    Monotonic f = ∀ {a₁ a₂ : A} → a₁ ≼₁ a₂ → f a₁ ≼₂ f a₂
+
+module ChainMapping {a b} {A : Set a} {B : Set b}
+    {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b}
+    {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}
     (slA : IsSemilattice A _≈₁_ _⊔₁_) (slB : IsSemilattice B _≈₂_ _⊔₂_) where
 
     open IsSemilattice slA renaming (_≼_ to _≼₁_; _≺_ to _≺₁_)
     open IsSemilattice slB renaming (_≼_ to _≼₂_; _≺_ to _≺₂_)
 
-    Monotonic : (A → B) → Set (a ⊔ℓ b)
+    Chain-map : ∀ (f : A → B) → Monotonic _≼₁_ _≼₂_ f → Injective _≈₁_ _≈₂_ f →
-    Monotonic f = ∀ {a₁ a₂ : A} → a₁ ≼₁ a₂ → f a₁ ≼₂ f a₂
-
-    Chain-map : ∀ (f : A → B) → Monotonic f → Injective _≈₁_ _≈₂_ f →
                 ∀ {a₁ a₂ : A} {n : ℕ} → Chain _≺₁_ a₁ a₂ n → Chain _≺₂_ (f a₁) (f a₂) n
     Chain-map f Monotonicᶠ Injectiveᶠ done = done
     Chain-map f Monotonicᶠ Injectiveᶠ (step (a₁≼₁a , a₁̷≈₁a) aa₂) =
@@ -378,3 +387,52 @@ module IsLatticeInstances where
             ; absorb-⊔-⊓ = union-intersect-absorb _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ _⊓₂_ ⊔₂-idemp ⊓₂-idemp absorb-⊔₂-⊓₂ absorb-⊓₂-⊔₂
             ; absorb-⊓-⊔ = intersect-union-absorb _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ _⊓₂_ ⊔₂-idemp ⊓₂-idemp absorb-⊔₂-⊓₂ absorb-⊓₂-⊔₂
             }
+
+module IsFiniteHeightLatticeInstances where
+    module ForProd {a} {A B : Set a}
+        (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
+        (_⊔₁_ : A → A → A) (_⊓₁_ : A → A → A)
+        (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
+        (h₁ h₂ : ℕ)
+        (lA : IsFiniteHeightLattice A h₁ _≈₁_ _⊔₁_ _⊓₁_) (lB : IsFiniteHeightLattice B h₂ _≈₂_ _⊔₂_ _⊓₂_) where
+
+        module ProdLattice = IsLatticeInstances.ForProd _≈₁_ _≈₂_ _⊔₁_ _⊓₁_ _⊔₂_ _⊓₂_ (IsFiniteHeightLattice.isLattice lA) (IsFiniteHeightLattice.isLattice lB)
+        open ProdLattice using (_⊔_; _⊓_; _≈_) public
+        open IsLattice ProdLattice.ProdIsLattice using (_≼_; _≺_)
+        open IsFiniteHeightLattice lA using () renaming (⊔-idemp to ⊔₁-idemp; _≼_ to _≼₁_)
+        open IsFiniteHeightLattice lB using () renaming (⊔-idemp to ⊔₂-idemp; _≼_ to _≼₂_)
+
+        module ChainMapping₁ = ChainMapping (IsFiniteHeightLattice.joinSemilattice lA) (IsLattice.joinSemilattice ProdLattice.ProdIsLattice)
+        module ChainMapping₂ = ChainMapping (IsFiniteHeightLattice.joinSemilattice lB) (IsLattice.joinSemilattice ProdLattice.ProdIsLattice)
+
+        private
+            a,∙-Monotonic : ∀ (a : A) → Monotonic _≼₂_ _≼_ (λ b → (a , b))
+            a,∙-Monotonic a {b₁} {b₂} (b , b₁⊔b≈b₂) = ((a , b) , (⊔₁-idemp a , b₁⊔b≈b₂))
+
+            ∙,b-Monotonic : ∀ (b : B) → Monotonic _≼₁_ _≼_ (λ a → (a , b))
+            ∙,b-Monotonic b {a₁} {a₂} (a , a₁⊔a≈a₂) = ((a , b) , (a₁⊔a≈a₂ , ⊔₂-idemp b))
+
+            amin : A
+            amin = proj₁ (proj₁ (proj₁ (IsFiniteHeightLattice.fixedHeight lA)))
+
+            amax : A
+            amax = proj₂ (proj₁ (proj₁ (IsFiniteHeightLattice.fixedHeight lA)))
+
+            bmin : B
+            bmin = proj₁ (proj₁ (proj₁ (IsFiniteHeightLattice.fixedHeight lB)))
+
+            bmax : B
+            bmax = proj₂ (proj₁ (proj₁ (IsFiniteHeightLattice.fixedHeight lB)))
+
+        ProdIsFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
+        ProdIsFiniteHeightLattice = record
+            { isLattice = ProdLattice.ProdIsLattice
+            ; fixedHeight =
+                ( ( ((amin , bmin) , (amax , bmax))
+                  , concat _≺_
+                      (ChainMapping₁.Chain-map (λ a → (a , bmin)) (∙,b-Monotonic _) proj₁ (proj₂ (proj₁ (IsFiniteHeightLattice.fixedHeight lA))))
+                      (ChainMapping₂.Chain-map (λ b → (amax , b)) (a,∙-Monotonic _) proj₂ (proj₂ (proj₁ (IsFiniteHeightLattice.fixedHeight lB))))
+                  )
+                , _
+                )
+            }