diff --git a/Equivalence.agda b/Equivalence.agda index 82abed5..a17a438 100644 --- a/Equivalence.agda +++ b/Equivalence.agda @@ -9,29 +9,3 @@ record IsEquivalence {a} (A : Set a) (_≈_ : A → A → Set a) : Set a where ≈-refl : {a : A} → a ≈ a ≈-sym : {a b : A} → a ≈ b → b ≈ a ≈-trans : {a b c : A} → a ≈ b → b ≈ c → a ≈ c - -module IsEquivalenceInstances where - module ForProd {a} {A B : Set a} - (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a) - (eA : IsEquivalence A _≈₁_) (eB : IsEquivalence B _≈₂_) where - - infix 4 _≈_ - - _≈_ : A × B → A × B → Set a - (a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂) - - ProdEquivalence : IsEquivalence (A × B) _≈_ - ProdEquivalence = record - { ≈-refl = λ {p} → - ( IsEquivalence.≈-refl eA - , IsEquivalence.≈-refl eB - ) - ; ≈-sym = λ {p₁} {p₂} (a₁≈a₂ , b₁≈b₂) → - ( IsEquivalence.≈-sym eA a₁≈a₂ - , IsEquivalence.≈-sym eB b₁≈b₂ - ) - ; ≈-trans = λ {p₁} {p₂} {p₃} (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) → - ( IsEquivalence.≈-trans eA a₁≈a₂ a₂≈a₃ - , IsEquivalence.≈-trans eB b₁≈b₂ b₂≈b₃ - ) - } diff --git a/Lattice.agda b/Lattice.agda index 4d08965..14674e0 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -6,7 +6,6 @@ import Chain import Data.Nat.Properties as NatProps open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; subst) open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎) -open import Relation.Binary.Definitions open import Relation.Binary.Core using (_Preserves_⟶_ ) open import Relation.Nullary using (Dec; ¬_; yes; no) open import Data.Nat as Nat using (ℕ; _≤_; _+_; suc) @@ -142,152 +141,3 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where isLattice : IsLattice A _≈_ _⊔_ _⊓_ open IsLattice isLattice public - -module IsSemilatticeInstances where - module ForProd {a} {A B : Set a} - (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a) - (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B) - (sA : IsSemilattice A _≈₁_ _⊔₁_) (sB : IsSemilattice B _≈₂_ _⊔₂_) where - - open Eq - open Data.Product - - module ProdEquiv = IsEquivalenceInstances.ForProd _≈₁_ _≈₂_ (IsSemilattice.≈-equiv sA) (IsSemilattice.≈-equiv sB) - open ProdEquiv using (_≈_) public - - infixl 20 _⊔_ - - _⊔_ : A × B → A × B → A × B - (a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂) - - ProdIsSemilattice : IsSemilattice (A × B) _≈_ _⊔_ - ProdIsSemilattice = record - { ≈-equiv = ProdEquiv.ProdEquivalence - ; ≈-⊔-cong = λ (a₁≈a₂ , b₁≈b₂) (a₃≈a₄ , b₃≈b₄) → - ( IsSemilattice.≈-⊔-cong sA a₁≈a₂ a₃≈a₄ - , IsSemilattice.≈-⊔-cong sB b₁≈b₂ b₃≈b₄ - ) - ; ⊔-assoc = λ (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) → - ( IsSemilattice.⊔-assoc sA a₁ a₂ a₃ - , IsSemilattice.⊔-assoc sB b₁ b₂ b₃ - ) - ; ⊔-comm = λ (a₁ , b₁) (a₂ , b₂) → - ( IsSemilattice.⊔-comm sA a₁ a₂ - , IsSemilattice.⊔-comm sB b₁ b₂ - ) - ; ⊔-idemp = λ (a , b) → - ( IsSemilattice.⊔-idemp sA a - , IsSemilattice.⊔-idemp sB b - ) - } - -module IsLatticeInstances 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) - (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where - - module ProdJoin = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ (IsLattice.joinSemilattice lA) (IsLattice.joinSemilattice lB) - open ProdJoin using (_⊔_; _≈_) public - - module ProdMeet = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊓₁_ _⊓₂_ (IsLattice.meetSemilattice lA) (IsLattice.meetSemilattice lB) - open ProdMeet using () renaming (_⊔_ to _⊓_) public - - ProdIsLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_ - ProdIsLattice = record - { joinSemilattice = ProdJoin.ProdIsSemilattice - ; meetSemilattice = ProdMeet.ProdIsSemilattice - ; absorb-⊔-⊓ = λ (a₁ , b₁) (a₂ , b₂) → - ( IsLattice.absorb-⊔-⊓ lA a₁ a₂ - , IsLattice.absorb-⊔-⊓ lB b₁ b₂ - ) - ; absorb-⊓-⊔ = λ (a₁ , b₁) (a₂ , b₂) → - ( IsLattice.absorb-⊓-⊔ lA a₁ a₂ - , IsLattice.absorb-⊓-⊔ lB b₁ b₂ - ) - } - - -module IsFiniteHeightLatticeInstances where - module ForProd {a} {A B : Set a} - (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a) - (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) - (_⊔₁_ : A → A → A) (_⊓₁_ : A → A → A) - (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B) - (h₁ h₂ : ℕ) - (lA : IsFiniteHeightLattice A h₁ _≈₁_ _⊔₁_ _⊓₁_) (lB : IsFiniteHeightLattice B h₂ _≈₂_ _⊔₂_ _⊓₂_) where - - open NatProps - module ProdLattice = IsLatticeInstances.ForProd _≈₁_ _≈₂_ _⊔₁_ _⊓₁_ _⊔₂_ _⊓₂_ (IsFiniteHeightLattice.isLattice lA) (IsFiniteHeightLattice.isLattice lB) - open ProdLattice using (_⊔_; _⊓_; _≈_) public - open IsLattice ProdLattice.ProdIsLattice using (_≼_; _≺_; ≺-cong; ≈-equiv) - open IsFiniteHeightLattice lA using () renaming (⊔-idemp to ⊔₁-idemp; _≼_ to _≼₁_; ≈-equiv to ≈₁-equiv; ≈-refl to ≈₁-refl; ≈-trans to ≈₁-trans; ≈-sym to ≈₁-sym; _≺_ to _≺₁_; ≺-cong to ≺₁-cong) - open IsFiniteHeightLattice lB using () renaming (⊔-idemp to ⊔₂-idemp; _≼_ to _≼₂_; ≈-equiv to ≈₂-equiv; ≈-refl to ≈₂-refl; ≈-trans to ≈₂-trans; ≈-sym to ≈₂-sym; _≺_ to _≺₂_; ≺-cong to ≺₂-cong) - - module ChainMapping₁ = ChainMapping (IsFiniteHeightLattice.joinSemilattice lA) (IsLattice.joinSemilattice ProdLattice.ProdIsLattice) - module ChainMapping₂ = ChainMapping (IsFiniteHeightLattice.joinSemilattice lB) (IsLattice.joinSemilattice ProdLattice.ProdIsLattice) - - module ChainA = Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong - module ChainB = Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong - module ProdChain = Chain _≈_ ≈-equiv _≺_ ≺-cong - - open ChainA using () renaming (Chain to Chain₁; done to done₁; step to step₁; Chain-≈-cong₁ to Chain₁-≈-cong₁) - open ChainB using () renaming (Chain to Chain₂; done to done₂; step to step₂; Chain-≈-cong₁ to Chain₂-≈-cong₁) - open ProdChain using (Chain; concat; done; step) - - 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₂)) - - a,∙-Preserves-≈₂ : ∀ (a : A) → (λ b → (a , b)) Preserves _≈₂_ ⟶ _≈_ - a,∙-Preserves-≈₂ a {b₁} {b₂} b₁≈b₂ = (≈₁-refl , 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)) - - ∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶ _≈_ - ∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl) - - 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))) - - unzip : ∀ {a₁ a₂ : A} {b₁ b₂ : B} {n : ℕ} → Chain (a₁ , b₁) (a₂ , b₂) n → Σ (ℕ × ℕ) (λ (n₁ , n₂) → ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n ≤ n₁ + n₂))) - unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl)) - unzip {a₁} {a₂} {b₁} {b₂} {n} (step {(a₁ , b₁)} {(a , b)} (((d₁ , d₂) , (a₁⊔d₁≈a , b₁⊔d₂≈b)) , a₁b₁̷≈ab) (a≈a' , b≈b') a'b'a₂b₂) - with ≈₁-dec a₁ a | ≈₂-dec b₁ b | unzip a'b'a₂b₂ - ... | yes a₁≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = absurd (a₁b₁̷≈ab (a₁≈a , b₁≈b)) - ... | no a₁̷≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = - ((suc n₁ , n₂) , ((step₁ ((d₁ , a₁⊔d₁≈a) , a₁̷≈a) a≈a' c₁ , Chain₂-≈-cong₁ (≈₂-sym (≈₂-trans b₁≈b b≈b')) c₂), +-monoʳ-≤ 1 (n≤n₁+n₂))) - ... | yes a₁≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = - ((n₁ , suc n₂) , ( (Chain₁-≈-cong₁ (≈₁-sym (≈₁-trans a₁≈a a≈a')) c₁ , step₂ ((d₂ , b₁⊔d₂≈b) , b₁̷≈b) b≈b' c₂) - , subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂) - )) - ... | no a₁̷≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = - ((suc n₁ , suc n₂) , ( (step₁ ((d₁ , a₁⊔d₁≈a) , a₁̷≈a) a≈a' c₁ , step₂ ((d₂ , b₁⊔d₂≈b) , b₁̷≈b) b≈b' c₂) - , ≤-stepsˡ 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂)) - )) - - 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₁ (∙,b-Preserves-≈₁ _) (proj₂ (proj₁ (IsFiniteHeightLattice.fixedHeight lA)))) - (ChainMapping₂.Chain-map (λ b → (amax , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) (proj₂ (proj₁ (IsFiniteHeightLattice.fixedHeight lB)))) - ) - , λ a₁b₁a₂b₂ → let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂ - in ≤-trans n≤n₁+n₂ (+-mono-≤ (proj₂ (IsFiniteHeightLattice.fixedHeight lA) a₁a₂) - (proj₂ (IsFiniteHeightLattice.fixedHeight lB) b₁b₂)) - ) - } diff --git a/Lattice/Prod.agda b/Lattice/Prod.agda new file mode 100644 index 0000000..dbe36e9 --- /dev/null +++ b/Lattice/Prod.agda @@ -0,0 +1,168 @@ +open import Lattice + +module Lattice.Prod {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 (_×_; Σ; _,_; proj₁; proj₂) +open import Equivalence +open import Relation.Binary.Core using (_Preserves_⟶_ ) +open import Relation.Binary.Definitions +open import Relation.Binary.PropositionalEquality using (sym; subst) +open import Relation.Nullary using (¬_; yes; no) +import Chain + +open IsLattice lA using () renaming + ( ≈-equiv to ≈₁-equiv; ≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans + ; joinSemilattice to joinSemilattice₁ + ; meetSemilattice to meetSemilattice₁ + ; FixedHeight to FixedHeight₁ + ; ⊔-idemp to ⊔₁-idemp + ; _≼_ to _≼₁_; _≺_ to _≺₁_ + ; ≺-cong to ≺₁-cong + ) + +open IsLattice lB using () renaming + ( ≈-equiv to ≈₂-equiv; ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans + ; joinSemilattice to joinSemilattice₂ + ; meetSemilattice to meetSemilattice₂ + ; FixedHeight to FixedHeight₂ + ; ⊔-idemp to ⊔₂-idemp + ; _≼_ to _≼₂_; _≺_ to _≺₂_ + ; ≺-cong to ≺₂-cong + ) + +_≈_ : A × B → A × B → Set a +(a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂) + +≈-equiv : IsEquivalence (A × B) _≈_ +≈-equiv = record + { ≈-refl = λ {p} → (≈₁-refl , ≈₂-refl) + ; ≈-sym = λ {p₁} {p₂} (a₁≈a₂ , b₁≈b₂) → (≈₁-sym a₁≈a₂ , ≈₂-sym b₁≈b₂) + ; ≈-trans = λ {p₁} {p₂} {p₃} (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) → + ( ≈₁-trans a₁≈a₂ a₂≈a₃ , ≈₂-trans b₁≈b₂ b₂≈b₃ ) + } + +_⊔_ : A × B → A × B → A × B +(a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂) + +_⊓_ : A × B → A × B → A × B +(a₁ , b₁) ⊓ (a₂ , b₂) = (a₁ ⊓₁ a₂ , b₁ ⊓₂ b₂) + +private module ProdIsSemilattice (f₁ : A → A → A) (f₂ : B → B → B) (sA : IsSemilattice A _≈₁_ f₁) (sB : IsSemilattice B _≈₂_ f₂) where + isSemilattice : IsSemilattice (A × B) _≈_ (λ (a₁ , b₁) (a₂ , b₂) → (f₁ a₁ a₂ , f₂ b₁ b₂)) + isSemilattice = record + { ≈-equiv = ≈-equiv + ; ≈-⊔-cong = λ (a₁≈a₂ , b₁≈b₂) (a₃≈a₄ , b₃≈b₄) → + ( IsSemilattice.≈-⊔-cong sA a₁≈a₂ a₃≈a₄ + , IsSemilattice.≈-⊔-cong sB b₁≈b₂ b₃≈b₄ + ) + ; ⊔-assoc = λ (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) → + ( IsSemilattice.⊔-assoc sA a₁ a₂ a₃ + , IsSemilattice.⊔-assoc sB b₁ b₂ b₃ + ) + ; ⊔-comm = λ (a₁ , b₁) (a₂ , b₂) → + ( IsSemilattice.⊔-comm sA a₁ a₂ + , IsSemilattice.⊔-comm sB b₁ b₂ + ) + ; ⊔-idemp = λ (a , b) → + ( IsSemilattice.⊔-idemp sA a + , IsSemilattice.⊔-idemp sB b + ) + } + +isJoinSemilattice : IsSemilattice (A × B) _≈_ _⊔_ +isJoinSemilattice = ProdIsSemilattice.isSemilattice _⊔₁_ _⊔₂_ joinSemilattice₁ joinSemilattice₂ + +isMeetSemilattice : IsSemilattice (A × B) _≈_ _⊓_ +isMeetSemilattice = ProdIsSemilattice.isSemilattice _⊓₁_ _⊓₂_ meetSemilattice₁ meetSemilattice₂ + +isLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_ +isLattice = record + { joinSemilattice = isJoinSemilattice + ; meetSemilattice = isMeetSemilattice + ; absorb-⊔-⊓ = λ (a₁ , b₁) (a₂ , b₂) → + ( IsLattice.absorb-⊔-⊓ lA a₁ a₂ + , IsLattice.absorb-⊔-⊓ lB b₁ b₂ + ) + ; absorb-⊓-⊔ = λ (a₁ , b₁) (a₂ , b₂) → + ( IsLattice.absorb-⊓-⊔ lA a₁ a₂ + , IsLattice.absorb-⊓-⊔ lB b₁ b₂ + ) + } + +module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) + (h₁ h₂ : ℕ) + (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where + + open import Data.Nat.Properties + open IsLattice isLattice using (_≼_; _≺_; ≺-cong) + + module ChainMapping₁ = ChainMapping joinSemilattice₁ isJoinSemilattice + module ChainMapping₂ = ChainMapping joinSemilattice₂ isJoinSemilattice + + module ChainA = Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong + module ChainB = Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong + module ProdChain = Chain _≈_ ≈-equiv _≺_ ≺-cong + + open ChainA using () renaming (Chain to Chain₁; done to done₁; step to step₁; Chain-≈-cong₁ to Chain₁-≈-cong₁) + open ChainB using () renaming (Chain to Chain₂; done to done₂; step to step₂; Chain-≈-cong₁ to Chain₂-≈-cong₁) + open ProdChain using (Chain; concat; done; step) + + 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₂)) + + a,∙-Preserves-≈₂ : ∀ (a : A) → (λ b → (a , b)) Preserves _≈₂_ ⟶ _≈_ + a,∙-Preserves-≈₂ a {b₁} {b₂} b₁≈b₂ = (≈₁-refl , 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)) + + ∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶ _≈_ + ∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl) + + amin : A + amin = proj₁ (proj₁ (proj₁ fhA)) + + amax : A + amax = proj₂ (proj₁ (proj₁ fhA)) + + bmin : B + bmin = proj₁ (proj₁ (proj₁ fhB)) + + bmax : B + bmax = proj₂ (proj₁ (proj₁ fhB)) + + unzip : ∀ {a₁ a₂ : A} {b₁ b₂ : B} {n : ℕ} → Chain (a₁ , b₁) (a₂ , b₂) n → Σ (ℕ × ℕ) (λ (n₁ , n₂) → ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n ≤ n₁ + n₂))) + unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl)) + unzip {a₁} {a₂} {b₁} {b₂} {n} (step {(a₁ , b₁)} {(a , b)} (((d₁ , d₂) , (a₁⊔d₁≈a , b₁⊔d₂≈b)) , a₁b₁̷≈ab) (a≈a' , b≈b') a'b'a₂b₂) + with ≈₁-dec a₁ a | ≈₂-dec b₁ b | unzip a'b'a₂b₂ + ... | yes a₁≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = absurd (a₁b₁̷≈ab (a₁≈a , b₁≈b)) + ... | no a₁̷≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = + ((suc n₁ , n₂) , ((step₁ ((d₁ , a₁⊔d₁≈a) , a₁̷≈a) a≈a' c₁ , Chain₂-≈-cong₁ (≈₂-sym (≈₂-trans b₁≈b b≈b')) c₂), +-monoʳ-≤ 1 (n≤n₁+n₂))) + ... | yes a₁≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = + ((n₁ , suc n₂) , ( (Chain₁-≈-cong₁ (≈₁-sym (≈₁-trans a₁≈a a≈a')) c₁ , step₂ ((d₂ , b₁⊔d₂≈b) , b₁̷≈b) b≈b' c₂) + , subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂) + )) + ... | no a₁̷≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = + ((suc n₁ , suc n₂) , ( (step₁ ((d₁ , a₁⊔d₁≈a) , a₁̷≈a) a≈a' c₁ , step₂ ((d₂ , b₁⊔d₂≈b) , b₁̷≈b) b≈b' c₂) + , ≤-stepsˡ 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂)) + )) + + isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_ + isFiniteHeightLattice = record + { isLattice = isLattice + ; fixedHeight = + ( ( ((amin , bmin) , (amax , bmax)) + , concat + (ChainMapping₁.Chain-map (λ a → (a , bmin)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) (proj₂ (proj₁ fhA))) + (ChainMapping₂.Chain-map (λ b → (amax , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) (proj₂ (proj₁ fhB))) + ) + , λ a₁b₁a₂b₂ → let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂ + in ≤-trans n≤n₁+n₂ (+-mono-≤ (proj₂ fhA a₁a₂) (proj₂ fhB b₁b₂)) + ) + }