Lattice.agda

@@ -145,14 +145,3 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where
         isLattice : IsLattice A _≈_ _⊔_ _⊓_
 
     open IsLattice isLattice public
-
-record FiniteHeightLattice {a} (A : Set a) : Set (lsuc a) where
-    field
-        height : ℕ
-        _≈_ : A → A → Set a
-        _⊔_ : A → A → A
-        _⊓_ : A → A → A
-
-        isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
-
-    open IsFiniteHeightLattice isFiniteHeightLattice public

Lattice/FiniteMap.agda

@@ -1,78 +0,0 @@
-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 _⊔ℓ_)
-open import Data.List using (List)
-
-module Lattice.FiniteMap {a b : Level} (A : Set a) (B : Set b)
-    (_≈₂_ : B → B → Set b)
-    (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
-    (≡-dec-A : Decidable (_≡_ {a} {A}))
-    (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
-
-open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
-    using (Map; ⊔-equal-keys; ⊓-equal-keys)
-    renaming
-        ( _≈_ to _≈ᵐ_
-        ; _⊔_ to _⊔ᵐ_
-        ; _⊓_ to _⊓ᵐ_
-        ; ≈-equiv to ≈ᵐ-equiv
-        ; ≈-⊔-cong to ≈ᵐ-⊔ᵐ-cong
-        ; ⊔-assoc to ⊔ᵐ-assoc
-        ; ⊔-comm to ⊔ᵐ-comm
-        ; ⊔-idemp to ⊔ᵐ-idemp
-        ; ≈-⊓-cong to ≈ᵐ-⊓ᵐ-cong
-        ; ⊓-assoc to ⊓ᵐ-assoc
-        ; ⊓-comm to ⊓ᵐ-comm
-        ; ⊓-idemp to ⊓ᵐ-idemp
-        ; absorb-⊔-⊓ to absorb-⊔ᵐ-⊓ᵐ
-        ; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
-        )
-open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
-open import Equivalence
-
-module _ (ks : List A) where
-    FiniteMap : Set (a ⊔ℓ b)
-    FiniteMap = Σ Map (λ m → Map.keys m ≡ ks)
-
-    _≈_ : FiniteMap → FiniteMap → Set (a ⊔ℓ b)
-    _≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂
-
-    _⊔_ : FiniteMap → FiniteMap → FiniteMap
-    _⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = (m₁ ⊔ᵐ m₂ , trans (sym (⊔-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks)))) km₁≡ks)
-
-    _⊓_ : FiniteMap → FiniteMap → FiniteMap
-    _⊓_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = (m₁ ⊓ᵐ m₂ , trans (sym (⊓-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks)))) km₁≡ks)
-
-    ≈-equiv : IsEquivalence FiniteMap _≈_
-    ≈-equiv = record
-        { ≈-refl = λ {(m , _)} → IsEquivalence.≈-refl ≈ᵐ-equiv {m}
-        ; ≈-sym = λ {(m₁ , _)} {(m₂ , _)} → IsEquivalence.≈-sym ≈ᵐ-equiv {m₁} {m₂}
-        ; ≈-trans = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} → IsEquivalence.≈-trans ≈ᵐ-equiv {m₁} {m₂} {m₃}
-        }
-
-    isUnionSemilattice : IsSemilattice FiniteMap _≈_ _⊔_
-    isUnionSemilattice = record
-        { ≈-equiv = ≈-equiv
-        ; ≈-⊔-cong = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ → ≈ᵐ-⊔ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
-        ; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊔ᵐ-assoc m₁ m₂ m₃
-        ; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊔ᵐ-comm m₁ m₂
-        ; ⊔-idemp = λ (m , _) → ⊔ᵐ-idemp m
-        }
-
-    isIntersectSemilattice : IsSemilattice FiniteMap _≈_ _⊓_
-    isIntersectSemilattice = record
-        { ≈-equiv = ≈-equiv
-        ; ≈-⊔-cong = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ → ≈ᵐ-⊓ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
-        ; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊓ᵐ-assoc m₁ m₂ m₃
-        ; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊓ᵐ-comm m₁ m₂
-        ; ⊔-idemp = λ (m , _) → ⊓ᵐ-idemp m
-        }
-
-    isLattice : IsLattice FiniteMap _≈_ _⊔_ _⊓_
-    isLattice = record
-        { joinSemilattice = isUnionSemilattice
-        ; meetSemilattice = isIntersectSemilattice
-        ; absorb-⊔-⊓ = λ (m₁ , _) (m₂ , _) → absorb-⊔ᵐ-⊓ᵐ m₁ m₂
-        ; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂
-        }

Lattice/IterProd.agda

@@ -1,107 +0,0 @@
-open import Lattice
-
-module Lattice.IterProd {a} {A B : Set a}
-    (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
-    (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
-    (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B)
-    (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
-
-open import Agda.Primitive using (lsuc)
-open import Data.Nat using (ℕ; suc; _+_)
-open import Data.Product using (_×_)
-open import Utils using (iterate)
-
-open IsLattice lA renaming (FixedHeight to FixedHeight₁)
-open IsLattice lB renaming (FixedHeight to FixedHeight₂)
-
-IterProd : ℕ → Set a
-IterProd k = iterate k (λ t → A × t) B
-
--- To make iteration more convenient, package the definitions in Lattice
--- records, perform the recursion, and unpackage.
-
-private module _ where
-    BLattice : Lattice B
-    BLattice = record
-        { _≈_ = _≈₂_
-        ; _⊔_ = _⊔₂_
-        ; _⊓_ = _⊓₂_
-        ; isLattice = lB
-        }
-
-    IterProdLattice : ∀ {k : ℕ} → Lattice (IterProd k)
-    IterProdLattice {0} = BLattice
-    IterProdLattice {suc k'} = record
-        { _≈_ = _≈_
-        ; _⊔_ = _⊔_
-        ; _⊓_ = _⊓_
-        ; isLattice = isLattice
-        }
-        where
-            Right : Lattice (IterProd k')
-            Right = IterProdLattice {k'}
-
-            open import Lattice.Prod
-                _≈₁_ (Lattice._≈_ Right)
-                _⊔₁_ (Lattice._⊔_ Right)
-                _⊓₁_ (Lattice._⊓_ Right)
-                lA  (Lattice.isLattice Right)
-
-module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
-         (h₁ h₂ : ℕ)
-         (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
-
-    private module _ where
-        record FiniteHeightAndDecEq (A : Set a) : Set (lsuc a) where
-            field
-                height : ℕ
-                _≈_ : A → A → Set a
-                _⊔_ : A → A → A
-                _⊓_ : A → A → A
-
-                isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
-                ≈-dec : IsDecidable _≈_
-
-            open IsFiniteHeightLattice isFiniteHeightLattice public
-
-        BFiniteHeightLattice : FiniteHeightAndDecEq B
-        BFiniteHeightLattice = record
-            { height = h₂
-            ; _≈_ = _≈₂_
-            ; _⊔_ = _⊔₂_
-            ; _⊓_ = _⊓₂_
-            ; isFiniteHeightLattice = record
-                { isLattice = lB
-                ; fixedHeight = fhB
-                }
-            ; ≈-dec = ≈₂-dec
-            }
-
-        IterProdFiniteHeightLattice : ∀ {k : ℕ} → FiniteHeightAndDecEq (IterProd k)
-        IterProdFiniteHeightLattice {0} = BFiniteHeightLattice
-        IterProdFiniteHeightLattice {suc k'} = record
-            { height = h₁ + FiniteHeightAndDecEq.height Right
-            ; _≈_ = _≈_
-            ; _⊔_ = _⊔_
-            ; _⊓_ = _⊓_
-            ; isFiniteHeightLattice = isFiniteHeightLattice
-                ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
-                h₁ (FiniteHeightAndDecEq.height Right)
-                fhA (IsFiniteHeightLattice.fixedHeight (FiniteHeightAndDecEq.isFiniteHeightLattice Right))
-            ; ≈-dec = ≈-dec ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
-            }
-            where
-                Right = IterProdFiniteHeightLattice {k'}
-
-                open import Lattice.Prod
-                    _≈₁_ (FiniteHeightAndDecEq._≈_ Right)
-                    _⊔₁_ (FiniteHeightAndDecEq._⊔_ Right)
-                    _⊓₁_ (FiniteHeightAndDecEq._⊓_ Right)
-                    lA  (FiniteHeightAndDecEq.isLattice Right)
-
-    module _ (k : ℕ) where
-        open FiniteHeightAndDecEq (IterProdFiniteHeightLattice {k}) using (fixedHeight) public
-
--- Expose the computed definition in public.
-module _ (k : ℕ) where
-    open Lattice.Lattice (IterProdLattice {k}) public

Lattice/Map.agda

@@ -19,7 +19,6 @@ open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-ex
 open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Equivalence
-open import Utils using (Unique; push; empty; Unique-append; All¬-¬Any; All-x∈xs)
 
 open IsLattice lB using () renaming
     ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans
@@ -29,13 +28,35 @@ open IsLattice lB using () renaming
     ; absorb-⊔-⊓ to absorb-⊔₂-⊓₂; absorb-⊓-⊔ to absorb-⊓₂-⊔₂
     )
 
-private module ImplKeys where
 keys : List (A × B) → List A
 keys = map proj₁
 
+data Unique {c} {C : Set c} : List C → Set c where
+    empty : Unique []
+    push : ∀ {x : C} {xs : List C}
+        → All (λ x' → ¬ x ≡ x') xs
+        → Unique xs
+        → Unique (x ∷ xs)
+
+Unique-append : ∀ {c} {C : Set c} {x : C} {xs : List C} →
+                ¬ MemProp._∈_ x xs → Unique xs →  Unique (xs ++ (x ∷ []))
+Unique-append {c} {C} {x} {[]} _ _ = push [] empty
+Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') =
+    push (help x'≢) (Unique-append (λ x∈xs' → x∉xs (there x∈xs')) uxs')
+    where
+        x'≢x : ¬ x' ≡ x
+        x'≢x x'≡x = x∉xs (here (sym x'≡x))
+
+        help : {l : List C} → All (λ x'' → ¬ x' ≡ x'') l → All (λ x'' → ¬ x' ≡ x'') (l ++ (x ∷ []))
+        help {[]} _ = x'≢x ∷ []
+        help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es
+
+All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l
+All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
+All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
+
 private module _ where
     open MemProp using (_∈_)
-    open ImplKeys
 
     unique-not-in : ∀ {k : A} {v : B} {l : List (A × B)}  →
                     ¬ (All (λ k' → ¬ k ≡ k') (keys l) × (k , v) ∈ l)
@@ -87,7 +108,6 @@ private module ImplRelation where
 private module ImplInsert (f : B → B → B) where
     open import Data.List using (map)
     open MemProp using (_∈_)
-    open ImplKeys
 
     private
         _∈k_ : A → List (A × B) → Set a
@@ -133,20 +153,6 @@ private module ImplInsert (f : B → B → B) where
     ...   | yes k∈kl rewrite insert-keys-∈ {v = v} k∈kl = u
     ...   | no k∉kl rewrite sym (insert-keys-∉ {v = v} k∉kl) = Unique-append k∉kl u
 
-    union-subset-keys : ∀ {l₁ l₂ : List (A × B)} →
-                        All (λ k → k ∈k l₂) (keys l₁) →
-                        keys l₂ ≡ keys (union l₁ l₂)
-    union-subset-keys {[]} _ = refl
-    union-subset-keys {(k , v) ∷ l₁'} (k∈kl₂ ∷ kl₁'⊆kl₂)
-        rewrite union-subset-keys kl₁'⊆kl₂ =
-        insert-keys-∈ k∈kl₂
-
-    union-equal-keys : ∀ {l₁ l₂ : List (A × B)} →
-                       keys l₁ ≡ keys l₂ → keys l₁ ≡ keys (union l₁ l₂)
-    union-equal-keys {l₁} {l₂} kl₁≡kl₂
-        with subst (λ l → All (λ k → k ∈ l) (keys l₁)) kl₁≡kl₂ (All-x∈xs (keys l₁))
-    ...   | kl₁⊆kl₂ = trans kl₁≡kl₂ (union-subset-keys {l₁} {l₂} kl₁⊆kl₂)
-
     union-preserves-Unique : ∀ (l₁ l₂ : List (A × B)) →
                              Unique (keys l₂) → Unique (keys (union l₁ l₂))
     union-preserves-Unique [] l₂ u₂ = u₂
@@ -360,29 +366,6 @@ private module ImplInsert (f : B → B → B) where
             let (k∈kl₁ , k∈kxs) = restrict-needs-both k∈l₁xs
             in (k∈kl₁ , there k∈kxs)
 
-    restrict-subset-keys : ∀ {l₁ l₂ : List (A × B)} →
-                           All (λ k → k ∈k l₁) (keys l₂) →
-                           keys l₂ ≡ keys (restrict l₁ l₂)
-    restrict-subset-keys {l₁} {[]} _ = refl
-    restrict-subset-keys {l₁} {(k , v) ∷ l₂'} (k∈kl₁ ∷ kl₂'⊆kl₁)
-        with ∈k-dec k l₁
-    ...   | no k∉kl₁ = ⊥-elim (k∉kl₁ k∈kl₁)
-    ...   | yes _ rewrite restrict-subset-keys {l₁} {l₂'} kl₂'⊆kl₁ = refl
-
-    restrict-equal-keys : ∀ {l₁ l₂ : List (A × B)} →
-                          keys l₁ ≡ keys l₂ →
-                          keys l₁ ≡ keys (restrict l₁ l₂)
-    restrict-equal-keys {l₁} {l₂} kl₁≡kl₂
-        with subst (λ l → All (λ k → k ∈ l) (keys l₂)) (sym kl₁≡kl₂) (All-x∈xs (keys l₂))
-    ...   | kl₂⊆kl₁ = trans kl₁≡kl₂ (restrict-subset-keys {l₁} {l₂} kl₂⊆kl₁)
-
-    intersect-equal-keys : ∀ {l₁ l₂ : List (A × B)} →
-                           keys l₁ ≡ keys l₂ →
-                           keys l₁ ≡ keys (intersect l₁ l₂)
-    intersect-equal-keys {l₁} {l₂} kl₁≡kl₂
-        rewrite restrict-equal-keys (trans kl₁≡kl₂ (updates-keys {l₁} {l₂}))
-        rewrite updates-keys {l₁} {l₂} = refl
-
     restrict-preserves-∉₁ : ∀ {k : A} {l₁ l₂ : List (A × B)} →
                             ¬ k ∈k l₁ → ¬ k ∈k restrict l₁ l₂
     restrict-preserves-∉₁ {k} {l₁} {l₂} k∉kl₁ k∈kl₁l₂ =
@@ -465,16 +448,13 @@ private module ImplInsert (f : B → B → B) where
 
 
 Map : Set (a ⊔ℓ b)
-Map = Σ (List (A × B)) (λ l → Unique (ImplKeys.keys l))
-
-keys : Map → List A
-keys (kvs , _) = ImplKeys.keys kvs
+Map = Σ (List (A × B)) (λ l → Unique (keys l))
 
 _∈_ : (A × B) → Map → Set (a ⊔ℓ b)
 _∈_ p (kvs , _) = MemProp._∈_ p kvs
 
 _∈k_ : A → Map → Set a
-_∈k_ k m = MemProp._∈_ k (keys m)
+_∈k_ k (kvs , _) = MemProp._∈_ k (keys kvs)
 
 Map-functional : ∀ {k : A} {v v' : B} {m : Map} → (k , v) ∈ m → (k , v') ∈ m → v ≡ v'
 Map-functional {m = (l , ul)} k,v∈m k,v'∈m = ListAB-functional ul k,v∈m k,v'∈m
@@ -512,8 +492,8 @@ data Expr : Set (a ⊔ℓ b) where
     _∪_ : Expr → Expr → Expr
     _∩_ : Expr → Expr → Expr
 
-open ImplInsert _⊔₂_ using (union-preserves-Unique; union-equal-keys) renaming (insert to insert-impl; union to union-impl)
-open ImplInsert _⊓₂_ using (intersect-preserves-Unique; intersect-equal-keys) renaming (intersect to intersect-impl)
+open ImplInsert _⊔₂_ using (union-preserves-Unique) renaming (insert to insert-impl; union to union-impl)
+open ImplInsert _⊓₂_ using (intersect-preserves-Unique) renaming (intersect to intersect-impl)
 
 _⊔_ : Map → Map → Map
 _⊔_ (kvs₁ , _) (kvs₂ , uks₂) = (union-impl kvs₁ kvs₂ , union-preserves-Unique kvs₁ kvs₂ uks₂)
@@ -573,8 +553,6 @@ Expr-Provenance k (e₁ ∩ e₂) k∈ke₁e₂
 ...   | no k∉ke₁ | yes k∈ke₂ = ⊥-elim (intersect-preserves-∉₁ {l₂ = proj₁ ⟦ e₂ ⟧} k∉ke₁ k∈ke₁e₂)
 ...   | no k∉ke₁ | no k∉ke₂ = ⊥-elim (intersect-preserves-∉₂ {l₁ = proj₁ ⟦ e₁ ⟧} k∉ke₂ k∈ke₁e₂)
 
-module _ (≈₂-dec : ∀ (b₁ b₂ : B) → Dec (b₁ ≈₂ b₂)) where
-    private module _ where
 data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where
     extra : (k : A) → k ∈k m₁ → ¬ k ∈k m₂ → SubsetInfo m₁ m₂
     mismatch : (k : A) (v₁ v₂ : B) → (k , v₁) ∈ m₁ → (k , v₂) ∈ m₂ → ¬ v₁ ≈₂ v₂ → SubsetInfo m₁ m₂
@@ -592,6 +570,7 @@ module _ (≈₂-dec : ∀ (b₁ b₂ : B) → Dec (b₁ ≈₂ b₂)) where
         in v₁̷≈v₂ (subst (λ v'' → v₁ ≈₂ v'') (Map-functional {k} {v'} {v₂} {m₂} k,v'∈m₂ k,v₂∈m₂) v₁≈v')) -- for some reason, can't just use subst...
 SubsetInfo-to-dec (fine m₁⊆m₂) = yes m₁⊆m₂
 
+module _ (≈₂-dec : ∀ (b₁ b₂ : B) → Dec (b₁ ≈₂ b₂)) where
     compute-SubsetInfo : ∀ m₁ m₂ → SubsetInfo m₁ m₂
     compute-SubsetInfo ([] , _) m₂ = fine (λ k v ())
     compute-SubsetInfo m₁@((k , v) ∷ xs₁ , push k≢xs₁ uxs₁) m₂@(l₂ , u₂)
@@ -881,9 +860,3 @@ isLattice = record
     ; absorb-⊔-⊓ = absorb-⊔-⊓
     ; absorb-⊓-⊔ = absorb-⊓-⊔
     }
-
-⊔-equal-keys : ∀ {m₁ m₂ : Map} → keys m₁ ≡ keys m₂ → keys m₁ ≡ keys (m₁ ⊔ m₂)
-⊔-equal-keys km₁≡km₂ = union-equal-keys km₁≡km₂
-
-⊓-equal-keys : ∀ {m₁ m₂ : Map} → keys m₁ ≡ keys m₂ → keys m₁ ≡ keys (m₁ ⊓ m₂)
-⊓-equal-keys km₁≡km₂ = intersect-equal-keys km₁≡km₂

Lattice/Prod.agda

@@ -94,16 +94,6 @@ isLattice = record
         )
     }
 
-
-module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) where
-    ≈-dec : IsDecidable _≈_
-    ≈-dec (a₁ , b₁) (a₂ , b₂)
-        with ≈₁-dec a₁ a₂ | ≈₂-dec b₁ b₂
-    ...   | yes a₁≈a₂ | yes b₁≈b₂ = yes (a₁≈a₂ , b₁≈b₂)
-    ...   | no a₁̷≈a₂ | _ = no (λ (a₁≈a₂ , _) → a₁̷≈a₂ a₁≈a₂)
-    ...   | _ | no b₁̷≈b₂ = no (λ (_ , b₁≈b₂) → b₁̷≈b₂ b₁≈b₂)
-
-
 module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
          (h₁ h₂ : ℕ)
          (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where

Utils.agda

@@ -1,41 +0,0 @@
-module Utils where
-
-open import Data.Nat using (ℕ; suc)
-open import Data.List using (List; []; _∷_; _++_)
-open import Data.List.Membership.Propositional using (_∈_)
-open import Data.List.Relation.Unary.All using (All; []; _∷_; map)
-open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
-open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl)
-open import Relation.Nullary using (¬_)
-
-data Unique {c} {C : Set c} : List C → Set c where
-    empty : Unique []
-    push : ∀ {x : C} {xs : List C}
-        → All (λ x' → ¬ x ≡ x') xs
-        → Unique xs
-        → Unique (x ∷ xs)
-
-Unique-append : ∀ {c} {C : Set c} {x : C} {xs : List C} →
-                ¬ x ∈ xs → Unique xs →  Unique (xs ++ (x ∷ []))
-Unique-append {c} {C} {x} {[]} _ _ = push [] empty
-Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') =
-    push (help x'≢) (Unique-append (λ x∈xs' → x∉xs (there x∈xs')) uxs')
-    where
-        x'≢x : ¬ x' ≡ x
-        x'≢x x'≡x = x∉xs (here (sym x'≡x))
-
-        help : {l : List C} → All (λ x'' → ¬ x' ≡ x'') l → All (λ x'' → ¬ x' ≡ x'') (l ++ (x ∷ []))
-        help {[]} _ = x'≢x ∷ []
-        help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es
-
-All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l
-All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
-All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
-
-All-x∈xs : ∀ {a} {A : Set a} (xs : List A) → All (λ x → x ∈ xs) xs
-All-x∈xs [] = []
-All-x∈xs (x ∷ xs') = here refl ∷ map there (All-x∈xs xs')
-
-iterate : ∀ {a} {A : Set a} (n : ℕ) → (f : A → A) → A → A
-iterate 0 _ a = a
-iterate (suc n) f a = f (iterate n f a)