agda-spa/Lattice.agda

442 lines
22 KiB
Agda
Raw Normal View History

module Lattice where
open import Equivalence
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)
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 Function.Definitions using (Injective)
open import Data.Empty using ()
absurd : {a} {A : Set a} A
absurd ()
IsDecidable : {a} {A : Set a} (R : A A Set a) Set a
IsDecidable {a} {A} R = (a₁ a₂ : A) Dec (R a₁ a₂)
record IsSemilattice {a} (A : Set a)
(_≈_ : A A Set a)
(_⊔_ : A A A) : Set a where
_≼_ : A A Set a
a b = Σ A (λ c (a c) b)
_≺_ : A A Set a
a b = (a b) × (¬ a b)
field
≈-equiv : IsEquivalence A _≈_
≈-⊔-cong : {a₁ a₂ a₃ a₄} a₁ a₂ a₃ a₄ (a₁ a₃) (a₂ a₄)
⊔-assoc : (x y z : A) ((x y) z) (x (y z))
⊔-comm : (x y : A) (x y) (y x)
⊔-idemp : (x : A) (x x) x
open IsEquivalence ≈-equiv public
≼-refl : (a : A) a a
≼-refl a = (a , ⊔-idemp a)
≼-cong : {a₁ a₂ a₃ a₄ : A} a₁ a₂ a₃ a₄ a₁ a₃ a₂ a₄
≼-cong a₁≈a₂ a₃≈a₄ (c₁ , a₁⊔c₁≈a₃) = (c₁ , ≈-trans (≈-⊔-cong (≈-sym a₁≈a₂) ≈-refl) (≈-trans a₁⊔c₁≈a₃ a₃≈a₄))
≺-cong : {a₁ a₂ a₃ a₄ : A} a₁ a₂ a₃ a₄ a₁ a₃ a₂ a₄
≺-cong a₁≈a₂ a₃≈a₄ (a₁≼a₃ , a₁̷≈a₃) =
( ≼-cong a₁≈a₂ a₃≈a₄ a₁≼a₃
, λ a₂≈a₄ a₁̷≈a₃ (≈-trans a₁≈a₂ (≈-trans a₂≈a₄ (≈-sym a₃≈a₄)))
)
record IsLattice {a} (A : Set a)
(_≈_ : A A Set a)
(_⊔_ : A A A)
(_⊓_ : A A A) : Set a where
field
joinSemilattice : IsSemilattice A _≈_ _⊔_
meetSemilattice : IsSemilattice A _≈_ _⊓_
absorb-⊔-⊓ : (x y : A) (x (x y)) x
absorb-⊓-⊔ : (x y : A) (x (x y)) x
open IsSemilattice joinSemilattice public
open IsSemilattice meetSemilattice public using () renaming
( ⊔-assoc to ⊓-assoc
; ⊔-comm to ⊓-comm
; ⊔-idemp to ⊓-idemp
; ≈-⊔-cong to ≈-⊓-cong
; _≼_ to _≽_
; _≺_ to _≻_
; ≼-refl to ≽-refl
)
record IsFiniteHeightLattice {a} (A : Set a)
(h : )
(_≈_ : A A Set a)
(_⊔_ : A A A)
(_⊓_ : A A A) : Set (lsuc a) where
field
isLattice : IsLattice A _≈_ _⊔_ _⊓_
fixedHeight : Chain.Height (_≈_) (IsLattice.≈-equiv isLattice) (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice) h
open IsLattice isLattice public
module _ {a b} {A : Set a} {B : Set b}
(_≼₁_ : A A Set a) (_≼₂_ : B B Set b) where
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 _≺₁_; ≈-equiv to ≈₁-equiv; ≺-cong to ≺₁-cong)
open IsSemilattice slB renaming (_≼_ to _≼₂_; _≺_ to _≺₂_; ≈-equiv to ≈₂-equiv; ≺-cong to ≺₂-cong)
open Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong using () renaming (Chain to Chain₁; step to step₁; done to done₁)
open Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; step to step₂; done to done₂)
Chain-map : (f : A B)
Monotonic _≼₁_ _≼₂_ f
Injective _≈₁_ _≈₂_ f
f Preserves _≈₁_ _≈₂_
{a₁ a₂ : A} {n : } Chain₁ a₁ a₂ n Chain₂ (f a₁) (f a₂) n
Chain-map f Monotonicᶠ Injectiveᶠ Preservesᶠ (done₁ a₁≈a₂) =
done₂ (Preservesᶠ a₁≈a₂)
Chain-map f Monotonicᶠ Injectiveᶠ Preservesᶠ (step₁ (a₁≼₁a , a₁̷≈₁a) a≈₁a' a'a₂) =
let fa₁≺₂fa = (Monotonicᶠ a₁≼₁a , λ fa₁≈₂fa a₁̷≈₁a (Injectiveᶠ fa₁≈₂fa))
fa≈fa' = Preservesᶠ a≈₁a'
in step₂ fa₁≺₂fa fa≈fa' (Chain-map f Monotonicᶠ Injectiveᶠ Preservesᶠ a'a₂)
record Semilattice {a} (A : Set a) : Set (lsuc a) where
field
_≈_ : A A Set a
_⊔_ : A A A
isSemilattice : IsSemilattice A _≈_ _⊔_
open IsSemilattice isSemilattice public
record Lattice {a} (A : Set a) : Set (lsuc a) where
field
_≈_ : A A Set a
_⊔_ : A A A
_⊓_ : A A A
isLattice : IsLattice A _≈_ _⊔_ _⊓_
open IsLattice isLattice public
module IsSemilatticeInstances where
module ForNat where
open Nat
open NatProps
open Eq
private
≡-⊔-cong : {a₁ a₂ a₃ a₄} a₁ a₂ a₃ a₄ (a₁ a₃) (a₂ a₄)
≡-⊔-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl
≡-⊓-cong : {a₁ a₂ a₃ a₄} a₁ a₂ a₃ a₄ (a₁ a₃) (a₂ a₄)
≡-⊓-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl
NatIsMaxSemilattice : IsSemilattice _≡_ _⊔_
NatIsMaxSemilattice = record
{ ≈-equiv = record
{ ≈-refl = refl
; ≈-sym = sym
; ≈-trans = trans
}
; ≈-⊔-cong = ≡-⊔-cong
; ⊔-assoc = ⊔-assoc
; ⊔-comm = ⊔-comm
; ⊔-idemp = ⊔-idem
}
NatIsMinSemilattice : IsSemilattice _≡_ _⊓_
NatIsMinSemilattice = record
{ ≈-equiv = record
{ ≈-refl = refl
; ≈-sym = sym
; ≈-trans = trans
}
; ≈-⊔-cong = ≡-⊓-cong
; ⊔-assoc = ⊓-assoc
; ⊔-comm = ⊓-comm
; ⊔-idemp = ⊓-idem
}
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 ForMap {a} {A B : Set a}
(≡-dec-A : Decidable (_≡_ {a} {A}))
(_≈₂_ : B B Set a)
(_⊔₂_ : B B B)
(sB : IsSemilattice B _≈₂_ _⊔₂_) where
open import Map A B ≡-dec-A
open IsSemilattice sB renaming
( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-⊔-cong to ≈₂-⊔₂-cong
; ⊔-assoc to ⊔₂-assoc; ⊔-comm to ⊔₂-comm; ⊔-idemp to ⊔₂-idemp
)
module MapEquiv = IsEquivalenceInstances.ForMap A B ≡-dec-A _≈₂_ (IsSemilattice.≈-equiv sB)
open MapEquiv using (_≈_) public
infixl 20 _⊔_
infixl 20 _⊓_
_⊔_ : Map Map Map
m₁ m₂ = union _⊔₂_ m₁ m₂
_⊓_ : Map Map Map
m₁ m₂ = intersect _⊔₂_ m₁ m₂
MapIsUnionSemilattice : IsSemilattice Map _≈_ _⊔_
MapIsUnionSemilattice = record
{ ≈-equiv = MapEquiv.LiftEquivalence
; ≈-⊔-cong = λ {m₁} {m₂} {m₃} {m₄} union-cong _≈₂_ _⊔₂_ ≈₂-⊔₂-cong {m₁} {m₂} {m₃} {m₄}
; ⊔-assoc = union-assoc _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-assoc
; ⊔-comm = union-comm _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-comm
; ⊔-idemp = union-idemp _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-idemp
}
MapIsIntersectSemilattice : IsSemilattice Map _≈_ _⊓_
MapIsIntersectSemilattice = record
{ ≈-equiv = MapEquiv.LiftEquivalence
; ≈-⊔-cong = λ {m₁} {m₂} {m₃} {m₄} intersect-cong _≈₂_ _⊔₂_ ≈₂-⊔₂-cong {m₁} {m₂} {m₃} {m₄}
; ⊔-assoc = intersect-assoc _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-assoc
; ⊔-comm = intersect-comm _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-comm
; ⊔-idemp = intersect-idemp _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-idemp
}
module IsLatticeInstances where
module ForNat where
open Nat
open NatProps
open Eq
open IsSemilatticeInstances.ForNat
open Data.Product
private
max-bound₁ : {x y z : } x y z x z
max-bound₁ {x} {y} {z} x⊔y≡z
rewrite sym x⊔y≡z
rewrite ⊔-comm x y = m≤n⇒m≤o⊔n y (≤-refl)
min-bound₁ : {x y z : } x y z z x
min-bound₁ {x} {y} {z} x⊓y≡z
rewrite sym x⊓y≡z = m≤n⇒m⊓o≤n y (≤-refl)
minmax-absorb : {x y : } x (x y) x
minmax-absorb {x} {y} = ≤-antisym x⊓x⊔y≤x (helper x⊓x≤x⊓x⊔y (⊓-idem x))
where
x⊓x⊔y≤x = min-bound₁ {x} {x y} {x (x y)} refl
x⊓x≤x⊓x⊔y = ⊓-mono-≤ {x} {x} ≤-refl (max-bound₁ {x} {y} {x y} refl)
-- >:(
helper : x x x (x y) x x x x x (x y)
helper x⊓x≤x⊓x⊔y x⊓x≡x rewrite x⊓x≡x = x⊓x≤x⊓x⊔y
maxmin-absorb : {x y : } x (x y) x
maxmin-absorb {x} {y} = ≤-antisym (helper x⊔x⊓y≤x⊔x (⊔-idem x)) x≤x⊔x⊓y
where
x≤x⊔x⊓y = max-bound₁ {x} {x y} {x (x y)} refl
x⊔x⊓y≤x⊔x = ⊔-mono-≤ {x} {x} ≤-refl (min-bound₁ {x} {y} {x y} refl)
-- >:(
helper : x (x y) x x x x x x (x y) x
helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x
NatIsLattice : IsLattice _≡_ _⊔_ _⊓_
NatIsLattice = record
{ joinSemilattice = NatIsMaxSemilattice
; meetSemilattice = NatIsMinSemilattice
; absorb-⊔-⊓ = λ x y maxmin-absorb {x} {y}
; absorb-⊓-⊔ = λ x y minmax-absorb {x} {y}
}
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 ForMap {a} {A B : Set a}
(≡-dec-A : Decidable (_≡_ {a} {A}))
(_≈₂_ : B B Set a)
(_⊔₂_ : B B B)
(_⊓₂_ : B B B)
(lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
open import Map A B ≡-dec-A
open IsLattice lB renaming
( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym
; ⊔-idemp to ⊔₂-idemp; ⊓-idemp to ⊓₂-idemp
; absorb-⊔-⊓ to absorb-⊔₂-⊓₂; absorb-⊓-⊔ to absorb-⊓₂-⊔₂
)
module MapJoin = IsSemilatticeInstances.ForMap ≡-dec-A _≈₂_ _⊔₂_ (IsLattice.joinSemilattice lB)
open MapJoin using (_⊔_; _≈_) public
module MapMeet = IsSemilatticeInstances.ForMap ≡-dec-A _≈₂_ _⊓₂_ (IsLattice.meetSemilattice lB)
open MapMeet using (_⊓_) public
MapIsLattice : IsLattice Map _≈_ _⊔_ _⊓_
MapIsLattice = record
{ joinSemilattice = MapJoin.MapIsUnionSemilattice
; meetSemilattice = MapMeet.MapIsIntersectSemilattice
; 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)
(≈₁-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₂))
)
}