diff --git a/Makefile b/Makefile
index 0d15fe66..edc095a2 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,4 @@
-.PHONY : install agda repl libHtml test testHtml golden docs
+.PHONY : install agda repl libHtml test testContainers testHtml golden docs
 FILES = $(shell find src -type f)
 
 install :
@@ -17,7 +17,10 @@ libHtml :
 test/agda2hs : $(FILES)
 	cabal install agda2hs --overwrite-policy=always --installdir=test --install-method=copy
 
-test : test/agda2hs
+testContainers:
+	cd ./lib/containers && ./generate-haskell.sh && cabal build containers-prop
+
+test : test/agda2hs testContainers
 	make -C test
 
 testHtml : test/agda2hs
diff --git a/cabal.project b/cabal.project
index bfe5b80c..cbfef8ca 100644
--- a/cabal.project
+++ b/cabal.project
@@ -1,3 +1,5 @@
-packages: ./agda2hs.cabal
-constraints: Agda +debug
+packages:
+  ./agda2hs.cabal
+  ./lib/containers/containers-prop.cabal
 
+constraints: Agda +debug
diff --git a/lib/containers/CHANGELOG.md b/lib/containers/CHANGELOG.md
new file mode 100644
index 00000000..5f45c534
--- /dev/null
+++ b/lib/containers/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Revision history for containers-prop
+
+## 0.8.0.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.
diff --git a/lib/containers/README.md b/lib/containers/README.md
new file mode 100644
index 00000000..8bfeb4c0
--- /dev/null
+++ b/lib/containers/README.md
@@ -0,0 +1,14 @@
+`containers.agda-lib` proves properties about the Haskell [containers][] library.
+
+
+## Roadmap
+
+For the time being, this library is developed as part of the [agda2hs][] repository. There are two reasons:
+
+* Significant backflow of code from `containers.agda-lib` to `base.agda-lib`. For example, proving properties about `Data.Map.spanAntitone` will require additions to `Data.Ord`.
+* Informs the development of [agda2hs][]: changes to `agda2hs` are immediately confronted with the fact that there is at least one separate library of considerable size.
+
+However, once [agda2hs][] has become sufficiently complete and stable, we want to move `containers.agda-lib` into a separate repository.
+
+  [agda2hs]: https://github.com/agda/agda2hs
+  [containers]: https://hackage.haskell.org/package/containers
diff --git a/lib/containers/agda/Data/Map.agda b/lib/containers/agda/Data/Map.agda
new file mode 100644
index 00000000..345aaf33
--- /dev/null
+++ b/lib/containers/agda/Data/Map.agda
@@ -0,0 +1,4 @@
+module Data.Map where
+
+open import Haskell.Data.Map public
+open import Data.Map.Prop public
diff --git a/lib/containers/agda/Data/Map/Maybe.agda b/lib/containers/agda/Data/Map/Maybe.agda
new file mode 100644
index 00000000..8e194e04
--- /dev/null
+++ b/lib/containers/agda/Data/Map/Maybe.agda
@@ -0,0 +1,221 @@
+
+module Data.Map.Maybe
+    {-
+    This module adds functions for the 'Maybe' type
+    that are analogous to the functions in 'Data.Map'.
+    This is used to make proofs for 'Data.Map' more transparent.
+    -} where
+
+open import Haskell.Law.Equality
+open import Haskell.Prelude hiding (null; map; filter)
+
+open import Haskell.Data.Maybe using
+    ( isJust
+    )
+
+{-----------------------------------------------------------------------------
+    Data.Maybe
+    Functions
+------------------------------------------------------------------------------}
+
+null : Maybe a → Bool
+null Nothing = True
+null (Just x) = False
+
+update : (a → Maybe a) → Maybe a → Maybe a
+update f Nothing = Nothing
+update f (Just x) = f x
+
+filter : (a → Bool) → Maybe a → Maybe a
+filter p Nothing = Nothing
+filter p (Just x) = if p x then Just x else Nothing
+
+-- | Degenerate 'filter', does not look at the contents.
+-- Similar to 'guard'.
+filt : Bool → Maybe a → Maybe a
+filt True m = m
+filt False m = Nothing
+
+mapMaybe : (a → Maybe b) → Maybe a → Maybe b
+mapMaybe f Nothing = Nothing
+mapMaybe f (Just x) = f x
+
+unionWith : (a → a → a) → Maybe a → Maybe a → Maybe a
+unionWith f Nothing my = my
+unionWith f (Just x) Nothing = Just x
+unionWith f (Just x) (Just y) = Just (f x y)
+
+-- | Left-biased union.
+union : Maybe a → Maybe a → Maybe a
+union = unionWith (λ x y → x)
+
+intersectionWith : (a → b → c) → Maybe a → Maybe b → Maybe c
+intersectionWith f (Just x) (Just y) = Just (f x y)
+intersectionWith _ _ _ = Nothing
+
+disjoint : Maybe a → Maybe b → Bool
+disjoint m = null ∘ intersectionWith const m
+
+{-----------------------------------------------------------------------------
+    Properties
+    union
+------------------------------------------------------------------------------}
+
+--
+prop-union-empty-right
+  : ∀ {ma : Maybe a}
+  → union ma Nothing ≡ ma
+--
+prop-union-empty-right {_} {Nothing} = refl
+prop-union-empty-right {_} {Just x} = refl
+
+-- | 'unionWith' is symmetric if we 'flip' the function.
+-- Note that 'union' is left-biased, not symmetric.
+--
+prop-unionWith-sym
+  : ∀ {f : a → a → a} {ma mb : Maybe a}
+  → unionWith f ma mb ≡ unionWith (flip f) mb ma
+--
+prop-unionWith-sym {_} {f} {Nothing} {Nothing} = refl
+prop-unionWith-sym {_} {f} {Just x}  {Nothing} = refl
+prop-unionWith-sym {_} {f} {Nothing} {Just y} = refl
+prop-unionWith-sym {_} {f} {Just x}  {Just y} = refl
+
+--
+prop-union-assoc
+  : ∀ {ma mb mc : Maybe a}
+  → union (union ma mb) mc ≡ union ma (union mb mc)
+--
+prop-union-assoc {_} {Nothing} {mb} {mc} = refl
+prop-union-assoc {_} {Just x} {Nothing} {mc} = refl
+prop-union-assoc {_} {Just x} {Just y} {Nothing} = refl
+prop-union-assoc {_} {Just x} {Just y} {Just z} = refl
+
+-- | 'union' is symmetric if at most one argument is 'Just'.
+--
+prop-union-sym
+  : ∀ {ma mb : Maybe a}
+  → disjoint ma mb ≡ True
+  → union ma mb ≡ union mb ma
+--
+prop-union-sym {_} {Nothing} {Nothing} eq = refl
+prop-union-sym {_} {Nothing} {Just x} eq = refl
+prop-union-sym {_} {Just x} {Nothing} eq = refl
+
+--
+prop-union-left
+  : ∀ (x : a) (mb : Maybe a)
+  → union (Just x) mb ≡ Just x
+--
+prop-union-left x Nothing = refl
+prop-union-left x (Just y) = refl
+
+{-----------------------------------------------------------------------------
+    Properties
+    intersection
+------------------------------------------------------------------------------}
+--
+prop-isJust-intersectionWith
+  : ∀ {ma : Maybe a} {mb : Maybe b} {f : a → b → c}
+  → isJust (intersectionWith f ma mb)
+    ≡ (isJust ma && isJust mb)
+--
+prop-isJust-intersectionWith {_} {_} {_} {Nothing} = refl
+prop-isJust-intersectionWith {_} {_} {_} {Just x} {Nothing} = refl
+prop-isJust-intersectionWith {_} {_} {_} {Just x} {Just y} = refl
+
+{-----------------------------------------------------------------------------
+    Properties
+    filter
+------------------------------------------------------------------------------}
+-- |
+-- Since 'union' is left-biased,
+-- filtering commutes with union if the predicate is constant.
+--
+-- If the predicate is not constant, there are counterexamples.
+prop-filter-union
+  : ∀ (p : a → Bool) {m1 m2 : Maybe a}
+  → (∀ (x y : a) → p x ≡ p y)
+  → filter p (union m1 m2)
+    ≡ union (filter p m1) (filter p m2)
+--
+prop-filter-union p {Nothing} {m2} flat = refl
+prop-filter-union p {Just x} {Nothing} flat
+  with p x
+... | True = refl
+... | False = refl
+prop-filter-union p {Just x} {Just y} flat
+  rewrite flat x y
+  with p y
+... | True = refl
+... | False = refl
+
+--
+@0 prop-filter-||
+  : ∀ {ma : Maybe a} {p q : a → Bool}
+  → filter (λ x → p x || q x) ma
+    ≡ union (filter p ma) (filter q ma)
+--
+prop-filter-|| {_} {Nothing} {p} {q} = refl
+prop-filter-|| {_} {Just x} {p} {q}
+  with p x | q x
+... | True  | True  = refl
+... | True  | False = refl
+... | False | True  = refl
+... | False | False = refl
+
+-- |
+-- 'filt' is a special case of 'filter'.
+prop-filter-filt
+  : ∀ (b : Bool) (m : Maybe a)
+  → filter (λ x → b) m
+    ≡ filt b m
+--
+prop-filter-filt False Nothing = refl
+prop-filter-filt True Nothing = refl
+prop-filter-filt False (Just x) = refl
+prop-filter-filt True (Just x) = refl
+
+{-----------------------------------------------------------------------------
+    Properties
+    filt
+------------------------------------------------------------------------------}
+-- |
+-- Since 'union' is left-biased,
+-- filtering commutes with union if the predicate is constant.
+--
+-- If the predicate is not constant, there are counterexamples.
+prop-filt-||
+  : ∀ (x y : Bool) {m : Maybe a}
+  → filt (x || y) m
+    ≡ union (filt x m) (filt y m)
+--
+prop-filt-|| False y {Nothing} = refl
+prop-filt-|| False y {Just x} = refl
+prop-filt-|| True False {Nothing} = refl
+prop-filt-|| True False {Just x} = refl
+prop-filt-|| True True {Nothing} = refl
+prop-filt-|| True True {Just x} = refl
+
+--
+prop-filt-union
+  : ∀ (x : Bool) {m1 m2 : Maybe a}
+  → filt x (union m1 m2)
+    ≡ union (filt x m1) (filt x m2)
+--
+prop-filt-union False {Nothing} {m2} = refl
+prop-filt-union True {Nothing} {m2} = refl
+prop-filt-union False {Just y} {Nothing} = refl
+prop-filt-union True {Just y} {Nothing} = refl
+prop-filt-union False {Just y} {Just z} = refl
+prop-filt-union True {Just y} {Just z} = refl
+
+--
+prop-filt-filt
+  : ∀ (x y : Bool) (m : Maybe a)
+  → filt x (filt y m) ≡ filt (x && y) m
+--
+prop-filt-filt False False m = refl
+prop-filt-filt False True m = refl
+prop-filt-filt True False m = refl
+prop-filt-filt True True m = refl
diff --git a/lib/containers/agda/Data/Map/Prop.agda b/lib/containers/agda/Data/Map/Prop.agda
new file mode 100644
index 00000000..13f7788f
--- /dev/null
+++ b/lib/containers/agda/Data/Map/Prop.agda
@@ -0,0 +1,695 @@
+
+-- | Proofs on 'Map'.
+module Data.Map.Prop where
+
+open import Haskell.Law.Bool
+open import Haskell.Law.Equality
+open import Haskell.Prelude hiding (lookup; null; map; filter)
+
+open import Haskell.Data.Map
+open import Haskell.Data.Maybe using
+    ( isJust
+    )
+
+import Data.Map.Maybe as Maybe
+import Haskell.Prelude as List using (map)
+open import Data.Set using (Set)
+import Data.Set as Set
+
+{-----------------------------------------------------------------------------
+    Proofs
+    involving 1 value type
+------------------------------------------------------------------------------}
+module _ {k a : Type} {{_ : Ord k}} where
+
+  --
+  prop-member-null
+    : ∀ (m : Map k a)
+        (_ : ∀ (key : k) → member key m ≡ False)
+    → null m ≡ True
+  --
+  prop-member-null m f = prop-lookup-null m (λ key → lem-isJust (f key))
+    where
+      lem-isJust
+        : ∀ {x : Maybe a} → isJust x ≡ False → x ≡ Nothing
+      lem-isJust {Nothing} refl = refl
+
+  --
+  prop-null-empty
+    : null (empty {k} {a}) ≡ True
+  --
+  prop-null-empty =
+    prop-member-null
+      (empty {k} {a})
+      (λ key → cong isJust (prop-lookup-empty key))
+
+  --
+  prop-lookup-singleton
+    : ∀ (key keyi : k) (x : a)
+    → lookup key (singleton keyi x)
+      ≡ (if (key == keyi) then Just x else Nothing)
+  --
+  prop-lookup-singleton key keyi x =
+    begin
+      lookup key (singleton keyi x)
+    ≡⟨⟩
+      lookup key (insert keyi x empty)
+    ≡⟨ prop-lookup-insert key keyi x empty ⟩
+      (if (key == keyi) then Just x else lookup key empty)
+    ≡⟨ cong (λ f → if (key == keyi) then Just x else f) (prop-lookup-empty key) ⟩
+      (if (key == keyi) then Just x else Nothing)
+    ∎
+
+  --
+  prop-lookup-union
+    : ∀ (key : k) (m n : Map k a)
+    → lookup key (union m n)
+      ≡ Maybe.union (lookup key m) (lookup key n)
+  --
+  prop-lookup-union key m n = prop-lookup-unionWith key (λ x y → x) m n
+
+  --
+  prop-union-empty-left
+    : ∀ {ma : Map k a}
+    → union empty ma ≡ ma
+  --
+  prop-union-empty-left {ma} = prop-equality eq-key
+    where
+      eq-key = λ key →
+        begin
+          lookup key (union empty ma)
+        ≡⟨ prop-lookup-union key empty ma ⟩
+          Maybe.union (lookup key empty) (lookup key ma)
+        ≡⟨ cong (λ o → Maybe.union o (lookup key ma)) (prop-lookup-empty key) ⟩
+          Maybe.union Nothing (lookup key ma)
+        ≡⟨⟩
+          lookup key ma
+        ∎
+
+  --
+  prop-union-empty-right
+    : ∀ {ma : Map k a}
+    → union ma empty ≡ ma
+  --
+  prop-union-empty-right {ma} = prop-equality eq-key
+    where
+      eq-key = λ key →
+        begin
+          lookup key (union ma empty)
+        ≡⟨ prop-lookup-union key ma empty ⟩
+          Maybe.union (lookup key ma) (lookup key empty)
+        ≡⟨ cong (λ o → Maybe.union (lookup key ma) o) (prop-lookup-empty key) ⟩
+          Maybe.union (lookup key ma) Nothing
+        ≡⟨ Maybe.prop-union-empty-right ⟩
+          lookup key ma
+        ∎
+
+  --
+  prop-unionWith-sym
+    : ∀ {f : a → a → a} {ma mb : Map k a}
+    → unionWith f ma mb ≡ unionWith (flip f) mb ma
+  --
+  prop-unionWith-sym {f} {ma} {mb} = prop-equality eq-key
+    where
+      eq-key = λ key →
+        begin
+          lookup key (unionWith f ma mb)
+        ≡⟨ prop-lookup-unionWith key f _ _ ⟩
+          Maybe.unionWith f (lookup key ma) (lookup key mb)
+        ≡⟨ Maybe.prop-unionWith-sym {_} {f} {lookup key ma} {lookup key mb} ⟩
+          Maybe.unionWith (flip f) (lookup key mb) (lookup key ma)
+        ≡⟨ sym (prop-lookup-unionWith key (flip f) _ _) ⟩
+          lookup key (unionWith (flip f) mb ma)
+        ∎
+
+  --
+  prop-union-sym
+    : ∀ {ma mb : Map k a}
+    → disjoint ma mb ≡ True
+    → union ma mb ≡ union mb ma
+  --
+  prop-union-sym {ma} {mb} cond = prop-equality eq-key
+    where
+      lem1 : intersection ma mb ≡ empty
+      lem1 = prop-null→empty (intersection ma mb) cond
+
+      lem-disjoint = λ key →
+        begin
+          Maybe.disjoint (lookup key ma) (lookup key mb)
+        ≡⟨⟩
+          Maybe.null (Maybe.intersectionWith const (lookup key ma) (lookup key mb))
+        ≡⟨ cong Maybe.null (sym (prop-lookup-intersection key ma mb)) ⟩
+          Maybe.null (lookup key (intersection ma mb))
+        ≡⟨ cong (λ o → Maybe.null (lookup key o)) lem1 ⟩
+          Maybe.null (lookup key empty)
+        ≡⟨ cong Maybe.null (prop-lookup-empty key) ⟩
+          True
+        ∎
+
+      eq-key = λ key →
+        begin
+          lookup key (union ma mb)
+        ≡⟨ prop-lookup-unionWith key const _ _ ⟩
+          Maybe.union (lookup key ma) (lookup key mb)
+        ≡⟨ Maybe.prop-union-sym {_} {lookup key ma} {lookup key mb} (lem-disjoint key) ⟩
+          Maybe.union (lookup key mb) (lookup key ma)
+        ≡⟨ sym (prop-lookup-unionWith key const _ _) ⟩
+          lookup key (unionWith const mb ma)
+        ∎
+
+  --
+  prop-union-assoc
+    : ∀ {ma mb mc : Map k a}
+    → union (union ma mb) mc ≡ union ma (union mb mc)
+  --
+  prop-union-assoc {ma} {mb} {mc} = prop-equality eq-key
+    where
+      eq-key = λ key →
+        begin
+          lookup key (union (union ma mb) mc)
+        ≡⟨ prop-lookup-union key _ _ ⟩
+          Maybe.union (lookup key (union ma mb)) (lookup key mc)
+        ≡⟨ cong (λ o → Maybe.union o (lookup key mc)) (prop-lookup-union key _ _) ⟩
+          Maybe.union (Maybe.union (lookup key ma) (lookup key mb)) (lookup key mc)
+        ≡⟨ Maybe.prop-union-assoc {_} {lookup key ma} {_} {_} ⟩
+          Maybe.union (lookup key ma) (Maybe.union (lookup key mb) (lookup key mc))
+        ≡⟨ cong (λ o → Maybe.union (lookup key ma) o) (sym (prop-lookup-union key _ _)) ⟩
+          Maybe.union (lookup key ma) (lookup key (union mb mc))
+        ≡⟨ sym (prop-lookup-union key _ _) ⟩
+          lookup key (union ma (union mb mc))
+        ∎
+
+  -- 
+  prop-lookup-filter
+    : ∀ (key : k) (m : Map k a) (p : a → Bool)
+    → lookup key (filter p m)
+      ≡ Maybe.filter p (lookup key m)
+  --
+  prop-lookup-filter key m p =
+    prop-lookup-filterWithKey key m (λ _ x → p x)
+
+  --
+  prop-lookup-filterWithKey-Just
+    : ∀ (key : k) (x : a) (m : Map k a) (p : k → a → Bool)
+    → lookup key m ≡ Just x
+    → lookup key (filterWithKey p m)
+      ≡ (if p key x then Just x else Nothing)
+  --
+  prop-lookup-filterWithKey-Just key x m p eq =
+    begin
+      lookup key (filterWithKey p m)
+    ≡⟨ prop-lookup-filterWithKey key m p ⟩
+      Maybe.filter (p key) (lookup key m)
+    ≡⟨ cong (Maybe.filter (p key)) eq ⟩    
+      Maybe.filter (p key) (Just x)
+    ≡⟨⟩
+      (if p key x then Just x else Nothing)
+    ∎
+
+{-----------------------------------------------------------------------------
+    Proofs
+    involving keysSet
+------------------------------------------------------------------------------}
+module _ {k a : Type} {{_ : Ord k}} where
+
+  --
+  prop-member-keysSet
+    : ∀ {key : k} {m : Map k a}
+    → Set.member key (keysSet m)
+      ≡ member key m
+  --
+  prop-member-keysSet {key} {m} =
+    begin
+      Set.member key (keysSet m)
+    ≡⟨ Set.prop-member-fromList key (keys m) ⟩
+      elem key (keys m)
+    ≡⟨ prop-elem-keys key m ⟩
+      member key m
+    ∎
+
+  --
+  prop-null-keysSet
+    : ∀ {m : Map k a}
+    → Set.null (keysSet m) ≡ null m
+  --
+  prop-null-keysSet {m}
+    with null m in eql
+    with Set.null (keysSet m) in eqr
+  ... | True | True = refl
+  ... | True | False = trans (sym eqr) lem2 -- contradiction
+    where
+      lem1 = λ key → 
+        begin
+          Set.member key (keysSet m)
+        ≡⟨ prop-member-keysSet ⟩
+          member key m
+        ≡⟨ cong (member key) (prop-null→empty m eql) ⟩
+          member key empty
+        ≡⟨ cong isJust (prop-lookup-empty key) ⟩
+          False
+        ∎
+      lem2 = Set.prop-member-null (keysSet m) lem1
+  ... | False | False = refl
+  ... | False | True = sym (trans (sym eql) lem2) -- contradiction
+    where
+      lem1 = λ key → 
+        begin
+          member key m
+        ≡⟨ sym prop-member-keysSet ⟩
+          Set.member key (keysSet m)
+        ≡⟨ cong (Set.member key) (Set.prop-null→empty (keysSet m) eqr) ⟩
+          Set.member key Set.empty
+        ≡⟨ Set.prop-member-empty key ⟩
+          False
+        ∎
+      lem2 = prop-member-null m lem1
+
+  --
+  prop-keysSet-empty
+    : keysSet {k} {a} empty ≡ Set.empty {k}
+  --
+  prop-keysSet-empty =
+      Set.prop-null→empty _ lem1
+    where
+      lem1 =
+        begin
+          Set.null (keysSet {k} {a} empty)
+        ≡⟨ prop-null-keysSet ⟩
+          null {k} {a} empty
+        ≡⟨ prop-null-empty ⟩
+          True
+        ∎
+
+  --
+  prop-keysSet-intersection
+      : ∀ {ma mb : Map k a}
+      → keysSet (intersection ma mb)
+        ≡ Set.intersection (keysSet ma) (keysSet mb)
+  -- 
+  prop-keysSet-intersection {ma} {mb} = Set.prop-equality lem1
+    where
+      lem1
+        : ∀ (key : k)
+        → Set.member key (keysSet (intersection ma mb))
+          ≡ Set.member key (Set.intersection (keysSet ma) (keysSet mb))
+      lem1 key =
+        begin
+          Set.member key (keysSet (intersection ma mb))
+        ≡⟨ prop-member-keysSet ⟩
+          member key (intersection ma mb)
+        ≡⟨ cong isJust (prop-lookup-intersection _ _ _) ⟩
+          isJust (Maybe.intersectionWith const (lookup key ma) (lookup key mb))
+        ≡⟨ Maybe.prop-isJust-intersectionWith ⟩
+          isJust (lookup key ma) && isJust (lookup key mb)
+        ≡⟨⟩
+          member key ma && member key mb
+        ≡⟨ cong (λ o → o && _) (sym prop-member-keysSet) ⟩
+          Set.member key (keysSet ma) && member key mb
+        ≡⟨ cong (λ o → _ && o) (sym prop-member-keysSet) ⟩
+          Set.member key (keysSet ma) && Set.member key (keysSet mb)
+        ≡⟨ sym (Set.prop-member-intersection key (keysSet ma) (keysSet mb)) ⟩
+          Set.member key (Set.intersection (keysSet ma) (keysSet mb))
+        ∎
+
+  --
+  prop-keysSet-union
+    : ∀ {ma mb : Map k a}
+    → keysSet (union ma mb)
+      ≡ Set.union (keysSet ma) (keysSet mb)
+  -- 
+  prop-keysSet-union {ma} {mb} = Set.prop-equality lem1
+    where
+      lem1
+        : ∀ (key : k)
+        → Set.member key (keysSet (union ma mb))
+          ≡ Set.member key (Set.union (keysSet ma) (keysSet mb))
+      lem1 key
+        rewrite prop-member-keysSet {key} {union ma mb}
+        | prop-lookup-union key ma mb
+        | Set.prop-member-union {k} key (keysSet ma) (keysSet mb)
+        | prop-member-keysSet {key} {ma}
+        | prop-member-keysSet {key} {mb}
+        with lookup key ma | lookup key mb
+      ... | Nothing | Nothing = refl
+      ... | Just a  | Nothing = refl
+      ... | Nothing | Just b  = refl 
+      ... | Just a  | Just b  = refl
+
+  --
+  prop-disjoint-keysSet
+    : ∀ {ma mb : Map k a}
+    → disjoint ma mb
+      ≡ Set.disjoint (keysSet ma) (keysSet mb)
+  --
+  prop-disjoint-keysSet {ma} {mb} =
+    begin
+      null (intersection ma mb)
+    ≡⟨ sym prop-null-keysSet ⟩
+      Set.null (keysSet (intersection ma mb))
+    ≡⟨ cong Set.null prop-keysSet-intersection ⟩
+      Set.null (Set.intersection (keysSet ma) (keysSet mb))
+    ∎
+
+{-----------------------------------------------------------------------------
+    Proofs
+    involving withoutKeys and restrictKeys
+------------------------------------------------------------------------------}
+module _ {k a : Type} {{_ : Ord k}} where
+
+  --
+  prop-lookup-withoutKeys
+    : ∀ (key : k) (m : Map k a) (ks : Set k)
+    → lookup key (withoutKeys m ks)
+      ≡ Maybe.filt (not (Set.member key ks)) (lookup key m)
+  --
+  prop-lookup-withoutKeys key m ks =
+      begin
+        lookup key (withoutKeys m ks)
+      ≡⟨ prop-lookup-filterWithKey key m p ⟩
+        Maybe.filter (p key) (lookup key m)
+      ≡⟨ Maybe.prop-filter-filt (not (Set.member key ks)) (lookup key m) ⟩
+        Maybe.filt (not (Set.member key ks)) (lookup key m)
+      ∎
+    where
+      p : k → a → Bool
+      p = λ kx _ → not (Set.member kx ks)
+
+  --
+  prop-lookup-restrictKeys
+    : ∀ (key : k) (m : Map k a) (ks : Set k)
+    → lookup key (restrictKeys m ks)
+      ≡ Maybe.filt (Set.member key ks) (lookup key m)
+  --
+  prop-lookup-restrictKeys key m ks =
+      begin
+        lookup key (restrictKeys m ks)
+      ≡⟨ prop-lookup-filterWithKey key m p ⟩
+        Maybe.filter (p key) (lookup key m)
+      ≡⟨ Maybe.prop-filter-filt (Set.member key ks) (lookup key m) ⟩
+        Maybe.filt (Set.member key ks) (lookup key m)
+      ∎
+    where
+      p : k → a → Bool
+      p = λ kx _ → Set.member kx ks
+
+  --
+  prop-withoutKeys-empty
+    : ∀ (m : Map k a)
+    → withoutKeys m Set.empty ≡ m
+  --
+  prop-withoutKeys-empty m = prop-equality eq-key
+    where
+      eq-key = λ key →
+        begin
+          lookup key (withoutKeys m Set.empty)
+        ≡⟨ prop-lookup-withoutKeys key m Set.empty ⟩
+          Maybe.filt (not (Set.member key Set.empty)) (lookup key m)
+        ≡⟨ cong (λ o → Maybe.filt (not o) (lookup key m)) (Set.prop-member-empty key) ⟩
+          Maybe.filt True (lookup key m)
+        ≡⟨⟩
+          lookup key m
+        ∎
+
+  --
+  prop-withoutKeys-keysSet
+    : ∀ (m : Map k a)
+    → withoutKeys m (keysSet m) ≡ empty
+  --
+  prop-withoutKeys-keysSet m = prop-equality eq-key
+    where
+      ks = keysSet m
+
+      lem1
+        : ∀ (mx : Maybe a)
+        → Maybe.filt (not (isJust mx)) mx ≡ Nothing
+      lem1 Nothing = refl
+      lem1 (Just x) = refl
+
+      eq-key = λ key →
+        begin
+          lookup key (withoutKeys m ks)
+        ≡⟨ prop-lookup-withoutKeys key m ks ⟩
+          Maybe.filt (not (Set.member key ks)) (lookup key m)
+        ≡⟨ cong (λ o → Maybe.filt (not o) (lookup key m)) prop-member-keysSet ⟩
+          Maybe.filt (not (isJust (lookup key m))) (lookup key m)
+        ≡⟨ lem1 (lookup key m) ⟩
+          Nothing
+        ≡⟨ sym (prop-lookup-empty key) ⟩
+          lookup key empty
+        ∎
+
+  --
+  prop-restrictKeys-union
+    : ∀ (ma mb : Map k a) (ks : Set k)
+    → restrictKeys (union ma mb) ks
+      ≡ union (restrictKeys ma ks) (restrictKeys mb ks)
+  --
+  prop-restrictKeys-union ma mb ks = prop-equality eq-key
+    where
+      eq-key = λ key → let p = Set.member key ks in
+        begin
+          lookup key (restrictKeys (union ma mb) ks)
+        ≡⟨ prop-lookup-restrictKeys key (union ma mb) ks ⟩
+          Maybe.filt p (lookup key (union ma mb))
+        ≡⟨ cong (Maybe.filt p) (prop-lookup-union key ma mb)  ⟩
+          Maybe.filt p
+            (Maybe.union (lookup key ma) (lookup key mb))
+        ≡⟨ Maybe.prop-filt-union p {lookup key ma} {lookup key mb} ⟩
+          Maybe.union
+            (Maybe.filt p (lookup key ma))
+            (Maybe.filt p (lookup key mb))
+        ≡⟨ cong (λ o → Maybe.union o (Maybe.filt p (lookup key mb))) (sym (prop-lookup-restrictKeys key ma ks)) ⟩
+          Maybe.union
+            (lookup key (restrictKeys ma ks))
+            (Maybe.filt p (lookup key mb))
+        ≡⟨ cong (λ o → Maybe.union (lookup key (restrictKeys ma ks)) o) (sym (prop-lookup-restrictKeys key mb ks)) ⟩
+          Maybe.union
+            (lookup key (restrictKeys ma ks))
+            (lookup key (restrictKeys mb ks))
+        ≡⟨ sym (prop-lookup-union key _ _) ⟩
+          lookup key (union (restrictKeys ma ks) (restrictKeys mb ks))
+        ∎
+
+  --
+  prop-restrictKeys-keysSet
+    : ∀ (m : Map k a)
+    → restrictKeys m (keysSet m) ≡ m
+  --
+  prop-restrictKeys-keysSet m = prop-equality eq-key
+    where
+      ks = keysSet m
+
+      lem1
+        : ∀ (mx : Maybe a)
+        → Maybe.filt (isJust mx) mx ≡ mx
+      lem1 Nothing = refl
+      lem1 (Just x) = refl
+
+      eq-key = λ key →
+        begin
+          lookup key (restrictKeys m ks)
+        ≡⟨ prop-lookup-restrictKeys key m ks ⟩
+          Maybe.filt (Set.member key ks) (lookup key m)
+        ≡⟨ cong (λ o → Maybe.filt o (lookup key m)) prop-member-keysSet ⟩
+          Maybe.filt (isJust (lookup key m)) (lookup key m)
+        ≡⟨ lem1 (lookup key m) ⟩
+          lookup key m
+        ∎
+
+  --
+  prop-withoutKeys-union
+    : ∀ (ma mb : Map k a) (ks : Set k)
+    → withoutKeys (union ma mb) ks
+      ≡ union (withoutKeys ma ks) (withoutKeys mb ks)
+  --
+  prop-withoutKeys-union ma mb ks = prop-equality eq-key
+    where
+      eq-key = λ key → let p = not (Set.member key ks) in
+        begin
+          lookup key (withoutKeys (union ma mb) ks)
+        ≡⟨ prop-lookup-withoutKeys key (union ma mb) ks ⟩
+          Maybe.filt p (lookup key (union ma mb))
+        ≡⟨ cong (Maybe.filt p) (prop-lookup-union key ma mb)  ⟩
+          Maybe.filt p
+            (Maybe.union (lookup key ma) (lookup key mb))
+        ≡⟨ Maybe.prop-filt-union p {lookup key ma} {lookup key mb} ⟩
+          Maybe.union
+            (Maybe.filt p (lookup key ma))
+            (Maybe.filt p (lookup key mb))
+        ≡⟨ cong (λ o → Maybe.union o (Maybe.filt p (lookup key mb))) (sym (prop-lookup-withoutKeys key ma ks)) ⟩
+          Maybe.union
+            (lookup key (withoutKeys ma ks))
+            (Maybe.filt p (lookup key mb))
+        ≡⟨ cong (λ o → Maybe.union (lookup key (withoutKeys ma ks)) o) (sym (prop-lookup-withoutKeys key mb ks)) ⟩
+          Maybe.union
+            (lookup key (withoutKeys ma ks))
+            (lookup key (withoutKeys mb ks))
+        ≡⟨ sym (prop-lookup-union key _ _) ⟩
+          lookup key (union (withoutKeys ma ks) (withoutKeys mb ks))
+        ∎
+
+  --
+  prop-withoutKeys-difference
+    : ∀ (m : Map k a) (ka kb : Set k)
+    → withoutKeys m (Set.difference ka kb)
+      ≡ union (withoutKeys m ka) (restrictKeys m kb)
+  --
+  prop-withoutKeys-difference m ka kb = prop-equality eq-key
+    where
+      eq-key
+        : ∀ (key : k)
+        → lookup key (withoutKeys m (Set.difference ka kb))
+          ≡ lookup key (union (withoutKeys m ka) (restrictKeys m kb))
+      eq-key key =
+        begin
+          lookup key (withoutKeys m (Set.difference ka kb))
+        ≡⟨ prop-lookup-withoutKeys key _ (Set.difference ka kb) ⟩
+          Maybe.filt pab (lookup key m)
+        ≡⟨ cong (λ o → Maybe.filt o (lookup key m)) lem-pab ⟩
+          Maybe.filt (pa || not-pb) (lookup key m)
+        ≡⟨ Maybe.prop-filt-|| pa not-pb {lookup key m} ⟩
+          Maybe.union
+            (Maybe.filt pa (lookup key m))
+            (Maybe.filt not-pb (lookup key m))
+        ≡⟨ cong (λ o → Maybe.union o (Maybe.filt not-pb (lookup key m))) (sym (prop-lookup-withoutKeys key m ka)) ⟩
+          Maybe.union
+            (lookup key (withoutKeys m ka))
+            (Maybe.filt not-pb (lookup key m))
+        ≡⟨ cong (λ o → Maybe.union (lookup key (withoutKeys m ka)) o) (sym (prop-lookup-restrictKeys key m kb)) ⟩
+          Maybe.union
+            (lookup key (withoutKeys m ka))
+            (lookup key (restrictKeys m kb))
+        ≡⟨ sym (prop-lookup-union key _ _) ⟩
+          lookup key (union (withoutKeys m ka) (restrictKeys m kb))
+        ∎
+        where
+          pa = not (Set.member key ka)
+          not-pb = Set.member key kb
+          pab = not (Set.member key (Set.difference ka kb))
+
+          lem-pab : pab ≡ (pa || not-pb)
+          lem-pab =
+            begin
+              not (Set.member key (Set.difference ka kb))
+            ≡⟨ cong not (Set.prop-member-difference key ka kb) ⟩
+              not (Set.member key ka && not (Set.member key kb))
+            ≡⟨ prop-deMorgan-not-&& (Set.member key ka) (not (Set.member key kb)) ⟩
+              (not (Set.member key ka) || not (not (Set.member key kb)))
+            ≡⟨ cong (λ o → not (Set.member key ka) || o) (not-not (Set.member key kb)) ⟩
+              (not (Set.member key ka) || Set.member key kb)
+            ∎
+
+  --
+  prop-withoutKeys-withoutKeys
+    : ∀ (m : Map k a) (ka kb : Set k)
+    → withoutKeys (withoutKeys m ka) kb
+      ≡ withoutKeys m (Set.union ka kb)
+  --
+  prop-withoutKeys-withoutKeys m ka kb = prop-equality eq-key
+    where
+      eq-key
+        : ∀ (key : k)
+        → lookup key (withoutKeys (withoutKeys m ka) kb)
+          ≡ lookup key (withoutKeys m (Set.union ka kb))
+      eq-key key =
+        begin
+          lookup key (withoutKeys (withoutKeys m ka) kb)
+        ≡⟨ prop-lookup-withoutKeys key _ kb ⟩
+          Maybe.filt pb (lookup key (withoutKeys m ka))
+        ≡⟨ cong (Maybe.filt pb) (prop-lookup-withoutKeys key _ ka) ⟩
+          Maybe.filt pb (Maybe.filt pa (lookup key m))
+        ≡⟨ Maybe.prop-filt-filt pb pa (lookup key m) ⟩
+          Maybe.filt (pb && pa) (lookup key m)
+        ≡⟨ cong (λ o → Maybe.filt o (lookup key m)) (sym lem-pab) ⟩
+          Maybe.filt pab (lookup key m)
+        ≡⟨ sym (prop-lookup-withoutKeys key _ (Set.union ka kb)) ⟩
+          lookup key (withoutKeys m (Set.union ka kb))
+        ∎
+        where
+          pa = not (Set.member key ka)
+          pb = not (Set.member key kb)
+          pab = not (Set.member key (Set.union ka kb))
+
+          lem-pab : pab ≡ (pb && pa)
+          lem-pab =
+            begin
+              not (Set.member key (Set.union ka kb))
+            ≡⟨ cong not (Set.prop-member-union key ka kb) ⟩
+              not (Set.member key ka || Set.member key kb)
+            ≡⟨ prop-deMorgan-not-|| (Set.member key ka) (Set.member key kb) ⟩
+              (not (Set.member key ka) && not (Set.member key kb))
+            ≡⟨ &&-sym (not (Set.member key ka)) (not (Set.member key kb)) ⟩
+              (not (Set.member key kb) && not (Set.member key ka))
+            ∎
+
+  --
+  @0 prop-withoutKeys-intersection
+    : ∀ (m : Map k a) (ka kb : Set k)
+    → withoutKeys m (Set.intersection ka kb)
+      ≡ union (withoutKeys m ka) (withoutKeys m kb)
+  --
+  prop-withoutKeys-intersection m ka kb = prop-equality eq-key
+    where
+      eq-key
+        : ∀ (key : k)
+        → lookup key (withoutKeys m (Set.intersection ka kb))
+          ≡ lookup key (union (withoutKeys m ka) (withoutKeys m kb))
+      eq-key key =
+        begin
+          lookup key (withoutKeys m (Set.intersection ka kb))
+        ≡⟨ prop-lookup-withoutKeys key m (Set.intersection ka kb) ⟩
+          Maybe.filt pab (lookup key m)
+        ≡⟨ cong (λ o → Maybe.filt o (lookup key m)) lem-pab ⟩
+          Maybe.filt (pa || pb) (lookup key m)
+        ≡⟨ Maybe.prop-filt-|| pa pb {lookup key m} ⟩
+          Maybe.union
+            (Maybe.filt pa (lookup key m))
+            (Maybe.filt pb (lookup key m))
+        ≡⟨ cong (λ o → Maybe.union o (Maybe.filt pb (lookup key m))) (sym (prop-lookup-withoutKeys key m ka)) ⟩
+          Maybe.union
+            (lookup key (withoutKeys m ka))
+            (Maybe.filt pb (lookup key m))
+        ≡⟨ cong (λ o → Maybe.union (lookup key (withoutKeys m ka)) o) (sym (prop-lookup-withoutKeys key m kb)) ⟩
+          Maybe.union
+            (lookup key (withoutKeys m ka))
+            (lookup key (withoutKeys m kb))
+        ≡⟨ sym (prop-lookup-union key _ _) ⟩
+          lookup key (union (withoutKeys m ka) (withoutKeys m kb))
+        ∎
+        where
+          pa = not (Set.member key ka)
+          pb = not (Set.member key kb)
+          pab = not (Set.member key (Set.intersection ka kb))
+
+          lem-pab : pab ≡ (pa || pb)
+          lem-pab =
+            begin
+              not (Set.member key (Set.intersection ka kb))
+            ≡⟨ cong not (Set.prop-member-intersection key ka kb) ⟩
+              not (Set.member key ka && Set.member key kb)
+            ≡⟨ prop-deMorgan-not-&& (Set.member key ka) (Set.member key kb) ⟩
+              (not (Set.member key ka) || not (Set.member key kb))
+            ∎
+
+  --
+  prop-union-restrictKeys-absorbs
+    : ∀ (ma mb : Map k a)
+    → union ma (restrictKeys mb (keysSet ma))
+      ≡ ma
+  --
+  prop-union-restrictKeys-absorbs ma mb = prop-equality eq-key
+    where
+      eq-key
+        : ∀ (key : k)
+        → lookup key (union ma (restrictKeys mb (keysSet ma)))
+          ≡ lookup key ma
+      eq-key key
+        rewrite prop-lookup-union key ma (restrictKeys mb (keysSet ma))
+        | prop-lookup-restrictKeys key mb (keysSet ma)
+        | prop-member-keysSet {k} {a} {key} {ma}
+        with lookup key ma
+      ... | Nothing = refl
+      ... | Just a
+          with lookup key mb
+      ...   | Just b = refl
+      ...   | Nothing = refl
diff --git a/lib/containers/agda/Data/Set.agda b/lib/containers/agda/Data/Set.agda
new file mode 100644
index 00000000..de24d673
--- /dev/null
+++ b/lib/containers/agda/Data/Set.agda
@@ -0,0 +1,4 @@
+module Data.Set where
+
+open import Haskell.Data.Set public
+open import Data.Set.Prop public
diff --git a/lib/containers/agda/Data/Set/Prop.agda b/lib/containers/agda/Data/Set/Prop.agda
new file mode 100644
index 00000000..da56c616
--- /dev/null
+++ b/lib/containers/agda/Data/Set/Prop.agda
@@ -0,0 +1,501 @@
+
+-- | Proofs on 'Set'.
+module Data.Set.Prop where
+
+open import Haskell.Law.Bool
+open import Haskell.Law.Equality
+open import Haskell.Prelude hiding (lookup; null; map; filter)
+
+open import Haskell.Data.Set
+
+{-----------------------------------------------------------------------------
+    Properties
+    Basic
+------------------------------------------------------------------------------}
+module _ {a : Type} {{_ : Ord a}} where
+
+  --
+  prop-null-empty
+    : null {a} empty ≡ True
+  --
+  prop-null-empty =
+    prop-member-null empty prop-member-empty 
+
+{-----------------------------------------------------------------------------
+    Properties
+    https://en.wikipedia.org/wiki/Boolean_algebra_(structure)
+------------------------------------------------------------------------------}
+module _ {a : Type} {{_ : Ord a}} where
+
+  --
+  prop-union-idem
+    : ∀ {sa : Set a}
+    → union sa sa
+        ≡ sa
+  --
+  prop-union-idem {sa} = prop-equality eq
+    where
+      eq
+        : ∀ (x : a)
+        → member x (union sa sa) ≡ member x sa
+      eq x
+        rewrite prop-member-union x sa sa
+        | prop-||-idem (member x sa)
+        = refl
+
+  --
+  prop-union-assoc
+    : ∀ {sa sb sc : Set a}
+    → union (union sa sb) sc
+      ≡ union sa (union sb sc)
+  --
+  prop-union-assoc {sa} {sb} {sc} = prop-equality eq
+    where
+      eq
+        : ∀ (x : a)
+        → member x (union (union sa sb) sc)
+          ≡ member x (union sa (union sb sc))
+      eq x
+        rewrite prop-member-union x (union sa sb) sc
+        | prop-member-union x sa sb
+        | prop-member-union x sa (union sb sc)
+        | prop-member-union x sb sc
+        | prop-||-assoc (member x sa) (member x sb) (member x sc)
+        = refl
+
+  --
+  prop-union-sym
+    : ∀ {sa sb : Set a}
+    → union sa sb
+        ≡ union sb sa
+  --
+  prop-union-sym {sa} {sb} = prop-equality eq
+    where
+      eq
+        : ∀ (x : a)
+        → member x (union sa sb) ≡ member x (union sb sa)
+      eq x
+        rewrite prop-member-union x sa sb
+        | prop-member-union x sb sa
+        | prop-||-sym (member x sa) (member x sb)
+        = refl
+
+  --
+  prop-union-absorb
+    : ∀ {sa sb : Set a}
+    → union sa (intersection sa sb)
+      ≡ sa
+  --
+  prop-union-absorb {sa} {sb} = prop-equality eq
+    where
+      eq
+        : ∀ (x : a)
+        → member x (union sa (intersection sa sb)) ≡ member x sa
+      eq x
+        rewrite prop-member-union x sa (intersection sa sb)
+        | prop-member-intersection x sa sb
+        | prop-||-absorb (member x sa) (member x sb)
+        = refl
+
+  --
+  prop-union-identity
+    : ∀ {sa : Set a}
+    → union sa empty
+      ≡ sa
+  --
+  prop-union-identity {sa} = prop-equality eq
+    where
+      eq
+        : ∀ (x : a)
+        → member x (union sa empty) ≡ member x sa
+      eq x
+        rewrite prop-member-union x sa empty
+        | prop-member-empty x
+        | prop-||-identity (member x sa)
+        = refl
+
+  --
+  prop-union-intersection-distribute
+    : ∀ {sa sb sc : Set a}
+    → union sa (intersection sb sc)
+      ≡ intersection (union sa sb) (union sa sc)
+  --
+  prop-union-intersection-distribute {sa} {sb} {sc} = prop-equality eq
+    where
+      eq
+        : ∀ (x : a)
+        → member x (union sa (intersection sb sc))
+          ≡ member x (intersection (union sa sb) (union sa sc))
+      eq x
+        rewrite prop-member-union x sa (intersection sb sc)
+        | prop-member-intersection x sb sc
+        | prop-member-intersection x (union sa sb) (union sa sc)
+        | prop-member-union x sa sb
+        | prop-member-union x sa sc
+        | prop-||-&&-distribute (member x sa) (member x sb) (member x sc)
+        = refl
+
+
+  --
+  prop-intersection-idem
+    : ∀ {sa : Set a}
+    → intersection sa sa
+        ≡ sa
+  --
+  prop-intersection-idem {sa} = prop-equality eq
+    where
+      eq
+        : ∀ (x : a)
+        → member x (intersection sa sa) ≡ member x sa
+      eq x
+        rewrite prop-member-intersection x sa sa
+        | prop-&&-idem (member x sa)
+        = refl
+
+  --
+  prop-intersection-assoc
+    : ∀ {sa sb sc : Set a}
+    → intersection (intersection sa sb) sc
+      ≡ intersection sa (intersection sb sc)
+  --
+  prop-intersection-assoc {sa} {sb} {sc} = prop-equality eq
+    where
+      eq
+        : ∀ (x : a)
+        → member x (intersection (intersection sa sb) sc)
+          ≡ member x (intersection sa (intersection sb sc))
+      eq x
+        rewrite prop-member-intersection x (intersection sa sb) sc
+        | prop-member-intersection x sa sb
+        | prop-member-intersection x sa (intersection sb sc)
+        | prop-member-intersection x sb sc
+        | prop-&&-assoc (member x sa) (member x sb) (member x sc)
+        = refl
+
+  --
+  prop-intersection-sym
+    : ∀ {sa sb : Set a}
+    → intersection sa sb
+        ≡ intersection sb sa
+  --
+  prop-intersection-sym {sa} {sb} = prop-equality eq
+    where
+      eq
+        : ∀ (x : a)
+        → member x (intersection sa sb) ≡ member x (intersection sb sa)
+      eq x
+        rewrite prop-member-intersection x sa sb
+        | prop-member-intersection x sb sa
+        | prop-&&-sym (member x sa) (member x sb)
+        = refl
+
+  --
+  prop-intersection-absorb
+    : ∀ {sa sb : Set a}
+    → intersection sa (union sa sb)
+      ≡ sa
+  --
+  prop-intersection-absorb {sa} {sb} = prop-equality eq
+    where
+      eq
+        : ∀ (x : a)
+        → member x (intersection sa (union sa sb)) ≡ member x sa
+      eq x
+        rewrite prop-member-intersection x sa (union sa sb)
+        | prop-member-union x sa sb
+        | prop-&&-absorb (member x sa) (member x sb)
+        = refl
+
+  --
+  prop-intersection-union-distribute
+    : ∀ {sa sb sc : Set a}
+    → intersection sa (union sb sc)
+      ≡ union (intersection sa sb) (intersection sa sc)
+  --
+  prop-intersection-union-distribute {sa} {sb} {sc} = prop-equality eq
+    where
+      eq
+        : ∀ (x : a)
+        → member x (intersection sa (union sb sc))
+          ≡ member x (union (intersection sa sb) (intersection sa sc))
+      eq x
+        rewrite prop-member-intersection x sa (union sb sc)
+        | prop-member-union x sb sc
+        | prop-member-union x (intersection sa sb) (intersection sa sc)
+        | prop-member-intersection x sa sb
+        | prop-member-intersection x sa sc
+        | prop-&&-||-distribute (member x sa) (member x sb) (member x sc)
+        = refl
+
+  --
+  prop-intersection-empty-right
+    : ∀ {sa : Set a}
+    → intersection sa empty
+      ≡ empty
+  --
+  prop-intersection-empty-right {sa} = prop-equality eq
+    where
+      eq
+        : ∀ (x : a)
+        → member x (intersection sa empty) ≡ member x empty
+      eq x
+        rewrite prop-member-intersection x sa empty
+        | prop-member-empty x
+        | prop-x-&&-False (member x sa)
+        = refl
+
+  --
+  prop-intersection-empty-left
+    : ∀ {sa : Set a}
+    → intersection empty sa
+      ≡ empty
+  --
+  prop-intersection-empty-left {sa} = prop-equality eq
+    where
+      eq
+        : ∀ (x : a)
+        → member x (intersection empty sa) ≡ member x empty
+      eq x
+        rewrite prop-member-intersection x empty sa
+        | prop-member-empty x
+        = refl
+
+{-----------------------------------------------------------------------------
+    Properties
+    involving  difference
+------------------------------------------------------------------------------}
+module _ {a : Type} {{_ : Ord a}} where
+
+  --
+  prop-intersection-difference
+    : ∀ {sa sb : Set a}
+    → intersection sb (difference sa sb)
+      ≡ empty
+  --
+  prop-intersection-difference {sa} {sb} = prop-equality eq
+    where
+      eq
+        : ∀ (x : a)
+        → member x (intersection sb (difference sa sb)) ≡ member x empty
+      eq x
+        rewrite prop-member-intersection x sb (difference sa sb)
+        | prop-member-difference x sa sb
+        | prop-member-empty x
+        with member x sa | member x sb
+      ... | True  | True  = refl
+      ... | False | True  = refl
+      ... | True  | False = refl
+      ... | False | False = refl
+
+  --
+  prop-disjoint-difference
+    : ∀ {sa sb : Set a}
+    → disjoint sb (difference sa sb)
+      ≡ True
+  --
+  prop-disjoint-difference {sa} {sb} =
+    trans (cong null prop-intersection-difference) prop-null-empty
+
+  --
+  prop-union-difference
+    : ∀ {sa sb : Set a}
+    → union (difference sa sb) sb
+      ≡ union sa sb
+  --
+  prop-union-difference {sa} {sb} = prop-equality eq
+    where
+      eq
+        : ∀ (x : a)
+        → member x (union (difference sa sb) sb)
+          ≡ member x (union sa sb)
+      eq x
+        rewrite prop-member-union x (difference sa sb) sb
+        | prop-member-difference x sa sb
+        | prop-member-union x sa sb
+        with member x sa | member x sb
+      ... | True  | True  = refl
+      ... | False | True  = refl
+      ... | True  | False = refl
+      ... | False | False = refl
+
+  --
+  prop-difference-union-x
+    : ∀ {sa sb sc : Set a}
+    → difference (union sa sb) sc
+      ≡ union (difference sa sc) (difference sb sc)
+  --
+  prop-difference-union-x {sa} {sb} {sc} = prop-equality eq
+    where
+      eq
+        : ∀ (x : a)
+        → member x (difference (union sa sb) sc)
+          ≡ member x (union (difference sa sc) (difference sb sc))
+      eq x
+        rewrite prop-member-difference x (union sa sb) sc
+        | prop-member-union x sa sb
+        | prop-member-union x (difference sa sc) (difference sb sc)
+        | prop-member-difference x sa sc
+        | prop-member-difference x sb sc
+        with member x sa | member x sb
+      ... | False | r = refl
+      ... | True  | True  = sym (prop-||-idem (not (member x sc)))
+      ... | True  | False = sym (prop-x-||-False (not (member x sc)))
+
+  --
+  prop-deMorgan-difference-intersection
+    : ∀ {sa sb sc : Set a}
+    → difference sa (intersection sb sc)
+      ≡ union (difference sa sb) (difference sa sc)
+  --
+  prop-deMorgan-difference-intersection {sa} {sb} {sc} = prop-equality eq
+    where
+      eq
+        : ∀ (x : a)
+        → member x (difference sa (intersection sb sc))
+          ≡ member x (union (difference sa sb) (difference sa sc))
+      eq x
+        rewrite prop-member-difference x sa (intersection sb sc)
+        | prop-member-intersection x sb sc
+        | prop-member-union x (difference sa sb) (difference sa sc)
+        | prop-member-difference x sa sb
+        | prop-member-difference x sa sc
+        with member x sa
+      ... | False = refl
+      ... | True  = prop-deMorgan-not-&& (member x sb) (member x sc)
+
+  --
+  prop-deMorgan-difference-union
+    : ∀ {sa sb sc : Set a}
+    → difference sa (union sb sc)
+      ≡ intersection (difference sa sb) (difference sa sc)
+  --
+  prop-deMorgan-difference-union {sa} {sb} {sc} = prop-equality eq
+    where
+      eq
+        : ∀ (x : a)
+        → member x (difference sa (union sb sc))
+          ≡ member x (intersection (difference sa sb) (difference sa sc))
+      eq x
+        rewrite prop-member-difference x sa (union sb sc)
+        | prop-member-union x sb sc
+        | prop-member-intersection x (difference sa sb) (difference sa sc)
+        | prop-member-difference x sa sb
+        | prop-member-difference x sa sc
+        with member x sa
+      ... | False = refl
+      ... | True  = prop-deMorgan-not-|| (member x sb) (member x sc)
+
+{-----------------------------------------------------------------------------
+    Properties
+    involving  isSubsetOf
+------------------------------------------------------------------------------}
+module _ {a : Type} {{_ : Ord a}} where
+
+  -- | The 'empty' set is a subset of every set.
+  prop-isSubsetOf-empty
+    : ∀ {sa : Set a}
+    → isSubsetOf empty sa ≡ True
+  --
+  prop-isSubsetOf-empty {sa} =
+    prop-intersection→isSubsetOf empty sa prop-intersection-empty-left
+
+  -- | 'isSubsetOf' is reflexive
+  prop-isSubsetOf-refl
+    : ∀ {sa : Set a}
+    → isSubsetOf sa sa ≡ True
+  --
+  prop-isSubsetOf-refl {sa} =
+    prop-intersection→isSubsetOf sa sa prop-intersection-idem
+
+  -- | 'isSubsetOf' is antisymmetric
+  prop-isSubsetOf-antisym
+    : ∀ {sa sb : Set a}
+    → isSubsetOf sa sb ≡ True
+    → isSubsetOf sb sa ≡ True
+    → sa ≡ sb
+  --
+  prop-isSubsetOf-antisym {sa} {sb} condab condba =
+    lem
+      (prop-isSubsetOf→intersection sa sb condab)
+      (prop-isSubsetOf→intersection sb sa condba)
+   where
+    lem
+      : intersection sa sb ≡ sa
+      → intersection sb sa ≡ sb
+      → sa ≡ sb
+    lem eq1 eq2 =
+      begin
+        sa
+      ≡⟨ sym eq1 ⟩
+        intersection sa sb
+      ≡⟨ prop-intersection-sym ⟩
+        intersection sb sa
+      ≡⟨ eq2 ⟩
+        sb
+      ∎
+
+  -- | 'isSubsetOf' is transitive
+  prop-isSubsetOf-trans
+    : ∀ {sa sb sc : Set a}
+    → isSubsetOf sa sb ≡ True
+    → isSubsetOf sb sc ≡ True
+    → isSubsetOf sa sc ≡ True
+  --
+  prop-isSubsetOf-trans {sa} {sb} {sc} condab condbc =
+    prop-intersection→isSubsetOf sa sc
+      (lem
+        (prop-isSubsetOf→intersection sa sb condab)
+        (prop-isSubsetOf→intersection sb sc condbc)
+      )
+   where
+    lem
+      : intersection sa sb ≡ sa
+      → intersection sb sc ≡ sb
+      → intersection sa sc ≡ sa
+    lem eq1 eq2 =
+      begin
+        intersection sa sc
+      ≡⟨ cong (λ o → intersection o sc) (sym eq1) ⟩
+        intersection (intersection sa sb) sc
+      ≡⟨ prop-intersection-assoc ⟩
+        intersection sa (intersection sb sc)
+      ≡⟨ cong (λ o → intersection sa o) eq2 ⟩
+        intersection sa sb
+      ≡⟨ eq1 ⟩
+        sa
+      ∎
+
+  --
+  prop-isSubsetOf-intersection
+    : ∀ {sa sb : Set a}
+    → isSubsetOf (intersection sa sb) sb ≡ True
+  --
+  prop-isSubsetOf-intersection {sa} {sb} =
+      prop-intersection→isSubsetOf _ _ eq
+    where
+      eq
+        : intersection (intersection sa sb) sb
+        ≡ intersection sa sb
+      eq
+        rewrite prop-intersection-assoc {_} {sa} {sb} {sb}
+        | prop-intersection-idem {_} {sb}
+        = refl
+
+  --
+  prop-isSubsetOf-difference
+    : ∀ {sa sb : Set a}
+    → isSubsetOf (difference sa sb) sa ≡ True
+  --
+  prop-isSubsetOf-difference {sa} {sb} =
+      prop-intersection→isSubsetOf _ _ (prop-equality eq)
+    where
+      eq
+        : ∀ (x : a)
+        → member x (intersection (difference sa sb) sa)
+          ≡ member x (difference sa sb)
+      eq x
+        rewrite prop-member-intersection x (difference sa sb) sa
+        | prop-member-difference x sa sb
+        with member x sa
+      ... | False = refl
+      ... | True  = prop-x-&&-True (not (member x sb))
diff --git a/lib/containers/agda/Haskell/Data/Map.agda b/lib/containers/agda/Haskell/Data/Map.agda
new file mode 100644
index 00000000..e8a6628c
--- /dev/null
+++ b/lib/containers/agda/Haskell/Data/Map.agda
@@ -0,0 +1,233 @@
+
+-- | Postulates and definitions of the operations supported by 'Map'.
+module Haskell.Data.Map where
+
+open import Haskell.Law.Equality
+open import Haskell.Prelude hiding (lookup; null; map; filter)
+import Haskell.Prelude as L using (map)
+
+open import Haskell.Data.Maybe using
+    ( isJust
+    )
+
+import Data.Map.Maybe as Maybe
+import Haskell.Prelude as List using (map)
+
+open import Data.Set using (Set)
+import Data.Set as Set
+
+{-----------------------------------------------------------------------------
+    Helper predicates
+------------------------------------------------------------------------------}
+Antitonic : {a : Type} → {{Ord a}} → (a → Bool) → Type
+Antitonic {a} p =
+  ∀ {x y : a} → ((x <= y) ≡ True) → ((p x >= p y) ≡ True)
+
+{-----------------------------------------------------------------------------
+    Functions
+    involving 1 value type
+------------------------------------------------------------------------------}
+postulate
+  Map : ∀ (k : Type) → Type → Type
+
+module _ {k a : Type} {{_ : Ord k}} where
+  postulate
+    lookup    : k → Map k a → Maybe a
+    null      : Map k a → Bool
+    toAscList : Map k a → List (k × a)
+
+  member : k → Map k a → Bool
+  member key = isJust ∘ lookup key
+
+  elems : Map k a → List a
+  elems = List.map snd ∘ toAscList
+
+  keys : Map k a → List k
+  keys = List.map fst ∘ toAscList
+
+  keysSet : Map k a → Set k
+  keysSet = Set.fromList ∘ keys
+
+  size : Map k a → Int
+  size = length ∘ toAscList
+
+  postulate
+    prop-elem-keys
+      : ∀ (key : k) (m : Map k a)
+      → elem key (keys m)
+        ≡ member key m
+
+  postulate
+    empty     : Map k a
+    insert    : k → a → Map k a → Map k a
+    delete    : k → Map k a → Map k a
+    update    : (a → Maybe a) → k → Map k a → Map k a
+    fromList  : List (k × a) → Map k a
+    fromListWith : (a → a → a) → List (k × a) → Map k a
+
+    unionWith     : (a → a → a) → Map k a → Map k a → Map k a
+    filterWithKey : (k → a → Bool) → Map k a → Map k a
+
+    takeWhileAntitone : (k → Bool) → Map k a → Map k a
+    dropWhileAntitone : (k → Bool) → Map k a → Map k a
+
+    prop-lookup-null
+      : ∀ (m : Map k a)
+          (_ : ∀ (key : k) → lookup key m ≡ Nothing)
+      → null m ≡ True
+
+    prop-null→empty
+      : ∀ (m : Map k a)
+      → null m ≡ True
+      → m ≡ empty
+  
+    prop-equality
+      : ∀ {m1 m2 : Map k a}
+      → (∀ (key : k) → lookup key m1 ≡ lookup key m2)
+      → m1 ≡ m2
+
+    prop-lookup-eq
+      : ∀ (key1 key2 : k) (m : Map k a)
+      → (key1 == key2) ≡ True
+      → lookup key1 m ≡ lookup key2 m
+
+    prop-lookup-empty
+      : ∀ (key : k)
+      → lookup key empty ≡ Nothing
+
+    prop-lookup-insert
+      : ∀ (key keyi : k) (x : a) (m : Map k a)
+      → lookup key (insert keyi x m)
+        ≡ (if (key == keyi) then Just x else lookup key m)
+
+    prop-lookup-delete
+      : ∀ (key keyi : k) (m : Map k a)
+      → lookup key (delete keyi m)
+        ≡ (if (key == keyi) then Nothing else lookup key m)
+
+    prop-lookup-update
+      : ∀ (key keyi : k) (m : Map k a) (f : a → Maybe a)
+      → lookup key (update f keyi m)
+        ≡ (if (key == keyi) then (lookup keyi m >>= f) else lookup key m)
+
+    prop-lookup-unionWith
+      : ∀ (key : k) (f : a → a → a) (m n : Map k a)
+      → lookup key (unionWith f m n)
+        ≡ Maybe.unionWith f (lookup key m) (lookup key n)
+
+    prop-lookup-filterWithKey
+      : ∀ (key : k) (m : Map k a) (p : k → a → Bool)
+      → lookup key (filterWithKey p m)
+        ≡ Maybe.filter (p key) (lookup key m)
+
+    prop-lookup-takeWhileAntitone
+      : ∀ (p : k → Bool) → Antitonic p
+      → ∀ (key : k) (m : Map k a)
+      → lookup key (takeWhileAntitone p m)
+        ≡ lookup key (filterWithKey (λ k _ → p k) m)
+
+    prop-lookup-dropWhileAntitone
+      : ∀ (p : k → Bool) → Antitonic p
+      → ∀ (key : k) (m : Map k a)
+      → lookup key (dropWhileAntitone p m)
+        ≡ lookup key (filterWithKey (λ k _ → not (p k)) m)
+
+
+  singleton : k → a → Map k a
+  singleton = λ k x → insert k x empty
+
+  alter : (Maybe a → Maybe a) → k → Map k a → Map k a
+  alter f k m = case f (lookup k m) of λ where
+    Nothing → delete k m
+    (Just a) → insert k a m
+
+  insertWith : (a → a → a) → k → a → Map k a → Map k a
+  insertWith f k new m = case lookup k m of λ where
+    Nothing → insert k new m
+    (Just old) → insert k (f new old) m
+
+  withoutKeys : Map k a → Set k → Map k a
+  withoutKeys m s = filterWithKey (λ k _ → not (Set.member k s)) m
+
+  restrictKeys : Map k a → Set k → Map k a
+  restrictKeys m s = filterWithKey (λ k _ → Set.member k s) m
+
+  filter : (a → Bool) → Map k a → Map k a
+  filter p = filterWithKey (λ _ x → p x)
+
+  union : Map k a → Map k a → Map k a
+  union = unionWith (λ x y → x)
+
+  spanAntitone : (k → Bool) → Map k a → (Map k a × Map k a)
+  spanAntitone p m = (takeWhileAntitone p m , dropWhileAntitone p m)
+
+  foldMap' : ∀ {{_ : Monoid b}} → (a → b) → Map k a → b
+  foldMap' f = foldMap f ∘ List.map snd ∘ toAscList
+
+instance
+  iMapFoldable : ∀ {k : Type} {{_ : Ord k}} → Foldable (Map k)
+  iMapFoldable =
+    record {DefaultFoldable (record {foldMap = foldMap'})}
+
+instance
+  iEqMap : ∀ {k v : Type} {{_ : Ord k}} {{_ : Eq v}} → Eq (Map k v)
+  iEqMap ._==_ m1 m2 = toAscList m1 == toAscList m2
+
+{-----------------------------------------------------------------------------
+    Operations
+    involving 2 value types
+------------------------------------------------------------------------------}
+module _ {k : Type} {{_ : Ord k}} where
+  postulate
+    instance
+      iMapFunctor : Functor (Map k)    
+
+module _ {k a b : Type} {{_ : Ord k}} where
+  postulate
+
+    mapWithKey : (k → a → b) → Map k a → Map k b
+    mapMaybeWithKey : (k → a → Maybe b) → Map k a → Map k b
+
+    intersection : Map k a → Map k b → Map k a
+
+  map : (a → b) → Map k a → Map k b
+  map = fmap
+
+  disjoint : Map k a → Map k b → Bool
+  disjoint m1 m2 = null (intersection m1 m2)
+
+  postulate
+    prop-lookup-fmap
+      : ∀ (key : k) (m : Map k a) (f : a → b)
+      → lookup key (fmap {{iMapFunctor}} f m)
+        ≡ fmap f (lookup key m)
+
+    prop-lookup-mapWithKey
+      : ∀ (key : k) (m : Map k a) (f : k → a → b)
+      → lookup key (mapWithKey f m)
+        ≡ fmap (f key) (lookup key m)
+
+    prop-lookup-mapMaybeWithKey
+      : ∀ (key : k) (m : Map k a) (f : k → a → Maybe b)
+      → lookup key (mapMaybeWithKey f m)
+        ≡ Maybe.mapMaybe (f key) (lookup key m)
+
+    prop-lookup-intersection
+      : ∀ (key : k) (m1 : Map k a) (m2 : Map k b)
+      → lookup key (intersection m1 m2)
+        ≡ Maybe.intersectionWith const (lookup key m1) (lookup key m2)
+
+{-----------------------------------------------------------------------------
+    Operations
+    involving 3 value types
+------------------------------------------------------------------------------}
+module _ {k a b c : Type} {{_ : Ord k}} where
+  postulate
+
+    intersectionWith : (a → b → c) → Map k a → Map k b → Map k c
+
+    prop-lookup-intersectionWith
+      : ∀ (key : k) (ma : Map k a) (mb : Map k b)
+          (f : a → b → c)
+      → lookup key (intersectionWith f ma mb)
+        ≡ Maybe.intersectionWith f (lookup key ma) (lookup key mb)
diff --git a/lib/containers/agda/Haskell/Data/Set.agda b/lib/containers/agda/Haskell/Data/Set.agda
new file mode 100644
index 00000000..6e572d27
--- /dev/null
+++ b/lib/containers/agda/Haskell/Data/Set.agda
@@ -0,0 +1,128 @@
+
+-- | Postulates and definitions of the operations supported by 'Set'.
+module Haskell.Data.Set where
+
+open import Haskell.Prelude hiding (lookup; null; map; filter)
+
+{-----------------------------------------------------------------------------
+    Data.Set
+------------------------------------------------------------------------------}
+
+postulate
+  Set : Type → Type
+
+module _ {a : Type} where
+  postulate
+    toAscList : Set a → List a
+    null      : Set a → Bool
+
+module _ {a : Type} {{_ : Ord a}} where
+  postulate
+    member    : a → Set a → Bool
+
+    empty     : Set a
+    insert    : a → Set a → Set a
+    delete    : a → Set a → Set a
+    fromList  : List a → Set a
+
+    map          : ∀ {b} {{_ : Ord b}} → (a → b) → Set a → Set b
+    union        : Set a → Set a → Set a
+    intersection : Set a → Set a → Set a
+    difference   : Set a → Set a → Set a
+    filter       : (a → Bool) → Set a → Set a
+
+    isSubsetOf   : Set a → Set a → Bool
+
+    prop-member-null
+      : ∀ (s : Set a)
+          (_ : ∀ (x : a) → member x s ≡ False)
+      → null s ≡ True
+
+    prop-null→empty
+      : ∀ (s : Set a)
+      → null s ≡ True
+      → s ≡ empty
+
+    prop-equality
+      : ∀ {s1 s2 : Set a}
+      → (∀ (x : a) → member x s1 ≡ member x s2)
+      → s1 ≡ s2
+
+    prop-member-empty
+      : ∀ (x : a)
+      → member x empty ≡ False
+
+    prop-member-insert
+      : ∀ (x xi : a) (s : Set a)
+      → member x (insert xi s)
+        ≡ (if (x == xi) then True else member x s)
+
+    prop-member-delete
+      : ∀ (x xi : a) (s : Set a)
+      → member x (delete xi s)
+        ≡ (if (x == xi) then False else member x s)
+
+    prop-member-toAscList
+      : ∀ (x : a) (s : Set a)
+      → (elem x ∘ toAscList) s ≡ member x s
+
+    prop-member-fromList
+      : ∀ (x : a) (xs : List a)
+      → member x (fromList xs)
+        ≡ elem x xs
+
+    prop-member-union
+      : ∀ (x : a) (s1 s2 : Set a)
+      → member x (union s1 s2)
+        ≡ (member x s1 || member x s2)
+
+    prop-member-intersection    
+      : ∀ (x : a) (s1 s2 : Set a)
+      → member x (intersection s1 s2)
+        ≡ (member x s1 && member x s2)
+
+    prop-member-difference    
+      : ∀ (x : a) (s1 s2 : Set a)
+      → member x (difference s1 s2)
+        ≡ (member x s1 && not (member x s2))
+    
+    prop-member-filter    
+      : ∀ (x : a) (p : a → Bool) (s : Set a)
+      → member x (filter p s)
+        ≡ (p x && member x s)
+
+    prop-isSubsetOf→intersection
+      : ∀ (s1 s2 : Set a)
+      → isSubsetOf s1 s2 ≡ True
+      → intersection s1 s2 ≡ s1
+
+    prop-intersection→isSubsetOf
+      : ∀ (s1 s2 : Set a)
+      → intersection s1 s2 ≡ s1
+      → isSubsetOf s1 s2 ≡ True
+
+  singleton : a → Set a
+  singleton = λ x → insert x empty
+
+  disjoint : Set a → Set a → Bool
+  disjoint m = null ∘ intersection m
+
+foldMap' : ∀ {{_ : Monoid b}} → (a → b) → Set a → b
+foldMap' f = foldMap f ∘ toAscList
+
+postulate
+  prop-member-map
+    : ∀ {a b} {{_ : Ord a}} {{_ : Ord b}}
+      (x : a) (s : Set a) (f : a → b)
+    → member (f x) (map f s) ≡ member x s
+
+instance
+  iSetFoldable : Foldable Set
+  iSetFoldable =
+    record {DefaultFoldable (record {foldMap = foldMap'})}
+
+  iSetSemigroup : {{Ord a}} → Semigroup (Set a)
+  iSetSemigroup ._<>_ = union
+
+  iSetMonoid : {{Ord a}} → Monoid (Set a)
+  iSetMonoid = record {DefaultMonoid (record {mempty = empty})}
diff --git a/lib/containers/agda/Test/Agda2Hs/Data/Map.agda b/lib/containers/agda/Test/Agda2Hs/Data/Map.agda
new file mode 100644
index 00000000..a2a30838
--- /dev/null
+++ b/lib/containers/agda/Test/Agda2Hs/Data/Map.agda
@@ -0,0 +1,35 @@
+module Test.Agda2Hs.Data.Map where
+
+open import Haskell.Prelude
+
+open import Data.Map using (Map)
+import Data.Map as Map
+
+{-----------------------------------------------------------------------------
+    Test definitions
+    for exercising Data.Map
+------------------------------------------------------------------------------}
+test0 : Map Nat String
+test0 = Map.fromList ((1 , "Hello") ∷ (2 , "Map") ∷ [])
+
+test1 : Map Nat String
+test1 = Map.filter (λ x → length x > 3) test0
+
+test2 : Map Nat String
+test2 = Map.singleton 1 "Data"
+
+test3 : Map Nat String
+test3 = Map.unionWith _<>_ test0 (Map.unionWith _<>_ test1 test2)
+
+test4 : Map Nat String
+test4 = Map.intersectionWith _<>_ test2 test3
+
+testLookup0 : Maybe String
+testLookup0 = Map.lookup 1 test4
+
+{-# COMPILE AGDA2HS test0 #-}
+{-# COMPILE AGDA2HS test1 #-}
+{-# COMPILE AGDA2HS test2 #-}
+{-# COMPILE AGDA2HS test3 #-}
+{-# COMPILE AGDA2HS test4 #-}
+{-# COMPILE AGDA2HS testLookup0 #-}
diff --git a/lib/containers/agda/Test/Agda2Hs/Data/Set.agda b/lib/containers/agda/Test/Agda2Hs/Data/Set.agda
new file mode 100644
index 00000000..d040de82
--- /dev/null
+++ b/lib/containers/agda/Test/Agda2Hs/Data/Set.agda
@@ -0,0 +1,35 @@
+module Test.Agda2Hs.Data.Set where
+
+open import Haskell.Prelude
+
+open import Data.Set using (Set)
+import Data.Set as Set
+
+{-----------------------------------------------------------------------------
+    Test definitions
+    for exercising Data.Set
+------------------------------------------------------------------------------}
+test0 : Set String
+test0 = Set.fromList ("Hello" ∷ "Set" ∷ [])
+
+test1 : Set String
+test1 = Set.filter (λ x → length x > 3) test0
+
+test2 : Set String
+test2 = Set.singleton "Data"
+
+test3 : Set String
+test3 = Set.union test0 (Set.union test1 test2)
+
+test4 : Set String
+test4 = Set.intersection test2 test3
+
+testBool0 : Bool
+testBool0 = Set.isSubsetOf test2 test4
+
+{-# COMPILE AGDA2HS test0 #-}
+{-# COMPILE AGDA2HS test1 #-}
+{-# COMPILE AGDA2HS test2 #-}
+{-# COMPILE AGDA2HS test3 #-}
+{-# COMPILE AGDA2HS test4 #-}
+{-# COMPILE AGDA2HS testBool0 #-}
diff --git a/lib/containers/agda/containers.agda b/lib/containers/agda/containers.agda
new file mode 100644
index 00000000..a8ecac7a
--- /dev/null
+++ b/lib/containers/agda/containers.agda
@@ -0,0 +1,7 @@
+-- This file imports all modules from the library.
+
+import Data.Map
+import Data.Set
+
+import Test.Agda2Hs.Data.Map
+import Test.Agda2Hs.Data.Set
diff --git a/lib/containers/agda2hs-libraries b/lib/containers/agda2hs-libraries
new file mode 100644
index 00000000..7bd962ce
--- /dev/null
+++ b/lib/containers/agda2hs-libraries
@@ -0,0 +1 @@
+./../base/base.agda-lib
diff --git a/lib/containers/containers-prop.cabal b/lib/containers/containers-prop.cabal
new file mode 100644
index 00000000..f4d1fd86
--- /dev/null
+++ b/lib/containers/containers-prop.cabal
@@ -0,0 +1,55 @@
+cabal-version:      3.0
+name:               containers-prop
+build-type:         Simple
+version:            0.8
+synopsis:           Properties of containers, machine-checked
+description:
+  This package collects properties about data structures from the
+  [containers](https://hackage.haskell.org/package/containers) package,
+  such as `Data.Set` and `Data.Map`.
+  .
+  Basic properties are postulated, hoping that the implementation
+  satisfies them.
+  However, more complicated properties are proven from the basic properties.
+  These proofs are formalized and machine-checked
+  using [agda2hs](https://hackage.haskell.org/package/agda2hs).
+
+homepage:           https://github.com/agda/agda2hs
+license:            BSD-3-Clause
+author:             Heinrich Apfelmus
+maintainer:         apfelmus@quantentunnel.de
+copyright:          2025 Cardano Foundation
+category:           Language
+extra-doc-files:    CHANGELOG.md
+extra-source-files:
+  agda/**/*.agda
+  containers.agda-lib
+  generate-haskell.sh
+
+common language
+  default-language: Haskell2010
+
+common opts-lib
+  ghc-options:
+    -Wall -Wcompat -Wincomplete-record-updates
+    -Wno-incomplete-uni-patterns -Wno-redundant-constraints
+    -Wno-unused-matches -Wno-unused-imports
+
+library
+  import:          language, opts-lib
+  hs-source-dirs:  haskell
+  build-depends:
+    , base        >=4.13 && <4.21
+    , containers  >=0.6  && <0.9
+
+  exposed-modules:
+
+  --    Data.Maps.Maybe
+  --    Data.Map.Prop
+  --    Data.Map.Set
+  other-modules:
+    Test.Agda2Hs.Data.Map
+    Test.Agda2Hs.Data.Set
+  autogen-modules:
+    Test.Agda2Hs.Data.Map
+    Test.Agda2Hs.Data.Set
diff --git a/lib/containers/containers.agda-lib b/lib/containers/containers.agda-lib
new file mode 100644
index 00000000..29dd8e3e
--- /dev/null
+++ b/lib/containers/containers.agda-lib
@@ -0,0 +1,5 @@
+name: containers
+include: agda
+depend:
+  base
+flags: --erasure --no-import-sorts
diff --git a/lib/containers/generate-haskell.sh b/lib/containers/generate-haskell.sh
new file mode 100755
index 00000000..279207d4
--- /dev/null
+++ b/lib/containers/generate-haskell.sh
@@ -0,0 +1,9 @@
+#!/bin/sh
+ROOT=containers.agda
+AGDA2HS="cabal run agda2hs --"
+${AGDA2HS} \
+    --local-interfaces \
+    --no-default-libraries \
+    --library-file ./agda2hs-libraries \
+    -o ./haskell/ \
+    ./agda/${ROOT}