From 97a4165b5850993e58d89bbb29891625dfb8a93f Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 1 Mar 2024 21:35:40 -0800 Subject: [PATCH] Expose bundles from FiniteValueMap Signed-off-by: Danila Fedorin --- Isomorphism.agda | 9 +++++++++ Lattice/FiniteValueMap.agda | 2 +- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/Isomorphism.agda b/Isomorphism.agda index 59e37ff..454bf93 100644 --- a/Isomorphism.agda +++ b/Isomorphism.agda @@ -60,3 +60,12 @@ module TransportFiniteHeight { isLattice = lB ; fixedHeight = (((f a₁ , f a₂), portChain₁ c) , λ c' → bounded₁ (portChain₂ c')) } + + finiteHeightLattice : FiniteHeightLattice B + finiteHeightLattice = record + { height = height + ; _≈_ = _≈₂_ + ; _⊔_ = _⊔₂_ + ; _⊓_ = _⊓₂_ + ; isFiniteHeightLattice = isFiniteHeightLattice + } diff --git a/Lattice/FiniteValueMap.agda b/Lattice/FiniteValueMap.agda index d5eb4d1..a62184e 100644 --- a/Lattice/FiniteValueMap.agda +++ b/Lattice/FiniteValueMap.agda @@ -271,4 +271,4 @@ module IterProdIsomorphism where (to-preserves-≈ uks) (from-preserves-≈ {ks}) (to-⊔-distr uks) (from-⊔-distr {ks}) (from-to-inverseʳ uks) (from-to-inverseˡ uks) - using (isFiniteHeightLattice) public + using (isFiniteHeightLattice; finiteHeightLattice) public