2024-03-01 21:58:58 -08:00
|
|
|
|
open import Relation.Binary.PropositionalEquality using (_≡_)
|
|
|
|
|
|
open import Relation.Binary.Definitions using (Decidable)
|
|
|
|
|
|
|
|
|
|
|
|
module Lattice.Bundles.FiniteValueMap (A B : Set) (≡-dec-A : Decidable (_≡_ {_} {A})) where
|
|
|
|
|
|
|
|
|
|
|
|
open import Lattice
|
|
|
|
|
|
open import Data.List using (List)
|
|
|
|
|
|
open import Data.Nat using (ℕ)
|
|
|
|
|
|
open import Utils using (Unique)
|
|
|
|
|
|
|
|
|
|
|
|
module _ (fhB : FiniteHeightLattice B) where
|
|
|
|
|
|
open Lattice.FiniteHeightLattice fhB using () renaming
|
|
|
|
|
|
( _≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_
|
|
|
|
|
|
; height to height₂
|
|
|
|
|
|
; isLattice to isLattice₂
|
|
|
|
|
|
; fixedHeight to fixedHeight₂
|
|
|
|
|
|
)
|
|
|
|
|
|
|
|
|
|
|
|
module _ {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) where
|
|
|
|
|
|
import Lattice.FiniteValueMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂ as FVM
|
|
|
|
|
|
|
2024-03-09 13:59:22 -08:00
|
|
|
|
FiniteHeightType = FVM.FiniteMap ks
|
|
|
|
|
|
|
|
|
|
|
|
finiteHeightLattice = FVM.IterProdIsomorphism.finiteHeightLattice uks ≈₂-dec height₂ fixedHeight₂
|
|
|
|
|
|
open FiniteHeightLattice finiteHeightLattice public
|
2024-03-01 23:27:49 -08:00
|
|
|
|
|
|
|
|
|
|
≈-dec = FVM.≈-dec ks ≈₂-dec
|
|
|
|
|
|
|
