From 5420bb808e9b87eabeb43f98f6011a65ba4f714e Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 11 Feb 2024 21:16:41 -0800 Subject: [PATCH] Expose bundles from 'Prod' Signed-off-by: Danila Fedorin --- Lattice/Prod.agda | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/Lattice/Prod.agda b/Lattice/Prod.agda index 95a901f..0663eb5 100644 --- a/Lattice/Prod.agda +++ b/Lattice/Prod.agda @@ -94,6 +94,13 @@ isLattice = record ) } +lattice : Lattice (A × B) +lattice = record + { _≈_ = _≈_ + ; _⊔_ = _⊔_ + ; _⊓_ = _⊓_ + ; isLattice = isLattice + } module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) where ≈-dec : IsDecidable _≈_ @@ -176,3 +183,12 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) in ≤-trans n≤n₁+n₂ (+-mono-≤ (proj₂ fhA a₁a₂) (proj₂ fhB b₁b₂)) ) } + + finiteHeightLattice : FiniteHeightLattice (A × B) + finiteHeightLattice = record + { height = h₁ + h₂ + ; _≈_ = _≈_ + ; _⊔_ = _⊔_ + ; _⊓_ = _⊓_ + ; isFiniteHeightLattice = isFiniteHeightLattice + }