From e89418d600417dfa0c72d9675a1b8dd004cf0358 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 11 Feb 2024 21:12:49 -0800
Subject: [PATCH] Expose bundle form 'Map'

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/Map.agda | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/Lattice/Map.agda b/Lattice/Map.agda
index 980fe4e..4db7709 100644
--- a/Lattice/Map.agda
+++ b/Lattice/Map.agda
@@ -882,6 +882,14 @@ isLattice = record
     ; absorb-⊓-⊔ = absorb-⊓-⊔
     }
 
+lattice : Lattice Map
+lattice = record
+    { _≈_ = _≈_
+    ; _⊔_ = _⊔_
+    ; _⊓_ = _⊓_
+    ; isLattice = isLattice
+    }
+
 ⊔-equal-keys : ∀ {m₁ m₂ : Map} → keys m₁ ≡ keys m₂ → keys m₁ ≡ keys (m₁ ⊔ m₂)
 ⊔-equal-keys km₁≡km₂ = union-equal-keys km₁≡km₂