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

Expose bundles from FiniteValueMap

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

9
Isomorphism.agda
View File

@ -60,3 +60,12 @@ module TransportFiniteHeight
{ isLattice = lB { isLattice = lB
; fixedHeight = (((f a₁ , f a₂), portChain₁ c) , λ c' → bounded₁ (portChain₂ c')) ; fixedHeight = (((f a₁ , f a₂), portChain₁ c) , λ c' → bounded₁ (portChain₂ c'))
} }
finiteHeightLattice : FiniteHeightLattice B
finiteHeightLattice = record
{ height = height
; _≈_ = _≈₂_
; _⊔_ = _⊔₂_
; _⊓_ = _⊓₂_
; isFiniteHeightLattice = isFiniteHeightLattice
}

2
Lattice/FiniteValueMap.agda
View File

@ -271,4 +271,4 @@ module IterProdIsomorphism where
(to-preserves-≈ uks) (from-preserves-≈ {ks}) (to-preserves-≈ uks) (from-preserves-≈ {ks})
(to-⊔-distr uks) (from-⊔-distr {ks}) (to-⊔-distr uks) (from-⊔-distr {ks})
(from-to-inverseʳ uks) (from-to-inverseˡ uks) (from-to-inverseʳ uks) (from-to-inverseˡ uks)
using (isFiniteHeightLattice) public using (isFiniteHeightLattice; finiteHeightLattice) public