DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Restore bundles in IterProd

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-03-01 21:12:22 -08:00
parent ae09a27f64
commit 754714d770
1 changed files with 17 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
Lattice/IterProd.agda
View File

@ -98,6 +98,14 @@ module _ (k : ℕ) where
open Everything (everything k) using (_≈_; _⊔_; _⊓_; isLattice) public open Everything (everything k) using (_≈_; _⊔_; _⊓_; isLattice) public
open Lattice.IsLattice isLattice public open Lattice.IsLattice isLattice public
lattice : Lattice (IterProd k)
lattice = record
{ _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = isLattice
}
module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
(h₁ h₂ : ℕ) (h₁ h₂ : ℕ)
(fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
@ -117,3 +125,12 @@ module _ (k : ℕ) where
{ isLattice = isLattice { isLattice = isLattice
; fixedHeight = IsFiniteHeightAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required) ; fixedHeight = IsFiniteHeightAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
} }
finiteHeightLattice : FiniteHeightLattice (IterProd k)
finiteHeightLattice = record
{ height = IsFiniteHeightAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
; _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isFiniteHeightLattice = isFiniteHeightLattice
}