Prove that maps are functional assuming uniqueness

2023-07-23 17:50:25 -07:00
parent ab7ed2039a
commit d9c18fe483
2 changed files with 33 additions and 11 deletions
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -76,7 +76,6 @@ module IsEquivalenceInstances where

        open import Map A B ≡-dec-A using (Map; lift; subset; insert)
        open import Data.List using (_∷_; []) -- TODO: re-export these with nicer names from map
-        open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map

        open IsEquivalence eB renaming
            ( ≈-refl to ≈₂-refl