From 3c346dcd154e2953a695f56f29a1d63f9797c15a Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 23 Sep 2023 17:12:12 -0700
Subject: [PATCH] Add a 'set' lattice backed by maps

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/Map.agda    |  4 +---
 Lattice/MapSet.agda | 19 +++++++++++++++++++
 Lattice/Unit.agda   |  2 +-
 3 files changed, 21 insertions(+), 4 deletions(-)
 create mode 100644 Lattice/MapSet.agda

diff --git a/Lattice/Map.agda b/Lattice/Map.agda
index d89dd97..88e82aa 100644
--- a/Lattice/Map.agda
+++ b/Lattice/Map.agda
@@ -1,8 +1,6 @@
 open import Lattice
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Binary.Core using (Rel)
-open import Relation.Nullary using (Dec; yes; no; Reflects; ofʸ; ofⁿ)
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 
 module Lattice.Map {a b : Level} (A : Set a) (B : Set b)
@@ -13,7 +11,7 @@ module Lattice.Map {a b : Level} (A : Set a) (B : Set b)
 
 import Data.List.Membership.Propositional as MemProp
 
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Data.Nat using (ℕ)
 open import Data.List using (List; map; []; _∷_; _++_)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
diff --git a/Lattice/MapSet.agda b/Lattice/MapSet.agda
new file mode 100644
index 0000000..37b9e2c
--- /dev/null
+++ b/Lattice/MapSet.agda
@@ -0,0 +1,19 @@
+open import Lattice
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
+open import Relation.Binary.Definitions using (Decidable)
+open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
+
+module Lattice.MapSet {a : Level} (A : Set a) (≡-dec-A : Decidable (_≡_ {a} {A})) where
+
+open import Lattice.Unit using (⊤) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice)
+import Lattice.Map
+
+private module UnitMap = Lattice.Map A ⊤ _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A ⊤-isLattice
+open UnitMap using (Map)
+open UnitMap using
+    ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_
+    ; isUnionSemilattice; isIntersectSemilattice; isLattice
+    ) public
+
+MapSet : Set a
+MapSet = Map
diff --git a/Lattice/Unit.agda b/Lattice/Unit.agda
index 4c58592..5fb4809 100644
--- a/Lattice/Unit.agda
+++ b/Lattice/Unit.agda
@@ -3,7 +3,7 @@ module Lattice.Unit where
 open import Data.Empty using (⊥-elim)
 open import Data.Product using (_,_)
 open import Data.Nat using (ℕ; _≤_; z≤n)
-open import Data.Unit using (⊤; tt)
+open import Data.Unit using (⊤; tt) public
 open import Data.Unit.Properties using (_≟_; ≡-setoid)
 open import Relation.Binary using (Setoid)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_)