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

Tweak IterProd to expose more (including a bundle)

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-02-11 20:45:14 -08:00
parent 45f2babfa3
commit a920608bef
1 changed files with 19 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
Lattice/IterProd.agda
View File

@ -47,6 +47,9 @@ private module _ where
_⊓₁_ (Lattice._⊓_ Right) _⊓₁_ (Lattice._⊓_ Right)
lA (Lattice.isLattice Right) lA (Lattice.isLattice Right)
module _ (k : ℕ) where
open Lattice.Lattice (IterProdLattice {k}) public
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
@ -81,9 +84,9 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
IterProdFiniteHeightLattice {0} = BFiniteHeightLattice IterProdFiniteHeightLattice {0} = BFiniteHeightLattice
IterProdFiniteHeightLattice {suc k'} = record IterProdFiniteHeightLattice {suc k'} = record
{ height = h₁ + FiniteHeightAndDecEq.height Right { height = h₁ + FiniteHeightAndDecEq.height Right
; _≈_ = _≈_ ; _≈_ = P._≈_
; _⊔_ = _⊔_ ; _⊔_ = P._⊔_
; _⊓_ = _⊓_ ; _⊓_ = P._⊓_
; isFiniteHeightLattice = isFiniteHeightLattice ; isFiniteHeightLattice = isFiniteHeightLattice
≈₁-dec (FiniteHeightAndDecEq.≈-dec Right) ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
h₁ (FiniteHeightAndDecEq.height Right) h₁ (FiniteHeightAndDecEq.height Right)
@ -97,11 +100,19 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
_≈₁_ (FiniteHeightAndDecEq._≈_ Right) _≈₁_ (FiniteHeightAndDecEq._≈_ Right)
_⊔₁_ (FiniteHeightAndDecEq._⊔_ Right) _⊔₁_ (FiniteHeightAndDecEq._⊔_ Right)
_⊓₁_ (FiniteHeightAndDecEq._⊓_ Right) _⊓₁_ (FiniteHeightAndDecEq._⊓_ Right)
lA (FiniteHeightAndDecEq.isLattice Right) lA (FiniteHeightAndDecEq.isLattice Right) as P
module _ (k : ℕ) where module _ (k : ℕ) where
open FiniteHeightAndDecEq (IterProdFiniteHeightLattice {k}) using (fixedHeight) public open FiniteHeightAndDecEq (IterProdFiniteHeightLattice {k}) using (isFiniteHeightLattice) public
-- Expose the computed definition in public. private
module _ (k : ℕ) where FHD = IterProdFiniteHeightLattice {k}
open Lattice.Lattice (IterProdLattice {k}) public
finiteHeightLattice : FiniteHeightLattice (IterProd k)
finiteHeightLattice = record
{ height = FiniteHeightAndDecEq.height FHD
; _≈_ = FiniteHeightAndDecEq._≈_ FHD
; _⊔_ = FiniteHeightAndDecEq._⊔_ FHD
; _⊓_ = FiniteHeightAndDecEq._⊓_ FHD
; isFiniteHeightLattice = isFiniteHeightLattice
}