From 845a8a2236d3846a4d4757150917437b3877c23f Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 23 Sep 2023 15:06:43 -0700
Subject: [PATCH] Move the Map into Lattice/Map

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Equivalence.agda             | 2 +-
 Lattice.agda                 | 4 ++--
 Map.agda => Lattice/Map.agda | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)
 rename Map.agda => Lattice/Map.agda (99%)

diff --git a/Equivalence.agda b/Equivalence.agda
index 327b9bd..edac885 100644
--- a/Equivalence.agda
+++ b/Equivalence.agda
@@ -41,7 +41,7 @@ module IsEquivalenceInstances where
         (_≈₂_ : B → B → Set b)
         (eB : IsEquivalence B _≈₂_) where
 
-        open import Map A B ≡-dec-A using (Map; lift; subset)
+        open import Lattice.Map A B ≡-dec-A using (Map; lift; subset)
         open import Data.List using (_∷_; []) -- TODO: re-export these with nicer names from map
 
         open IsEquivalence eB renaming
diff --git a/Lattice.agda b/Lattice.agda
index b49afd8..03b61b6 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -221,7 +221,7 @@ module IsSemilatticeInstances where
         (_⊔₂_ : B → B → B)
         (sB : IsSemilattice B _≈₂_ _⊔₂_) where
 
-        open import Map A B ≡-dec-A
+        open import Lattice.Map A B ≡-dec-A
         open IsSemilattice sB renaming
             ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-⊔-cong to ≈₂-⊔₂-cong
             ; ⊔-assoc to ⊔₂-assoc; ⊔-comm to ⊔₂-comm; ⊔-idemp to ⊔₂-idemp
@@ -336,7 +336,7 @@ module IsLatticeInstances where
         (_⊓₂_ : B → B → B)
         (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
-        open import Map A B ≡-dec-A
+        open import Lattice.Map A B ≡-dec-A
         open IsLattice lB renaming
             ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym
             ; ⊔-idemp to ⊔₂-idemp; ⊓-idemp to ⊓₂-idemp
diff --git a/Map.agda b/Lattice/Map.agda
similarity index 99%
rename from Map.agda
rename to Lattice/Map.agda
index 3cf083e..d7b79ee 100644
--- a/Map.agda
+++ b/Lattice/Map.agda
@@ -4,7 +4,7 @@ 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 Map {a b : Level} (A : Set a) (B : Set b)
+module Lattice.Map {a b : Level} (A : Set a) (B : Set b)
     (≡-dec-A : Decidable (_≡_ {a} {A}))
     where