Merge tag 'upstream/0.17'

Upstream version 0.17

# gpg: Signature made Fri 23 Nov 2018 05:29:18 PM MST
# gpg:                using RSA key 9B917007AE030E36E4FC248B695B7AE4BF066240
# gpg:                issuer "spwhitton@spwhitton.name"
# gpg: Good signature from "Sean Whitton <spwhitton@spwhitton.name>" [ultimate]
# Primary key fingerprint: 8DC2 487E 51AB DD90 B5C4  753F 0F56 D055 3B6D 411B
#      Subkey fingerprint: 9B91 7007 AE03 0E36 E4FC  248B 695B 7AE4 BF06 6240

14 files changed, 1678 insertions, 762 deletions

diff --git a/src/Data/Vec/All.agda b/src/Data/Vec/All.agda
index 0dfe1b1..4c7f23e 100644
--- a/src/Data/Vec/All.agda
+++ b/src/Data/Vec/All.agda
@@ -6,16 +6,16 @@
 
 module Data.Vec.All where
 
-open import Data.Vec as Vec using (Vec; []; _∷_; zip)
-open import Data.Vec.Properties using (lookup-zip)
+open import Data.Nat using (zero; suc)
 open import Data.Fin using (Fin; zero; suc)
+open import Data.Product as Prod using (_,_)
+open import Data.Vec as Vec using (Vec; []; _∷_)
 open import Function using (_∘_)
 open import Level using (_⊔_)
-open import Data.Product using (uncurry)
 open import Relation.Nullary
 import Relation.Nullary.Decidable as Dec
-open import Relation.Unary using (Decidable) renaming (_⊆_ to _⋐_)
-open import Relation.Binary.PropositionalEquality using (subst)
+open import Relation.Unary
+open import Relation.Binary.PropositionalEquality as P using (subst)
 
 ------------------------------------------------------------------------
 -- All P xs means that all elements in xs satisfy P.
@@ -27,6 +27,9 @@ data All {a p} {A : Set a}
   []  : All P []
   _∷_ : ∀ {k x} {xs : Vec A k} (px : P x) (pxs : All P xs) → All P (x ∷ xs)
 
+------------------------------------------------------------------------
+-- Operations on All
+
 head : ∀ {a p} {A : Set a} {P : A → Set p} {k x} {xs : Vec A k} →
        All P (x ∷ xs) → P x
 head (px ∷ pxs) = px
@@ -41,23 +44,16 @@ lookup ()      []
 lookup zero    (px ∷ pxs) = px
 lookup (suc i) (px ∷ pxs) = lookup i pxs
 
-tabulate : ∀ {a p} {A : Set a} {P : A → Set p} {k} {xs : Vec A k} →
-           (∀ x → P x) → All P xs
-tabulate {xs = []}     hyp = []
-tabulate {xs = x ∷ xs} hyp = hyp x ∷ tabulate hyp
+tabulate : ∀ {a p} {A : Set a} {P : A → Set p} {k xs} →
+           (∀ i → P (Vec.lookup i xs)) → All P {k} xs
+tabulate {xs = []}    pxs = []
+tabulate {xs = _ ∷ _} pxs = pxs zero ∷ tabulate (pxs ∘ suc)
 
 map : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} {k} →
-      P ⋐ Q → All P {k} ⋐ All Q {k}
+      P ⊆ Q → All P {k} ⊆ All Q {k}
 map g []         = []
 map g (px ∷ pxs) = g px ∷ map g pxs
 
-all : ∀ {a p} {A : Set a} {P : A → Set p} {k} →
-      Decidable P → Decidable (All P {k})
-all p []       = yes []
-all p (x ∷ xs) with p x
-all p (x ∷ xs) | yes px = Dec.map′ (_∷_ px) tail (all p xs)
-all p (x ∷ xs) | no ¬px = no (¬px ∘ head)
-
 zipWith : ∀ {a b c p q r} {A : Set a} {B : Set b} {C : Set c} {_⊕_ : A → B → C}
           {P : A → Set p} {Q : B → Set q} {R : C → Set r} →
           (∀ {x y} → P x → Q y → R (x ⊕ y)) →
@@ -67,25 +63,36 @@ zipWith _⊕_ {xs = []}     {[]}     []         []         = []
 zipWith _⊕_ {xs = x ∷ xs} {y ∷ ys} (px ∷ pxs) (qy ∷ qys) =
   px ⊕ qy ∷ zipWith _⊕_ pxs qys
 
+zip : ∀ {a p q k} {A : Set a} {P : A → Set p} {Q : A → Set q} →
+      All P ∩ All Q ⊆ All (P ∩ Q) {k}
+zip ([] , [])             = []
+zip (px ∷ pxs , qx ∷ qxs) = (px , qx) ∷ zip (pxs , qxs)
+
+unzip : ∀ {a p q k} {A : Set a} {P : A → Set p} {Q : A → Set q} →
+        All (P ∩ Q) {k} ⊆ All P ∩ All Q
+unzip []           = [] , []
+unzip (pqx ∷ pqxs) = Prod.zip _∷_ _∷_ pqx (unzip pqxs)
 
 ------------------------------------------------------------------------
--- All₂ P xs ys means that every pointwise pair in xs ys satisfy P.
-
-data All₂ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p) :
-          ∀ {n} → Vec A n → Vec B n → Set (a ⊔ b ⊔ p) where
-    []  : All₂ P [] []
-    _∷_ : ∀ {n x y} {xs : Vec A n} {ys : Vec B n} →
-            P x y → All₂ P xs ys → All₂ P (x ∷ xs) (y ∷ ys)
-
-lookup₂ : ∀ {a b p} {A : Set a} {B : Set b} {P : A → B → Set p} {k}
-            {xs : Vec A k} {ys : Vec B k} →
-            ∀ i → All₂ P xs ys → P (Vec.lookup i xs) (Vec.lookup i ys)
-lookup₂ zero    (pxy ∷ _)    = pxy
-lookup₂ (suc i) (_   ∷ pxys) = lookup₂ i pxys
-
-map₂ : ∀ {a b p q} {A : Set a} {B : Set b}
-         {P : A → B → Set p} {Q : A → B → Set q} →
-         (∀ {x y} → P x y → Q x y) →
-         ∀ {k xs ys} → All₂ P {k} xs ys → All₂ Q {k} xs ys
-map₂ g [] = []
-map₂ g (pxy ∷ pxys) = g pxy  ∷ map₂ g pxys
+-- Properties of predicates preserved by All
+
+module _ {a p} {A : Set a} {P : A → Set p} where
+
+  all : ∀ {k} → Decidable P → Decidable (All P {k})
+  all P? []       = yes []
+  all P? (x ∷ xs) with P? x
+  ... | yes px = Dec.map′ (px ∷_) tail (all P? xs)
+  ... | no ¬px = no (¬px ∘ head)
+
+  universal : Universal P → ∀ {k} → Universal (All P {k})
+  universal u []       = []
+  universal u (x ∷ xs) = u x ∷ universal u xs
+
+  irrelevant : Irrelevant P → ∀ {k} → Irrelevant (All P {k})
+  irrelevant irr []           []           = P.refl
+  irrelevant irr (px₁ ∷ pxs₁) (px₂ ∷ pxs₂) =
+    P.cong₂ _∷_ (irr px₁ px₂) (irrelevant irr pxs₁ pxs₂)
+
+  satisfiable : Satisfiable P → ∀ {k} → Satisfiable (All P {k})
+  satisfiable (x , p) {zero}  = [] , []
+  satisfiable (x , p) {suc k} = Prod.map (x ∷_) (p ∷_) (satisfiable (x , p))
diff --git a/src/Data/Vec/All/Properties.agda b/src/Data/Vec/All/Properties.agda
index 3af19c7..4b1f735 100644
--- a/src/Data/Vec/All/Properties.agda
+++ b/src/Data/Vec/All/Properties.agda
@@ -6,194 +6,175 @@
 
 module Data.Vec.All.Properties where
 
-open import Data.Vec as Vec using (Vec; []; _∷_; zip; concat; _++_)
-open import Data.Vec.Properties using (map-id; lookup-zip)
+open import Data.List using ([]; _∷_)
+open import Data.List.All as List using ([]; _∷_)
 open import Data.Product as Prod using (_×_; _,_; uncurry; uncurry′)
-open import Data.Vec.All as All using (All; All₂; []; _∷_)
-open import Function
-open import Function.Inverse using (_↔_)
-open import Relation.Unary using () renaming (_⊆_ to _⋐_)
-open import Relation.Binary using (REL; Trans)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
-
--- Functions can be shifted between the predicate and the vector.
-
-All-map : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
-            {f : A → B} {k} {xs : Vec A k} →
-          All (P ∘ f) xs → All P (Vec.map f xs)
-All-map []         = []
-All-map (px ∷ pxs) = px ∷ All-map pxs
-
-map-All : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
-            {f : A → B} {k} {xs : Vec A k} →
-          All P (Vec.map f xs) → All (P ∘ f) xs
-map-All {xs = []}    []       = []
-map-All {xs = _ ∷ _} (px ∷ pxs) = px ∷ map-All pxs
-
--- A variant of All.map.
-
-gmap : ∀ {a b p q}
-         {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q}
-         {f : A → B} {k} →
-       P ⋐ Q ∘ f → All P {k} ⋐ All Q {k} ∘ Vec.map f
-gmap g = All-map ∘ All.map g
-
--- A variant of All-map for All₂.
-
-All₂-map : ∀ {a b c d p} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
-           {P : C → D → Set p}
-           {f₁ : A → C} {f₂ : B → D} {k} {xs : Vec A k} {ys : Vec B k} →
-           All₂ (λ x y → P (f₁ x) (f₂ y)) xs ys →
-           All₂ P (Vec.map f₁ xs) (Vec.map f₂ ys)
-All₂-map []         = []
-All₂-map (px ∷ pxs) = px ∷ All₂-map pxs
-
--- Abstract composition of binary relations lifted to All₂.
-
-comp : ∀ {a b c p q r} {A : Set a} {B : Set b} {C : Set c}
-       {P : A → B → Set p} {Q : B → C → Set q} {R : A → C → Set r} →
-       Trans P Q R → ∀ {k} → Trans (All₂ P {k}) (All₂ Q) (All₂ R)
-comp _⊙_ []           []           = []
-comp _⊙_ (pxy ∷ pxys) (qzx ∷ qzxs) = pxy ⊙ qzx ∷ comp _⊙_ pxys qzxs
+open import Data.Vec as Vec
+open import Data.Vec.All as All using (All; []; _∷_)
+open import Function using (_∘_; id)
+open import Function.Inverse using (_↔_; inverse)
+open import Relation.Unary using (Pred) renaming (_⊆_ to _⋐_)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; cong; cong₂; →-to-⟶)
 
 ------------------------------------------------------------------------
--- Variants of gmap for All₂.
+-- map
 
-module _ {a b c p q} {A : Set a} {B : Set b} {C : Set c} where
+module _ {a b p} {A : Set a} {B : Set b} {P : Pred B p} {f : A → B} where
 
-  -- A variant of gmap₂ shifting two functions from the binary
-  -- relation to the vector.
+  map⁺ : ∀ {n} {xs : Vec A n} → All (P ∘ f) xs → All P (map f xs)
+  map⁺ []         = []
+  map⁺ (px ∷ pxs) = px ∷ map⁺ pxs
 
-  gmap₂ : ∀ {d} {D : Set d} {P : A → B → Set p} {Q : C → D → Set q}
-            {f₁ : A → C} {f₂ : B → D} →
-          (∀ {x y} → P x y → Q (f₁ x) (f₂ y)) → ∀ {k xs ys} →
-          All₂ P {k} xs ys → All₂ Q {k} (Vec.map f₁ xs) (Vec.map f₂ ys)
-  gmap₂ g [] = []
-  gmap₂ g (pxy ∷ pxys) = g pxy ∷ gmap₂ g pxys
+  map⁻ : ∀ {n} {xs : Vec A n} → All P (map f xs) → All (P ∘ f) xs
+  map⁻ {xs = []}    []       = []
+  map⁻ {xs = _ ∷ _} (px ∷ pxs) = px ∷ map⁻ pxs
 
-  -- A variant of gmap₂ shifting only the first function from the binary
-  -- relation to the vector.
+-- A variant of All.map
 
-  gmap₂₁ : ∀ {P : A → B → Set p} {Q : C → B → Set q} {f : A → C} →
-           (∀ {x y} → P x y → Q (f x) y) → ∀ {k xs ys} →
-           All₂ P {k} xs ys → All₂ Q {k} (Vec.map f xs) ys
-  gmap₂₁ g [] = []
-  gmap₂₁ g (pxy ∷ pxys) = g pxy ∷ gmap₂₁ g pxys
-
-  -- A variant of gmap₂ shifting only the second function from the
-  -- binary relation to the vector.
-
-  gmap₂₂ : ∀ {P : A → B → Set p} {Q : A → C → Set q} {f : B → C} →
-           (∀ {x y} → P x y → Q x (f y)) → ∀ {k xs ys} →
-           All₂ P {k} xs ys → All₂ Q {k} xs (Vec.map f ys)
-  gmap₂₂ g [] = []
-  gmap₂₂ g (pxy ∷ pxys) = g pxy ∷ gmap₂₂ g pxys
+module _ {a b p q} {A : Set a} {B : Set b} {f : A → B}
+         {P : Pred A p} {Q : Pred B q} where
 
+  gmap : ∀ {n} → P ⋐ Q ∘ f → All P {n} ⋐ All Q {n} ∘ map f
+  gmap g = map⁺ ∘ All.map g
 
 ------------------------------------------------------------------------
--- All and _++_
+-- _++_
 
-module _ {a n p} {A : Set a} {P : A → Set p} where
+module _ {a n p} {A : Set a} {P : Pred A p} where
 
-  All-++⁺ : ∀ {m} {xs : Vec A m} {ys : Vec A n} →
-            All P xs → All P ys → All P (xs ++ ys)
-  All-++⁺ []         pys = pys
-  All-++⁺ (px ∷ pxs) pys = px ∷ All-++⁺ pxs pys
+  ++⁺ : ∀ {m} {xs : Vec A m} {ys : Vec A n} →
+        All P xs → All P ys → All P (xs ++ ys)
+  ++⁺ []         pys = pys
+  ++⁺ (px ∷ pxs) pys = px ∷ ++⁺ pxs pys
 
-  All-++ˡ⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
-          All P (xs ++ ys) → All P xs
-  All-++ˡ⁻ []       _          = []
-  All-++ˡ⁻ (x ∷ xs) (px ∷ pxs) = px ∷ All-++ˡ⁻ xs pxs
+  ++ˡ⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
+         All P (xs ++ ys) → All P xs
+  ++ˡ⁻ []       _          = []
+  ++ˡ⁻ (x ∷ xs) (px ∷ pxs) = px ∷ ++ˡ⁻ xs pxs
 
-  All-++ʳ⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
-          All P (xs ++ ys) → All P ys
-  All-++ʳ⁻ []       pys        = pys
-  All-++ʳ⁻ (x ∷ xs) (px ∷ pxs) = All-++ʳ⁻ xs pxs
+  ++ʳ⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
+         All P (xs ++ ys) → All P ys
+  ++ʳ⁻ []       pys        = pys
+  ++ʳ⁻ (x ∷ xs) (px ∷ pxs) = ++ʳ⁻ xs pxs
 
-  All-++⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
+  ++⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
         All P (xs ++ ys) → All P xs × All P ys
-  All-++⁻ []       p          = [] , p
-  All-++⁻ (x ∷ xs) (px ∷ pxs) = Prod.map (px ∷_) id (All-++⁻ _ pxs)
+  ++⁻ []       p          = [] , p
+  ++⁻ (x ∷ xs) (px ∷ pxs) = Prod.map₁ (px ∷_) (++⁻ _ pxs)
 
-  All-++⁺∘++⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
-                (p : All P (xs ++ ys)) →
-                uncurry′ All-++⁺ (All-++⁻ xs p) ≡ p
-  All-++⁺∘++⁻ []       p          = P.refl
-  All-++⁺∘++⁻ (x ∷ xs) (px ∷ pxs) = P.cong (px ∷_) (All-++⁺∘++⁻ xs pxs)
+  ++⁺∘++⁻ : ∀ {m} (xs : Vec A m) {ys : Vec A n} →
+            (p : All P (xs ++ ys)) →
+            uncurry′ ++⁺ (++⁻ xs p) ≡ p
+  ++⁺∘++⁻ []       p          = refl
+  ++⁺∘++⁻ (x ∷ xs) (px ∷ pxs) = cong (px ∷_) (++⁺∘++⁻ xs pxs)
 
-  All-++⁻∘++⁺ : ∀ {m} {xs : Vec A m} {ys : Vec A n} →
-                (p : All P xs × All P ys) →
-                All-++⁻ xs (uncurry All-++⁺ p) ≡ p
-  All-++⁻∘++⁺ ([]       , pys) = P.refl
-  All-++⁻∘++⁺ (px ∷ pxs , pys) rewrite All-++⁻∘++⁺ (pxs , pys) = P.refl
+  ++⁻∘++⁺ : ∀ {m} {xs : Vec A m} {ys : Vec A n} →
+            (p : All P xs × All P ys) →
+            ++⁻ xs (uncurry ++⁺ p) ≡ p
+  ++⁻∘++⁺ ([]       , pys) = refl
+  ++⁻∘++⁺ (px ∷ pxs , pys) rewrite ++⁻∘++⁺ (pxs , pys) = refl
 
   ++↔ : ∀ {m} {xs : Vec A m} {ys : Vec A n} →
         (All P xs × All P ys) ↔ All P (xs ++ ys)
-  ++↔ {xs = xs} = record
-    { to         = P.→-to-⟶ $ uncurry All-++⁺
-    ; from       = P.→-to-⟶ $ All-++⁻ xs
-    ; inverse-of = record
-      { left-inverse-of  = All-++⁻∘++⁺
-      ; right-inverse-of = All-++⁺∘++⁻ xs
-      }
-    }
+  ++↔ {xs = xs} = inverse (uncurry ++⁺) (++⁻ xs) ++⁻∘++⁺ (++⁺∘++⁻ xs)
 
 ------------------------------------------------------------------------
--- All₂ and _++_
-
-module _ {a b n p} {A : Set a} {B : Set b} {_~_ : REL A B p} where
+-- concat
 
-  All₂-++⁺ : ∀ {m} {ws : Vec A m} {xs} {ys : Vec A n} {zs} →
-           All₂ _~_ ws xs → All₂ _~_ ys zs →
-           All₂ _~_ (ws ++ ys) (xs ++ zs)
-  All₂-++⁺ []            ys~zs = ys~zs
-  All₂-++⁺ (w~x ∷ ws~xs) ys~zs = w~x ∷ (All₂-++⁺ ws~xs ys~zs)
+module _ {a m p} {A : Set a} {P : Pred A p} where
 
-  All₂-++ˡ⁻ : ∀ {m} (ws : Vec A m) xs {ys : Vec A n} {zs} →
-           All₂ _~_ (ws ++ ys) (xs ++ zs) → All₂ _~_ ws xs
-  All₂-++ˡ⁻ []       []        _                    = []
-  All₂-++ˡ⁻ (w ∷ ws) (x ∷ xs) (w~x ∷ ps) = w~x ∷ All₂-++ˡ⁻ ws xs ps
+  concat⁺ : ∀ {n} {xss : Vec (Vec A m) n} →
+            All (All P) xss → All P (concat xss)
+  concat⁺ []           = []
+  concat⁺ (pxs ∷ pxss) = ++⁺ pxs (concat⁺ pxss)
 
-  All₂-++ʳ⁻ : ∀ {m} (ws : Vec A m) (xs : Vec B m) {ys : Vec A n} {zs} →
-           All₂ _~_ (ws ++ ys) (xs ++ zs) → All₂ _~_ ys zs
-  All₂-++ʳ⁻ [] [] ys~zs = ys~zs
-  All₂-++ʳ⁻ (w ∷ ws) (x ∷ xs) (_ ∷ ps) = All₂-++ʳ⁻ ws xs ps
-
-  All₂-++⁻ : ∀ {m} (ws : Vec A m) (xs : Vec B m) {ys : Vec A n} {zs} →
-           All₂ _~_ (ws ++ ys) (xs ++ zs) →
-           All₂ _~_ ws xs × All₂ _~_ ys zs
-  All₂-++⁻ ws xs ps = All₂-++ˡ⁻ ws xs ps , All₂-++ʳ⁻ ws xs ps
+  concat⁻ : ∀ {n} (xss : Vec (Vec A m) n) →
+            All P (concat xss) → All (All P) xss
+  concat⁻ []         []   = []
+  concat⁻ (xs ∷ xss) pxss = ++ˡ⁻ xs pxss ∷ concat⁻ xss (++ʳ⁻ xs pxss)
 
 ------------------------------------------------------------------------
--- All and concat
+-- toList
 
-module _ {a m p} {A : Set a} {P : A → Set p} where
+module _ {a p} {A : Set a} {P : A → Set p} where
 
-  All-concat⁺ : ∀ {n} {xss : Vec (Vec A m) n} →
-                  All (All P) xss → All P (concat xss)
-  All-concat⁺ [] = []
-  All-concat⁺ (pxs ∷ pxss) = All-++⁺ pxs (All-concat⁺ pxss)
+  toList⁺ : ∀ {n} {xs : Vec A n} → List.All P (toList xs) → All P xs
+  toList⁺ {xs = []}     []         = []
+  toList⁺ {xs = x ∷ xs} (px ∷ pxs) = px ∷ toList⁺ pxs
 
-  All-concat⁻ : ∀ {n} (xss : Vec (Vec A m) n) →
-                  All P (concat xss) → All (All P) xss
-  All-concat⁻ [] [] = []
-  All-concat⁻ (xs ∷ xss) pxss = All-++ˡ⁻ xs pxss ∷ All-concat⁻ xss (All-++ʳ⁻ xs pxss)
+  toList⁻ : ∀ {n} {xs : Vec A n} → All P xs → List.All P (toList xs)
+  toList⁻ []         = []
+  toList⁻ (px ∷ pxs) = px ∷ toList⁻ pxs
 
 ------------------------------------------------------------------------
--- All₂ and concat
+-- fromList
 
-module _ {a b m p} {A : Set a} {B : Set b} {_~_ : REL A B p} where
+module _ {a p} {A : Set a} {P : A → Set p} where
 
-  All₂-concat⁺ : ∀ {n} {xss : Vec (Vec A m) n} {yss} →
-                   All₂ (All₂ _~_) xss yss →
-                   All₂ _~_ (concat xss) (concat yss)
-  All₂-concat⁺ [] = []
-  All₂-concat⁺ (xs~ys ∷ ps) = All₂-++⁺ xs~ys (All₂-concat⁺ ps)
+  fromList⁺ : ∀ {xs} → List.All P xs → All P (fromList xs)
+  fromList⁺ []         = []
+  fromList⁺ (px ∷ pxs) = px ∷ fromList⁺ pxs
 
-  All₂-concat⁻ : ∀ {n} (xss : Vec (Vec A m) n) yss →
-                   All₂ _~_ (concat xss) (concat yss) →
-                   All₂ (All₂ _~_) xss yss
-  All₂-concat⁻ []         []         [] = []
-  All₂-concat⁻ (xs ∷ xss) (ys ∷ yss) ps =
-    All₂-++ˡ⁻ xs ys ps ∷ All₂-concat⁻ xss yss (All₂-++ʳ⁻ xs ys ps)
+  fromList⁻ : ∀ {xs} → All P (fromList xs) → List.All P xs
+  fromList⁻ {[]}     []         = []
+  fromList⁻ {x ∷ xs} (px ∷ pxs) = px ∷ (fromList⁻ pxs)
 
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 0.16
+
+All-map     = map⁺
+{-# WARNING_ON_USAGE All-map
+"Warning: All-map was deprecated in v0.16.
+Please use map⁺ instead."
+#-}
+map-All     = map⁻
+{-# WARNING_ON_USAGE map-All
+"Warning: map-All was deprecated in v0.16.
+Please use map⁻ instead."
+#-}
+All-++⁺     = ++⁺
+{-# WARNING_ON_USAGE All-++⁺
+"Warning: All-++⁺ was deprecated in v0.16.
+Please use ++⁺ instead."
+#-}
+All-++ˡ⁻    = ++ˡ⁻
+{-# WARNING_ON_USAGE All-++ˡ⁻
+"Warning: All-++ˡ⁻ was deprecated in v0.16.
+Please use ++ˡ⁻ instead."
+#-}
+All-++ʳ⁻    = ++ʳ⁻
+{-# WARNING_ON_USAGE All-++ʳ⁻
+"Warning: All-++ʳ⁻ was deprecated in v0.16.
+Please use ++ʳ⁻ instead."
+#-}
+All-++⁻     = ++⁻
+{-# WARNING_ON_USAGE All-++⁻
+"Warning: All-++⁻ was deprecated in v0.16.
+Please use ++⁻ instead."
+#-}
+All-++⁺∘++⁻ = ++⁺∘++⁻
+{-# WARNING_ON_USAGE All-++⁺∘++⁻
+"Warning: All-++⁺∘++⁻ was deprecated in v0.16.
+Please use ++⁺∘++⁻ instead."
+#-}
+All-++⁻∘++⁺ = ++⁻∘++⁺
+{-# WARNING_ON_USAGE All-++⁻∘++⁺
+"Warning: All-++⁻∘++⁺ was deprecated in v0.16.
+Please use ++⁻∘++⁺ instead."
+#-}
+All-concat⁺ = concat⁺
+{-# WARNING_ON_USAGE All-concat⁺
+"Warning: All-concat⁺ was deprecated in v0.16.
+Please use concat⁺ instead."
+#-}
+All-concat⁻ = concat⁻
+{-# WARNING_ON_USAGE All-concat⁻
+"Warning: All-concat⁻ was deprecated in v0.16.
+Please use concat⁻ instead."
+#-}
diff --git a/src/Data/Vec/Any.agda b/src/Data/Vec/Any.agda
new file mode 100644
index 0000000..094bccf
--- /dev/null
+++ b/src/Data/Vec/Any.agda
@@ -0,0 +1,79 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Vectors where at least one element satisfies a given property
+------------------------------------------------------------------------
+
+module Data.Vec.Any {a} {A : Set a} where
+
+open import Data.Empty
+open import Data.Fin
+open import Data.Nat using (zero; suc)
+open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′)
+open import Data.Vec as Vec using (Vec; []; [_]; _∷_)
+open import Data.Product as Prod using (∃; _,_)
+open import Level using (_⊔_)
+open import Relation.Nullary using (¬_; yes; no)
+open import Relation.Nullary.Negation using (contradiction)
+import Relation.Nullary.Decidable as Dec
+open import Relation.Unary
+
+------------------------------------------------------------------------
+-- Any P xs means that at least one element in xs satisfies P.
+
+data Any {p} (P : A → Set p) : ∀ {n} → Vec A n → Set (a ⊔ p) where
+  here  : ∀ {n x} {xs : Vec A n} (px  : P x)      → Any P (x ∷ xs)
+  there : ∀ {n x} {xs : Vec A n} (pxs : Any P xs) → Any P (x ∷ xs)
+
+------------------------------------------------------------------------
+-- Operations on Any
+
+module _ {p} {P : A → Set p} {n x} {xs : Vec A n} where
+
+-- If the tail does not satisfy the predicate, then the head will.
+
+  head : ¬ Any P xs → Any P (x ∷ xs) → P x
+  head ¬pxs (here px)   = px
+  head ¬pxs (there pxs) = contradiction pxs ¬pxs
+
+-- If the head does not satisfy the predicate, then the tail will.
+  tail : ¬ P x → Any P (x ∷ xs) → Any P xs
+  tail ¬px (here  px)  = ⊥-elim (¬px px)
+  tail ¬px (there pxs) = pxs
+
+-- Convert back and forth with sum
+  toSum : Any P (x ∷ xs) → P x ⊎ Any P xs
+  toSum (here px)   = inj₁ px
+  toSum (there pxs) = inj₂ pxs
+
+  fromSum : P x ⊎ Any P xs → Any P (x ∷ xs)
+  fromSum = [ here , there ]′
+
+map : ∀ {p q} {P : A → Set p} {Q : A → Set q} →
+      P ⊆ Q → ∀ {n} → Any P {n} ⊆ Any Q {n}
+map g (here px)   = here (g px)
+map g (there pxs) = there (map g pxs)
+
+index : ∀ {p} {P : A → Set p} {n} {xs : Vec A n} → Any P xs → Fin n
+index (here  px)  = zero
+index (there pxs) = suc (index pxs)
+
+-- If any element satisfies P, then P is satisfied.
+satisfied : ∀ {p} {P : A → Set p} {n} {xs : Vec A n} → Any P xs → ∃ P
+satisfied (here px)   = _ , px
+satisfied (there pxs) = satisfied pxs
+
+------------------------------------------------------------------------
+-- Properties of predicates preserved by Any
+
+module _ {p} {P : A → Set p} where
+
+  any : Decidable P → ∀ {n} → Decidable (Any P {n})
+  any P? []       = no λ()
+  any P? (x ∷ xs) with P? x
+  ... | yes px = yes (here px)
+  ... | no ¬px = Dec.map′ there (tail ¬px) (any P? xs)
+
+  satisfiable : Satisfiable P → ∀ {n} → Satisfiable (Any P {suc n})
+  satisfiable (x , p) {zero}  = x ∷ [] , here p
+  satisfiable (x , p) {suc n} = Prod.map (x ∷_) there (satisfiable (x , p))
diff --git a/src/Data/Vec/Categorical.agda b/src/Data/Vec/Categorical.agda
new file mode 100644
index 0000000..773d019
--- /dev/null
+++ b/src/Data/Vec/Categorical.agda
@@ -0,0 +1,81 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- A categorical view of Vec
+------------------------------------------------------------------------
+
+module Data.Vec.Categorical {a n} where
+
+open import Category.Applicative using (RawApplicative)
+open import Category.Applicative.Indexed using (Morphism)
+open import Category.Functor as Fun using (RawFunctor)
+import Function.Identity.Categorical as Id
+open import Category.Monad using (RawMonad)
+open import Data.Fin using (Fin)
+open import Data.Vec as Vec hiding (_⊛_)
+open import Data.Vec.Properties
+open import Function
+
+------------------------------------------------------------------------
+-- Functor and applicative
+
+functor : RawFunctor (λ (A : Set a) → Vec A n)
+functor = record
+  { _<$>_ = map
+  }
+
+applicative : RawApplicative (λ (A : Set a) → Vec A n)
+applicative = record
+  { pure = replicate
+  ; _⊛_  = Vec._⊛_
+  }
+
+------------------------------------------------------------------------
+-- Get access to other monadic functions
+
+module _ {f F} (App : RawApplicative {f} F) where
+
+  open RawApplicative App
+
+  sequenceA : ∀ {A n} → Vec (F A) n → F (Vec A n)
+  sequenceA []       = pure []
+  sequenceA (x ∷ xs) = _∷_ <$> x ⊛ sequenceA xs
+
+  mapA : ∀ {a} {A : Set a} {B n} → (A → F B) → Vec A n → F (Vec B n)
+  mapA f = sequenceA ∘ map f
+
+  forA : ∀ {a} {A : Set a} {B n} → Vec A n → (A → F B) → F (Vec B n)
+  forA = flip mapA
+
+module _ {m M} (Mon : RawMonad {m} M) where
+
+  private App = RawMonad.rawIApplicative Mon
+
+  sequenceM : ∀ {A n} → Vec (M A) n → M (Vec A n)
+  sequenceM = sequenceA App
+
+  mapM : ∀ {a} {A : Set a} {B n} → (A → M B) → Vec A n → M (Vec B n)
+  mapM = mapA App
+
+  forM : ∀ {a} {A : Set a} {B n} → Vec A n → (A → M B) → M (Vec B n)
+  forM = forA App
+
+------------------------------------------------------------------------
+-- Other
+
+-- lookup is a functor morphism from Vec to Identity.
+
+lookup-functor-morphism : (i : Fin n) → Fun.Morphism functor Id.functor
+lookup-functor-morphism i = record
+  { op     = lookup i
+  ; op-<$> = lookup-map i
+  }
+
+-- lookup is an applicative functor morphism.
+
+lookup-morphism : (i : Fin n) → Morphism applicative Id.applicative
+lookup-morphism i = record
+  { op      = lookup i
+  ; op-pure = lookup-replicate i
+  ; op-⊛    = lookup-⊛ i
+  }
diff --git a/src/Data/Vec/Equality.agda b/src/Data/Vec/Equality.agda
deleted file mode 100644
index 8933a6d..0000000
--- a/src/Data/Vec/Equality.agda
+++ /dev/null
@@ -1,105 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- Semi-heterogeneous vector equality
-------------------------------------------------------------------------
-
-module Data.Vec.Equality where
-
-open import Data.Vec
-open import Data.Nat.Base using (suc)
-open import Function
-open import Level using (_⊔_)
-open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
-open import Relation.Binary.HeterogeneousEquality as H using (_≅_)
-module Equality {s₁ s₂} (S : Setoid s₁ s₂) where
-
-  private
-    open module SS = Setoid S
-      using () renaming (_≈_ to _≊_; Carrier to A)
-
-  infix 4 _≈_
-
-  data _≈_ : ∀ {n¹} → Vec A n¹ →
-             ∀ {n²} → Vec A n² → Set (s₁ ⊔ s₂) where
-    []-cong  : [] ≈ []
-    _∷-cong_ : ∀ {x¹ n¹} {xs¹ : Vec A n¹}
-                 {x² n²} {xs² : Vec A n²}
-                 (x¹≈x² : x¹ ≊ x²) (xs¹≈xs² : xs¹ ≈ xs²) →
-                 x¹ ∷ xs¹ ≈ x² ∷ xs²
-
-  length-equal : ∀ {n¹} {xs¹ : Vec A n¹}
-                   {n²} {xs² : Vec A n²} →
-                 xs¹ ≈ xs² → n¹ ≡ n²
-  length-equal []-cong        = P.refl
-  length-equal (_ ∷-cong eq₂) = P.cong suc $ length-equal eq₂
-
-  refl : ∀ {n} (xs : Vec A n) → xs ≈ xs
-  refl []       = []-cong
-  refl (x ∷ xs) = SS.refl ∷-cong refl xs
-
-  sym : ∀ {n m} {xs : Vec A n} {ys : Vec A m} →
-        xs ≈ ys → ys ≈ xs
-  sym []-cong                = []-cong
-  sym (x¹≡x² ∷-cong xs¹≈xs²) = SS.sym x¹≡x² ∷-cong sym xs¹≈xs²
-
-  trans : ∀ {n m l} {xs : Vec A n} {ys : Vec A m} {zs : Vec A l} →
-          xs ≈ ys → ys ≈ zs → xs ≈ zs
-  trans []-cong            []-cong            = []-cong
-  trans (x≈y ∷-cong xs≈ys) (y≈z ∷-cong ys≈zs) =
-    SS.trans x≈y y≈z ∷-cong trans xs≈ys ys≈zs
-
-  xs++[]≈xs : ∀ {n} (xs : Vec A n) → xs ++ [] ≈ xs
-  xs++[]≈xs []        = []-cong
-  xs++[]≈xs (x ∷ xs) = SS.refl ∷-cong (xs++[]≈xs xs)
-
-  _++-cong_ : ∀ {n₁¹ n₂¹} {xs₁¹ : Vec A n₁¹} {xs₂¹ : Vec A n₂¹}
-                {n₁² n₂²} {xs₁² : Vec A n₁²} {xs₂² : Vec A n₂²} →
-              xs₁¹ ≈ xs₁² → xs₂¹ ≈ xs₂² →
-              xs₁¹ ++ xs₂¹ ≈ xs₁² ++ xs₂²
-  []-cong          ++-cong eq₃ = eq₃
-  (eq₁ ∷-cong eq₂) ++-cong eq₃ = eq₁ ∷-cong (eq₂ ++-cong eq₃)
-
-module DecidableEquality {d₁ d₂} (D : DecSetoid d₁ d₂) where
-
-  private module DS = DecSetoid D
-  open DS using () renaming (_≟_ to _≟′_ ; Carrier to A)
-  open Equality DS.setoid
-  open import Relation.Nullary
-
-  infix 4 _≟_
-
-  _≟_ : ∀ {n m} (xs : Vec A n) (ys : Vec A m) → Dec (xs ≈ ys)
-  _≟_ []       []       = yes []-cong
-  _≟_ []       (y ∷ ys) = no (λ())
-  _≟_ (x ∷ xs) []       = no (λ())
-  _≟_ (x ∷ xs) (y ∷ ys) with xs ≟ ys | x ≟′ y
-  ... | yes xs≈ys | yes x≊y = yes (x≊y ∷-cong xs≈ys)
-  ... | no ¬xs≈ys | _       = no helper
-    where
-    helper : ¬ (x ∷ xs ≈ y ∷ ys)
-    helper (_ ∷-cong xs≈ys) = ¬xs≈ys xs≈ys
-  ... | _         | no ¬x≊y = no helper
-    where
-    helper : ¬ (x ∷ xs ≈ y ∷ ys)
-    helper (x≊y ∷-cong _) = ¬x≊y x≊y
-
-module PropositionalEquality {a} {A : Set a} where
-
-  open Equality (P.setoid A) public
-
-  to-≡ : ∀ {n} {xs ys : Vec A n} → xs ≈ ys → xs ≡ ys
-  to-≡ []-cong                 = P.refl
-  to-≡ (P.refl ∷-cong xs¹≈xs²) = P.cong (_∷_ _) $ to-≡ xs¹≈xs²
-
-  from-≡ : ∀ {n} {xs ys : Vec A n} → xs ≡ ys → xs ≈ ys
-  from-≡ P.refl = refl _
-
-  to-≅ : ∀ {m n} {xs : Vec A m} {ys : Vec A n} →
-            xs ≈ ys → xs ≅ ys
-  to-≅ p with length-equal p
-  to-≅ p | P.refl = H.≡-to-≅ (to-≡ p)
-
-  xs++[]≅xs : ∀ {n} → (xs : Vec A n) → (xs ++ []) ≅ xs
-  xs++[]≅xs xs = to-≅ (xs++[]≈xs xs)
diff --git a/src/Data/Vec/Membership/Propositional.agda b/src/Data/Vec/Membership/Propositional.agda
new file mode 100644
index 0000000..01251f1
--- /dev/null
+++ b/src/Data/Vec/Membership/Propositional.agda
@@ -0,0 +1,24 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Membership of vectors based on propositional equality,
+-- along with some additional definitions.
+------------------------------------------------------------------------
+
+module Data.Vec.Membership.Propositional {a} {A : Set a} where
+
+open import Data.Vec using (Vec)
+open import Data.Vec.Any using (Any)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Nullary using (¬_)
+
+------------------------------------------------------------------------
+-- Types
+
+infix 4 _∈_ _∉_
+
+_∈_ : A → ∀ {n} → Vec A n → Set _
+x ∈ xs = Any (x ≡_) xs
+
+_∉_ : A → ∀ {n} → Vec A n → Set _
+x ∉ xs = ¬ x ∈ xs
diff --git a/src/Data/Vec/Membership/Propositional/Properties.agda b/src/Data/Vec/Membership/Propositional/Properties.agda
new file mode 100644
index 0000000..07e3670
--- /dev/null
+++ b/src/Data/Vec/Membership/Propositional/Properties.agda
@@ -0,0 +1,103 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of membership of vectors based on propositional equality.
+------------------------------------------------------------------------
+
+module Data.Vec.Membership.Propositional.Properties where
+
+open import Data.Fin using (Fin; zero; suc)
+open import Data.Product using (_,_)
+open import Data.Vec hiding (here; there)
+open import Data.Vec.Any using (here; there)
+open import Data.List using ([]; _∷_)
+open import Data.List.Any using (here; there)
+open import Data.Vec.Membership.Propositional
+import Data.List.Membership.Propositional as List
+open import Function using (_∘_; id)
+open import Relation.Binary.PropositionalEquality using (refl)
+
+------------------------------------------------------------------------
+-- lookup
+
+module _ {a} {A : Set a} where
+
+  ∈-lookup : ∀ {n} i (xs : Vec A n) → lookup i xs ∈ xs
+  ∈-lookup zero    (x ∷ xs) = here refl
+  ∈-lookup (suc i) (x ∷ xs) = there (∈-lookup i xs)
+
+------------------------------------------------------------------------
+-- map
+
+module _ {a b} {A : Set a} {B : Set b} (f : A → B) where
+
+  ∈-map⁺ : ∀ {m v} {xs : Vec A m} → v ∈ xs → f v ∈ map f xs
+  ∈-map⁺ (here refl)  = here refl
+  ∈-map⁺ (there x∈xs) = there (∈-map⁺ x∈xs)
+
+------------------------------------------------------------------------
+-- _++_
+
+module _ {a} {A : Set a} {v : A} where
+
+  ∈-++⁺ˡ : ∀ {m n} {xs : Vec A m} {ys : Vec A n} → v ∈ xs → v ∈ xs ++ ys
+  ∈-++⁺ˡ (here refl)  = here refl
+  ∈-++⁺ˡ (there x∈xs) = there (∈-++⁺ˡ x∈xs)
+
+  ∈-++⁺ʳ : ∀ {m n} (xs : Vec A m) {ys : Vec A n} → v ∈ ys → v ∈ xs ++ ys
+  ∈-++⁺ʳ []       x∈ys = x∈ys
+  ∈-++⁺ʳ (x ∷ xs) x∈ys = there (∈-++⁺ʳ xs x∈ys)
+
+------------------------------------------------------------------------
+-- tabulate
+
+module _ {a} {A : Set a} where
+
+  ∈-tabulate⁺ : ∀ {n} (f : Fin n → A) i → f i ∈ tabulate f
+  ∈-tabulate⁺ f zero    = here refl
+  ∈-tabulate⁺ f (suc i) = there (∈-tabulate⁺ (f ∘ suc) i)
+
+------------------------------------------------------------------------
+-- allFin
+
+∈-allFin⁺ : ∀ {n} (i : Fin n) → i ∈ allFin n
+∈-allFin⁺ = ∈-tabulate⁺ id
+
+------------------------------------------------------------------------
+-- allPairs
+
+module _ {a b} {A : Set a} {B : Set b} where
+
+  ∈-allPairs⁺ : ∀ {m n x y} {xs : Vec A m} {ys : Vec B n} →
+               x ∈ xs → y ∈ ys → (x , y) ∈ allPairs xs ys
+  ∈-allPairs⁺ {xs = x ∷ xs} (here refl) = ∈-++⁺ˡ ∘ ∈-map⁺ (x ,_)
+  ∈-allPairs⁺ {xs = x ∷ _} (there x∈xs) =
+    ∈-++⁺ʳ (map (x ,_) _) ∘ ∈-allPairs⁺ x∈xs
+
+------------------------------------------------------------------------
+-- toList
+
+module _ {a} {A : Set a} {v : A} where
+
+  ∈-toList⁺ : ∀ {n} {xs : Vec A n} → v ∈ xs → v List.∈ toList xs
+  ∈-toList⁺ (here refl) = here refl
+  ∈-toList⁺ (there x∈)  = there (∈-toList⁺ x∈)
+
+  ∈-toList⁻ : ∀ {n} {xs : Vec A n} → v List.∈ toList xs → v ∈ xs
+  ∈-toList⁻ {xs = []}     ()
+  ∈-toList⁻ {xs = x ∷ xs} (here refl)  = here refl
+  ∈-toList⁻ {xs = x ∷ xs} (there v∈xs) = there (∈-toList⁻ v∈xs)
+
+------------------------------------------------------------------------
+-- fromList
+
+module _ {a} {A : Set a} {v : A} where
+
+  ∈-fromList⁺ : ∀ {xs} → v List.∈ xs → v ∈ fromList xs
+  ∈-fromList⁺ (here refl) = here refl
+  ∈-fromList⁺ (there x∈)  = there (∈-fromList⁺ x∈)
+
+  ∈-fromList⁻ : ∀ {xs} → v ∈ fromList xs → v List.∈ xs
+  ∈-fromList⁻ {[]}    ()
+  ∈-fromList⁻ {_ ∷ _} (here refl)  = here refl
+  ∈-fromList⁻ {_ ∷ _} (there v∈xs) = there (∈-fromList⁻ v∈xs)
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 8a3d370..27c1ff0 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -6,352 +6,436 @@
 
 module Data.Vec.Properties where
 
-open import Algebra
-open import Category.Applicative.Indexed
-import Category.Functor as Fun
-open import Category.Functor.Identity using (IdentityFunctor)
-open import Category.Monad
-open import Category.Monad.Identity
-open import Data.Vec
-open import Data.List.Any using (here; there)
-import Data.List.Any.Membership.Propositional as List
-open import Data.Nat
-open import Data.Nat.Properties using (+-assoc)
+open import Algebra.FunctionProperties
 open import Data.Empty using (⊥-elim)
 open import Data.Fin as Fin using (Fin; zero; suc; toℕ; fromℕ)
 open import Data.Fin.Properties using (_+′_)
-open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂; <_,_>)
+open import Data.List.Base as List using (List)
+open import Data.List.Any using (here; there)
+import Data.List.Membership.Propositional as List
+open import Data.Nat
+open import Data.Nat.Properties using (+-assoc; ≤-step)
+open import Data.Product as Prod
+  using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry)
+open import Data.Vec
 open import Function
-open import Function.Inverse using (_↔_)
-open import Relation.Binary
+open import Function.Inverse using (_↔_; inverse)
+open import Relation.Binary hiding (Decidable)
+open import Relation.Binary.PropositionalEquality as P
+  using (_≡_; _≢_; refl; _≗_)
+open import Relation.Binary.HeterogeneousEquality as H using (_≅_; refl)
+open import Relation.Unary using (Pred; Decidable)
+open import Relation.Nullary using (yes; no)
 
-module UsingVectorEquality {s₁ s₂} (S : Setoid s₁ s₂) where
+------------------------------------------------------------------------
+-- Properties of propositional equality over vectors
 
-  private module SS = Setoid S
-  open SS using () renaming (Carrier to A)
-  import Data.Vec.Equality as VecEq
-  open VecEq.Equality S
+module _ {a} {A : Set a} {n} {x y : A} {xs ys : Vec A n} where
 
-  replicate-lemma : ∀ {m} n x (xs : Vec A m) →
-                    replicate {n = n}     x ++ (x ∷ xs) ≈
-                    replicate {n = 1 + n} x ++      xs
-  replicate-lemma zero    x xs = refl (x ∷ xs)
-  replicate-lemma (suc n) x xs = SS.refl ∷-cong replicate-lemma n x xs
+ ∷-injectiveˡ : x ∷ xs ≡ y ∷ ys → x ≡ y
+ ∷-injectiveˡ refl = refl
 
-  xs++[]=xs : ∀ {n} (xs : Vec A n) → xs ++ [] ≈ xs
-  xs++[]=xs []       = []-cong
-  xs++[]=xs (x ∷ xs) = SS.refl ∷-cong xs++[]=xs xs
+ ∷-injectiveʳ : x ∷ xs ≡ y ∷ ys → xs ≡ ys
+ ∷-injectiveʳ refl = refl
 
-  map-++-commute : ∀ {b m n} {B : Set b}
-                   (f : B → A) (xs : Vec B m) {ys : Vec B n} →
-                   map f (xs ++ ys) ≈ map f xs ++ map f ys
-  map-++-commute f []       = refl _
-  map-++-commute f (x ∷ xs) = SS.refl ∷-cong map-++-commute f xs
+ ∷-injective : (x ∷ xs) ≡ (y ∷ ys) → x ≡ y × xs ≡ ys
+ ∷-injective refl = refl , refl
 
-open import Relation.Binary.PropositionalEquality as P
-  using (_≡_; _≢_; refl; _≗_)
-open import Relation.Binary.HeterogeneousEquality using (_≅_; refl)
+------------------------------------------------------------------------
+-- _[_]=_
 
-∷-injective : ∀ {a n} {A : Set a} {x y : A} {xs ys : Vec A n} →
-              (x ∷ xs) ≡ (y ∷ ys) → x ≡ y × xs ≡ ys
-∷-injective refl = refl , refl
+module _ {a} {A : Set a} where
 
--- lookup is a functor morphism from Vec to Identity.
+  []=-injective : ∀ {n} {xs : Vec A n} {i x y} →
+                  xs [ i ]= x → xs [ i ]= y → x ≡ y
+  []=-injective here          here          = refl
+  []=-injective (there xsᵢ≡x) (there xsᵢ≡y) = []=-injective xsᵢ≡x xsᵢ≡y
 
-lookup-map : ∀ {a b n} {A : Set a} {B : Set b} (i : Fin n) (f : A → B) (xs : Vec A n) →
-             lookup i (map f xs) ≡ f (lookup i xs)
-lookup-map zero    f (x ∷ xs) = refl
-lookup-map (suc i) f (x ∷ xs) = lookup-map i f xs
+  []=-irrelevance : ∀ {n} {xs : Vec A n} {i x} →
+                    (p q : xs [ i ]= x) → p ≡ q
+  []=-irrelevance here            here             = refl
+  []=-irrelevance (there xs[i]=x) (there xs[i]=x') =
+    P.cong there ([]=-irrelevance xs[i]=x xs[i]=x')
 
-lookup-functor-morphism : ∀ {a n} (i : Fin n) →
-                          Fun.Morphism (functor {a = a} {n = n}) IdentityFunctor
-lookup-functor-morphism i = record { op = lookup i ; op-<$> = lookup-map i }
-
--- lookup is even an applicative functor morphism.
-
-lookup-morphism :
-  ∀ {a n} (i : Fin n) →
-  Morphism (applicative {a = a})
-           (RawMonad.rawIApplicative IdentityMonad)
-lookup-morphism i = record
-  { op      = lookup i
-  ; op-pure = lookup-replicate i
-  ; op-⊛    = lookup-⊛ i
-  }
-  where
-  lookup-replicate : ∀ {a n} {A : Set a} (i : Fin n) (x : A) →
-                     lookup i (replicate x) ≡ x
-  lookup-replicate zero    = λ _ → refl
-  lookup-replicate (suc i) = lookup-replicate i
-
-  lookup-⊛ : ∀ {a b n} {A : Set a} {B : Set b}
-             i (fs : Vec (A → B) n) (xs : Vec A n) →
-             lookup i (fs ⊛ xs) ≡ (lookup i fs $ lookup i xs)
-  lookup-⊛ zero    (f ∷ fs) (x ∷ xs) = refl
-  lookup-⊛ (suc i) (f ∷ fs) (x ∷ xs) = lookup-⊛ i fs xs
+------------------------------------------------------------------------
+-- lookup
 
--- tabulate is an inverse of flip lookup.
+module _ {a} {A : Set a} where
 
-lookup∘tabulate : ∀ {a n} {A : Set a} (f : Fin n → A) (i : Fin n) →
-                  lookup i (tabulate f) ≡ f i
-lookup∘tabulate f zero    = refl
-lookup∘tabulate f (suc i) = lookup∘tabulate (f ∘ suc) i
+  []=⇒lookup : ∀ {n} {x : A} {xs} {i : Fin n} →
+               xs [ i ]= x → lookup i xs ≡ x
+  []=⇒lookup here            = refl
+  []=⇒lookup (there xs[i]=x) = []=⇒lookup xs[i]=x
 
-tabulate∘lookup : ∀ {a n} {A : Set a} (xs : Vec A n) →
-                  tabulate (flip lookup xs) ≡ xs
-tabulate∘lookup []       = refl
-tabulate∘lookup (x ∷ xs) = P.cong (_∷_ x) $ tabulate∘lookup xs
+  lookup⇒[]= : ∀ {n} (i : Fin n) {x : A} xs →
+               lookup i xs ≡ x → xs [ i ]= x
+  lookup⇒[]= zero    (_ ∷ _)  refl = here
+  lookup⇒[]= (suc i) (_  ∷ xs) p    = there (lookup⇒[]= i xs p)
 
--- If you look up an index in allFin n, then you get the index.
+  []=↔lookup : ∀ {n i} {x} {xs : Vec A n} →
+               xs [ i ]= x ↔ lookup i xs ≡ x
+  []=↔lookup = inverse []=⇒lookup (lookup⇒[]= _ _)
+     (λ _ → []=-irrelevance _ _) (λ _ → P.≡-irrelevance _ _)
 
-lookup-allFin : ∀ {n} (i : Fin n) → lookup i (allFin n) ≡ i
-lookup-allFin = lookup∘tabulate id
+------------------------------------------------------------------------
+-- _[_]≔_ (update)
+
+module _ {a} {A : Set a} where
+
+  []≔-idempotent : ∀ {n} (xs : Vec A n) (i : Fin n) {x₁ x₂ : A} →
+                   (xs [ i ]≔ x₁) [ i ]≔ x₂ ≡ xs [ i ]≔ x₂
+  []≔-idempotent []       ()
+  []≔-idempotent (x ∷ xs) zero    = refl
+  []≔-idempotent (x ∷ xs) (suc i) = P.cong (x ∷_) ([]≔-idempotent xs i)
+
+  []≔-commutes : ∀ {n} (xs : Vec A n) (i j : Fin n) {x y : A} → i ≢ j →
+                 (xs [ i ]≔ x) [ j ]≔ y ≡ (xs [ j ]≔ y) [ i ]≔ x
+  []≔-commutes []       ()      ()      _
+  []≔-commutes (x ∷ xs) zero    zero    0≢0 = ⊥-elim $ 0≢0 refl
+  []≔-commutes (x ∷ xs) zero    (suc i) _   = refl
+  []≔-commutes (x ∷ xs) (suc i) zero    _   = refl
+  []≔-commutes (x ∷ xs) (suc i) (suc j) i≢j =
+    P.cong (x ∷_) $ []≔-commutes xs i j (i≢j ∘ P.cong suc)
+
+  []≔-updates : ∀ {n} (xs : Vec A n) (i : Fin n) {x : A} →
+                (xs [ i ]≔ x) [ i ]= x
+  []≔-updates []       ()
+  []≔-updates (x ∷ xs) zero    = here
+  []≔-updates (x ∷ xs) (suc i) = there ([]≔-updates xs i)
+
+  []≔-minimal : ∀ {n} (xs : Vec A n) (i j : Fin n) {x y : A} → i ≢ j →
+                xs [ i ]= x → (xs [ j ]≔ y) [ i ]= x
+  []≔-minimal []       ()      ()      _   _
+  []≔-minimal (x ∷ xs) .zero   zero    0≢0 here        = ⊥-elim (0≢0 refl)
+  []≔-minimal (x ∷ xs) .zero   (suc j) _   here        = here
+  []≔-minimal (x ∷ xs) (suc i) zero    _   (there loc) = there loc
+  []≔-minimal (x ∷ xs) (suc i) (suc j) i≢j (there loc) =
+    there ([]≔-minimal xs i j (i≢j ∘ P.cong suc) loc)
+
+  []≔-lookup : ∀ {n} (xs : Vec A n) (i : Fin n) →
+               xs [ i ]≔ lookup i xs ≡ xs
+  []≔-lookup []       ()
+  []≔-lookup (x ∷ xs) zero    = refl
+  []≔-lookup (x ∷ xs) (suc i) = P.cong (_∷_ x) $ []≔-lookup xs i
+
+  lookup∘update : ∀ {n} (i : Fin n) (xs : Vec A n) x →
+                  lookup i (xs [ i ]≔ x) ≡ x
+  lookup∘update zero    (_ ∷ xs) x = refl
+  lookup∘update (suc i) (_ ∷ xs) x = lookup∘update i xs x
+
+  lookup∘update′ : ∀ {n} {i j : Fin n} → i ≢ j → ∀ (xs : Vec A n) y →
+                   lookup i (xs [ j ]≔ y) ≡ lookup i xs
+  lookup∘update′ {i = zero}  {zero}  i≢j      xs  y = ⊥-elim (i≢j refl)
+  lookup∘update′ {i = zero}  {suc j} i≢j (x ∷ xs) y = refl
+  lookup∘update′ {i = suc i} {zero}  i≢j (x ∷ xs) y = refl
+  lookup∘update′ {i = suc i} {suc j} i≢j (x ∷ xs) y =
+    lookup∘update′ (i≢j ∘ P.cong suc) xs y
 
--- Various lemmas relating lookup and _++_.
-
-lookup-++-< : ∀ {a} {A : Set a} {m n}
-              (xs : Vec A m) (ys : Vec A n) i (i<m : toℕ i < m) →
-              lookup i (xs ++ ys) ≡ lookup (Fin.fromℕ≤ i<m) xs
-lookup-++-< []       ys i       ()
-lookup-++-< (x ∷ xs) ys zero    (s≤s z≤n)       = refl
-lookup-++-< (x ∷ xs) ys (suc i) (s≤s (s≤s i<m)) =
-  lookup-++-< xs ys i (s≤s i<m)
-
-lookup-++-≥ : ∀ {a} {A : Set a} {m n}
-              (xs : Vec A m) (ys : Vec A n) i (i≥m : toℕ i ≥ m) →
-              lookup i (xs ++ ys) ≡ lookup (Fin.reduce≥ i i≥m) ys
-lookup-++-≥ []       ys i       i≥m = refl
-lookup-++-≥ (x ∷ xs) ys zero    ()
-lookup-++-≥ (x ∷ xs) ys (suc i) (s≤s i≥m) = lookup-++-≥ xs ys i i≥m
-
-lookup-++-inject+ : ∀ {a} {A : Set a} {m n}
-                    (xs : Vec A m) (ys : Vec A n) i →
-                    lookup (Fin.inject+ n i) (xs ++ ys) ≡ lookup i xs
-lookup-++-inject+ []       ys ()
-lookup-++-inject+ (x ∷ xs) ys zero    = refl
-lookup-++-inject+ (x ∷ xs) ys (suc i) = lookup-++-inject+ xs ys i
-
-lookup-++-+′ : ∀ {a} {A : Set a} {m n}
-               (xs : Vec A m) (ys : Vec A n) i →
-               lookup (fromℕ m +′ i) (xs ++ ys) ≡ lookup i ys
-lookup-++-+′ []       ys       zero    = refl
-lookup-++-+′ []       (y ∷ xs) (suc i) = lookup-++-+′ [] xs i
-lookup-++-+′ (x ∷ xs) ys       i       = lookup-++-+′ xs ys i
-
--- Properties relating lookup and _[_]≔_.
-
-lookup∘update : ∀ {a} {A : Set a} {n}
-                (i : Fin n) (xs : Vec A n) x →
-                lookup i (xs [ i ]≔ x) ≡ x
-lookup∘update zero    (_ ∷ xs) x = refl
-lookup∘update (suc i) (_ ∷ xs) x = lookup∘update i xs x
-
-lookup∘update′ : ∀ {a} {A : Set a} {n} {i j : Fin n} →
-                 i ≢ j → ∀ (xs : Vec A n) y →
-                 lookup i (xs [ j ]≔ y) ≡ lookup i xs
-lookup∘update′ {i = zero}  {zero}  i≢j      xs  y = ⊥-elim (i≢j refl)
-lookup∘update′ {i = zero}  {suc j} i≢j (x ∷ xs) y = refl
-lookup∘update′ {i = suc i} {zero}  i≢j (x ∷ xs) y = refl
-lookup∘update′ {i = suc i} {suc j} i≢j (x ∷ xs) y =
-  lookup∘update′ (i≢j ∘ P.cong suc) xs y
-
--- map is a congruence.
+------------------------------------------------------------------------
+-- map
+
+map-id : ∀ {a n} {A : Set a} → map {n = n} {A} id ≗ id
+map-id []       = refl
+map-id (x ∷ xs) = P.cong (x ∷_) (map-id xs)
 
 map-cong : ∀ {a b n} {A : Set a} {B : Set b} {f g : A → B} →
-           f ≗ g → _≗_ {A = Vec A n} (map f) (map g)
+           f ≗ g → map {n = n} f ≗ map g
 map-cong f≗g []       = refl
 map-cong f≗g (x ∷ xs) = P.cong₂ _∷_ (f≗g x) (map-cong f≗g xs)
 
--- map is functorial.
-
-map-id : ∀ {a n} {A : Set a} → _≗_ {A = Vec A n} (map id) id
-map-id []       = refl
-map-id (x ∷ xs) = P.cong (_∷_ x) (map-id xs)
-
 map-∘ : ∀ {a b c n} {A : Set a} {B : Set b} {C : Set c}
         (f : B → C) (g : A → B) →
-        _≗_ {A = Vec A n} (map (f ∘ g)) (map f ∘ map g)
+        map {n = n} (f ∘ g) ≗ map f ∘ map g
 map-∘ f g []       = refl
-map-∘ f g (x ∷ xs) = P.cong (_∷_ (f (g x))) (map-∘ f g xs)
-
--- Laws of the applicative.
-
--- Idiomatic application is a special case of zipWith:
--- _⊛_ = zipWith id
-
-⊛-is-zipWith : ∀ {a b n} {A : Set a} {B : Set b} →
-               (fs : Vec (A → B) n) (xs : Vec A n) →
-               (fs ⊛ xs) ≡ zipWith _$_ fs xs
-⊛-is-zipWith []       []       = refl
-⊛-is-zipWith (f ∷ fs) (x ∷ xs) = P.cong (f x ∷_) (⊛-is-zipWith fs xs)
-
--- map is expressible via idiomatic application
-
-map-is-⊛ : ∀ {a b n} {A : Set a} {B : Set b} (f : A → B) (xs : Vec A n) →
-           map f xs ≡ (replicate f ⊛ xs)
-map-is-⊛ f []       = refl
-map-is-⊛ f (x ∷ xs) = P.cong (_ ∷_) (map-is-⊛ f xs)
-
--- zipWith is expressible via idiomatic application
-
-zipWith-is-⊛ : ∀ {a b c n} {A : Set a} {B : Set b} {C : Set c} →
-               (f : A → B → C) (xs : Vec A n) (ys : Vec B n) →
-               zipWith f xs ys ≡ (replicate f ⊛ xs ⊛ ys)
-zipWith-is-⊛ f []       []       = refl
-zipWith-is-⊛ f (x ∷ xs) (y ∷ ys) = P.cong (_ ∷_) (zipWith-is-⊛ f xs ys)
-
--- Applicative fusion laws for map and zipWith.
+map-∘ f g (x ∷ xs) = P.cong (f (g x) ∷_) (map-∘ f g xs)
 
--- pulling a replicate into a map
-
-map-replicate :  ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (x : A) (n : ℕ) →
-                 map f (replicate {n = n} x) ≡ replicate {n = n} (f x)
-map-replicate f x zero = refl
-map-replicate f x (suc n) = P.cong (f x ∷_) (map-replicate f x n)
+lookup-map : ∀ {a b n} {A : Set a} {B : Set b}
+             (i : Fin n) (f : A → B) (xs : Vec A n) →
+             lookup i (map f xs) ≡ f (lookup i xs)
+lookup-map zero    f (x ∷ xs) = refl
+lookup-map (suc i) f (x ∷ xs) = lookup-map i f xs
 
--- pulling a replicate into a zipWith
+map-[]≔ : ∀ {n a b} {A : Set a} {B : Set b}
+          (f : A → B) (xs : Vec A n) (i : Fin n) {x : A} →
+          map f (xs [ i ]≔ x) ≡ map f xs [ i ]≔ f x
+map-[]≔ f []       ()
+map-[]≔ f (x ∷ xs) zero    = refl
+map-[]≔ f (x ∷ xs) (suc i) = P.cong (_ ∷_) $ map-[]≔ f xs i
 
-zipWith-replicate₁ : ∀ {a b c n} {A : Set a} {B : Set b} {C : Set c} →
-                    (_⊕_ : A → B → C) (x : A) (ys : Vec B n) →
-                    zipWith _⊕_ (replicate x) ys ≡ map (x ⊕_) ys
-zipWith-replicate₁ _⊕_ x []       = refl
-zipWith-replicate₁ _⊕_ x (y ∷ ys) = P.cong ((x ⊕ y) ∷_) (zipWith-replicate₁ _⊕_ x ys)
+------------------------------------------------------------------------
+-- _++_
+
+module _ {a} {A : Set a} {m} {ys ys' : Vec A m} where
+
+  ++-injectiveˡ : ∀ {n} (xs xs' : Vec A n) →
+                  xs ++ ys ≡ xs' ++ ys' → xs ≡ xs'
+  ++-injectiveˡ []       []         _  = refl
+  ++-injectiveˡ (x ∷ xs) (x' ∷ xs') eq =
+    P.cong₂ _∷_ (∷-injectiveˡ eq) (++-injectiveˡ _ _ (∷-injectiveʳ eq))
+
+  ++-injectiveʳ : ∀ {n} (xs xs' : Vec A n) →
+                  xs ++ ys ≡ xs' ++ ys' → ys ≡ ys'
+  ++-injectiveʳ []       []         eq = eq
+  ++-injectiveʳ (x ∷ xs) (x' ∷ xs') eq =
+    ++-injectiveʳ xs xs' (∷-injectiveʳ eq)
+
+  ++-injective  : ∀ {n} (xs xs' : Vec A n) →
+                  xs ++ ys ≡ xs' ++ ys' → xs ≡ xs' × ys ≡ ys'
+  ++-injective xs xs' eq =
+    (++-injectiveˡ xs xs' eq , ++-injectiveʳ xs xs' eq)
+
+module _ {a} {A : Set a} where
+
+  ++-assoc : ∀ {m n k} (xs : Vec A m) (ys : Vec A n) (zs : Vec A k) →
+             (xs ++ ys) ++ zs ≅ xs ++ (ys ++ zs)
+  ++-assoc         []       ys zs = refl
+  ++-assoc {suc m} (x ∷ xs) ys zs =
+    H.icong (Vec A) (+-assoc m _ _) (x ∷_) (++-assoc xs ys zs)
+
+  lookup-++-< : ∀ {m n} (xs : Vec A m) (ys : Vec A n) →
+                ∀ i (i<m : toℕ i < m) →
+                lookup i (xs ++ ys) ≡ lookup (Fin.fromℕ≤ i<m) xs
+  lookup-++-< []       ys i       ()
+  lookup-++-< (x ∷ xs) ys zero    (s≤s z≤n)       = refl
+  lookup-++-< (x ∷ xs) ys (suc i) (s≤s (s≤s i<m)) =
+    lookup-++-< xs ys i (s≤s i<m)
+
+  lookup-++-≥ : ∀ {m n} (xs : Vec A m) (ys : Vec A n) →
+                ∀ i (i≥m : toℕ i ≥ m) →
+                lookup i (xs ++ ys) ≡ lookup (Fin.reduce≥ i i≥m) ys
+  lookup-++-≥ []       ys i       i≥m       = refl
+  lookup-++-≥ (x ∷ xs) ys zero    ()
+  lookup-++-≥ (x ∷ xs) ys (suc i) (s≤s i≥m) = lookup-++-≥ xs ys i i≥m
+
+  lookup-++-inject+ : ∀ {m n} (xs : Vec A m) (ys : Vec A n) i →
+                      lookup (Fin.inject+ n i) (xs ++ ys) ≡ lookup i xs
+  lookup-++-inject+ []       ys ()
+  lookup-++-inject+ (x ∷ xs) ys zero    = refl
+  lookup-++-inject+ (x ∷ xs) ys (suc i) = lookup-++-inject+ xs ys i
+
+  lookup-++-+′ : ∀ {m n} (xs : Vec A m) (ys : Vec A n) i →
+                 lookup (fromℕ m +′ i) (xs ++ ys) ≡ lookup i ys
+  lookup-++-+′ []       ys       zero    = refl
+  lookup-++-+′ []       (y ∷ xs) (suc i) = lookup-++-+′ [] xs i
+  lookup-++-+′ (x ∷ xs) ys       i       = lookup-++-+′ xs ys i
+
+  []≔-++-inject+ : ∀ {m n x} (xs : Vec A m) (ys : Vec A n) i →
+                   (xs ++ ys) [ Fin.inject+ n i ]≔ x ≡ (xs [ i ]≔ x) ++ ys
+  []≔-++-inject+ []       ys ()
+  []≔-++-inject+ (x ∷ xs) ys zero    = refl
+  []≔-++-inject+ (x ∷ xs) ys (suc i) =
+    P.cong (x ∷_) $ []≔-++-inject+ xs ys i
 
-zipWith-replicate₂ : ∀ {a b c n} {A : Set a} {B : Set b} {C : Set c} →
-                    (_⊕_ : A → B → C) (xs : Vec A n) (y : B) →
-                    zipWith _⊕_ xs (replicate y) ≡ map (_⊕ y) xs
-zipWith-replicate₂ _⊕_ []       y = refl
-zipWith-replicate₂ _⊕_ (x ∷ xs) y = P.cong ((x ⊕ y) ∷_) (zipWith-replicate₂ _⊕_ xs y)
+------------------------------------------------------------------------
+-- zipWith
+
+module _ {a} {A : Set a} {f : A → A → A} where
+
+  zipWith-assoc : Associative _≡_ f → ∀ {n} →
+                  Associative _≡_ (zipWith {n = n} f)
+  zipWith-assoc assoc []       []       []       = refl
+  zipWith-assoc assoc (x ∷ xs) (y ∷ ys) (z ∷ zs) =
+    P.cong₂ _∷_ (assoc x y z) (zipWith-assoc assoc xs ys zs)
+
+  zipWith-idem : Idempotent _≡_ f → ∀ {n} →
+                 Idempotent _≡_ (zipWith {n = n} f)
+  zipWith-idem idem []       = refl
+  zipWith-idem idem (x ∷ xs) =
+    P.cong₂ _∷_ (idem x) (zipWith-idem idem xs)
+
+  zipWith-identityˡ : ∀ {1#} → LeftIdentity _≡_ 1# f → ∀ {n} →
+                      LeftIdentity _≡_ (replicate 1#) (zipWith {n = n} f)
+  zipWith-identityˡ idˡ []       = refl
+  zipWith-identityˡ idˡ (x ∷ xs) =
+    P.cong₂ _∷_ (idˡ x) (zipWith-identityˡ idˡ xs)
+
+  zipWith-identityʳ : ∀ {1#} → RightIdentity _≡_ 1# f → ∀ {n} →
+                      RightIdentity _≡_ (replicate 1#) (zipWith {n = n} f)
+  zipWith-identityʳ idʳ []       = refl
+  zipWith-identityʳ idʳ (x ∷ xs) =
+    P.cong₂ _∷_ (idʳ x) (zipWith-identityʳ idʳ xs)
+
+  zipWith-zeroˡ : ∀ {0#} → LeftZero _≡_ 0# f → ∀ {n} →
+                  LeftZero _≡_ (replicate 0#) (zipWith {n = n} f)
+  zipWith-zeroˡ zeˡ []       = refl
+  zipWith-zeroˡ zeˡ (x ∷ xs) =
+    P.cong₂ _∷_ (zeˡ x) (zipWith-zeroˡ zeˡ xs)
+
+  zipWith-zeroʳ : ∀ {0#} → RightZero _≡_ 0# f → ∀ {n} →
+                  RightZero _≡_ (replicate 0#) (zipWith {n = n} f)
+  zipWith-zeroʳ zeʳ []       = refl
+  zipWith-zeroʳ zeʳ (x ∷ xs) =
+    P.cong₂ _∷_ (zeʳ x) (zipWith-zeroʳ zeʳ xs)
+
+  zipWith-inverseˡ : ∀ {⁻¹ 0#} → LeftInverse _≡_ 0# ⁻¹ f → ∀ {n} →
+                     LeftInverse _≡_ (replicate {n = n} 0#) (map ⁻¹) (zipWith f)
+  zipWith-inverseˡ invˡ []       = refl
+  zipWith-inverseˡ invˡ (x ∷ xs) =
+    P.cong₂ _∷_ (invˡ x) (zipWith-inverseˡ invˡ xs)
+
+  zipWith-inverseʳ : ∀ {⁻¹ 0#} → RightInverse _≡_ 0# ⁻¹ f → ∀ {n} →
+                     RightInverse _≡_ (replicate {n = n} 0#) (map ⁻¹) (zipWith f)
+  zipWith-inverseʳ invʳ []       = refl
+  zipWith-inverseʳ invʳ (x ∷ xs) =
+    P.cong₂ _∷_ (invʳ x) (zipWith-inverseʳ invʳ xs)
+
+  zipWith-distribˡ : ∀ {g} → _DistributesOverˡ_ _≡_ f g → ∀ {n} →
+                     _DistributesOverˡ_ _≡_ (zipWith {n = n} f) (zipWith g)
+  zipWith-distribˡ distribˡ []        []      []       = refl
+  zipWith-distribˡ distribˡ (x ∷ xs) (y ∷ ys) (z ∷ zs) =
+    P.cong₂ _∷_ (distribˡ x y z) (zipWith-distribˡ distribˡ xs ys zs)
+
+  zipWith-distribʳ : ∀ {g} → _DistributesOverʳ_ _≡_ f g → ∀ {n} →
+                     _DistributesOverʳ_ _≡_ (zipWith {n = n} f) (zipWith g)
+  zipWith-distribʳ distribʳ []        []      []       = refl
+  zipWith-distribʳ distribʳ (x ∷ xs) (y ∷ ys) (z ∷ zs) =
+    P.cong₂ _∷_ (distribʳ x y z) (zipWith-distribʳ distribʳ xs ys zs)
+
+  zipWith-absorbs : ∀ {g} → _Absorbs_ _≡_ f g → ∀ {n} →
+                   _Absorbs_ _≡_ (zipWith {n = n} f) (zipWith g)
+  zipWith-absorbs abs []       []       = refl
+  zipWith-absorbs abs (x ∷ xs) (y ∷ ys) =
+    P.cong₂ _∷_ (abs x y) (zipWith-absorbs abs xs ys)
+
+module _ {a b} {A : Set a} {B : Set b} {f : A → A → B} where
+
+  zipWith-comm : (∀ x y → f x y ≡ f y x) → ∀ {n}
+                 (xs ys : Vec A n) → zipWith f xs ys ≡ zipWith f ys xs
+  zipWith-comm comm []       []       = refl
+  zipWith-comm comm (x ∷ xs) (y ∷ ys) =
+    P.cong₂ _∷_ (comm x y) (zipWith-comm comm xs ys)
+
+module _ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} where
+
+  zipWith-map₁ : ∀ {n} (_⊕_ : B → C → D) (f : A → B)
+                 (xs : Vec A n) (ys : Vec C n) →
+                 zipWith _⊕_ (map f xs) ys ≡ zipWith (λ x y → f x ⊕ y) xs ys
+  zipWith-map₁ _⊕_ f []       []       = refl
+  zipWith-map₁ _⊕_ f (x ∷ xs) (y ∷ ys) =
+    P.cong (f x ⊕ y ∷_) (zipWith-map₁ _⊕_ f xs ys)
+
+  zipWith-map₂ : ∀ {n} (_⊕_ : A → C → D) (f : B → C)
+                 (xs : Vec A n) (ys : Vec B n) →
+                 zipWith _⊕_ xs (map f ys) ≡ zipWith (λ x y → x ⊕ f y) xs ys
+  zipWith-map₂ _⊕_ f []       []       = refl
+  zipWith-map₂ _⊕_ f (x ∷ xs) (y ∷ ys) =
+    P.cong (x ⊕ f y ∷_) (zipWith-map₂ _⊕_ f xs ys)
+
+module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where
+
+  lookup-zipWith : ∀ (f : A → B → C) {n} (i : Fin n) xs ys →
+                   lookup i (zipWith f xs ys) ≡ f (lookup i xs) (lookup i ys)
+  lookup-zipWith _ zero    (x ∷ _)  (y ∷ _)   = refl
+  lookup-zipWith _ (suc i) (_ ∷ xs) (_ ∷ ys)  = lookup-zipWith _ i xs ys
 
--- pulling a map into a zipWith
+------------------------------------------------------------------------
+-- zip
 
-zipWith-map₁ : ∀ {a b c d n} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
-               (_⊕_ : B → C → D) (f : A → B) (xs : Vec A n) (ys : Vec C n) →
-               zipWith _⊕_ (map f xs) ys ≡ zipWith (λ x y → f x ⊕ y) xs ys
-zipWith-map₁ _⊕_ f [] [] = refl
-zipWith-map₁ _⊕_ f (x ∷ xs) (y ∷ ys) = P.cong ((f x ⊕ y) ∷_) (zipWith-map₁ _⊕_ f xs ys)
+module _ {a b} {A : Set a} {B : Set b} where
 
-zipWith-map₂ : ∀ {a b c d n} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
-               (_⊕_ : A → C → D) (f : B → C) (xs : Vec A n) (ys : Vec B n) →
-               zipWith _⊕_ xs (map f ys) ≡ zipWith (λ x y → x ⊕ f y) xs ys
-zipWith-map₂ _⊕_ f [] [] = refl
-zipWith-map₂ _⊕_ f (x ∷ xs) (y ∷ ys) = P.cong ((x ⊕ f y) ∷_) (zipWith-map₂ _⊕_ f xs ys)
+  lookup-zip : ∀ {n} (i : Fin n) (xs : Vec A n) (ys : Vec B n) →
+               lookup i (zip xs ys) ≡ (lookup i xs , lookup i ys)
+  lookup-zip = lookup-zipWith _,_
 
--- Tabulation.
+  -- map lifts projections to vectors of products.
 
--- mapping over a tabulation is the tabulation of the composition
+  map-proj₁-zip : ∀ {n} (xs : Vec A n) (ys : Vec B n) →
+                  map proj₁ (zip xs ys) ≡ xs
+  map-proj₁-zip []       []       = refl
+  map-proj₁-zip (x ∷ xs) (y ∷ ys) = P.cong (x ∷_) (map-proj₁-zip xs ys)
 
-tabulate-∘ : ∀ {n a b} {A : Set a} {B : Set b}
-             (f : A → B) (g : Fin n → A) →
-             tabulate (f ∘ g) ≡ map f (tabulate g)
-tabulate-∘ {zero}  f g = refl
-tabulate-∘ {suc n} f g = P.cong (f (g zero) ∷_) (tabulate-∘ f (g ∘ suc))
+  map-proj₂-zip : ∀ {n} (xs : Vec A n) (ys : Vec B n) →
+                  map proj₂ (zip xs ys) ≡ ys
+  map-proj₂-zip []       []       = refl
+  map-proj₂-zip (x ∷ xs) (y ∷ ys) = P.cong (y ∷_) (map-proj₂-zip xs ys)
 
--- tabulate can be expressed using map and allFin.
+-- map lifts pairing to vectors of products.
 
-tabulate-allFin : ∀ {n a} {A : Set a} (f : Fin n → A) →
-                  tabulate f ≡ map f (allFin n)
-tabulate-allFin f = tabulate-∘ f id
+map-<,>-zip : ∀ {a b c n} {A : Set a} {B : Set b} {C : Set c}
+              (f : A → B) (g : A → C) (xs : Vec A n) →
+              map < f , g > xs ≡ zip (map f xs) (map g xs)
+map-<,>-zip f g []       = P.refl
+map-<,>-zip f g (x ∷ xs) = P.cong (_ ∷_) (map-<,>-zip f g xs)
 
--- The positive case of allFin can be expressed recursively using map.
+map-zip : ∀ {a b c d n} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
+          (f : A → B) (g : C → D) (xs : Vec A n) (ys : Vec C n) →
+          map (Prod.map f g) (zip xs ys) ≡ zip (map f xs) (map g ys)
+map-zip f g []       []       = refl
+map-zip f g (x ∷ xs) (y ∷ ys) = P.cong (_ ∷_) (map-zip f g xs ys)
 
-allFin-map : ∀ n → allFin (suc n) ≡ zero ∷ map suc (allFin n)
-allFin-map n = P.cong (_∷_ zero) $ tabulate-∘ suc id
+------------------------------------------------------------------------
+-- unzip
 
--- If you look up every possible index, in increasing order, then you
--- get back the vector you started with.
+module _ {a b} {A : Set a} {B : Set b} where
 
-map-lookup-allFin : ∀ {a} {A : Set a} {n} (xs : Vec A n) →
-                    map (λ x → lookup x xs) (allFin n) ≡ xs
-map-lookup-allFin {n = n} xs = begin
-  map (λ x → lookup x xs) (allFin n) ≡⟨ P.sym $ tabulate-∘ (λ x → lookup x xs) id ⟩
-  tabulate (λ x → lookup x xs)       ≡⟨ tabulate∘lookup xs ⟩
-  xs                                 ∎
-  where open P.≡-Reasoning
+  lookup-unzip : ∀ {n} (i : Fin n) (xys : Vec (A × B) n) →
+                 let xs , ys = unzip xys
+                 in (lookup i xs , lookup i ys) ≡ lookup i xys
+  lookup-unzip ()      []
+  lookup-unzip zero    ((x , y) ∷ xys) = refl
+  lookup-unzip (suc i) ((x , y) ∷ xys) = lookup-unzip i xys
 
--- tabulate f contains f i.
+  map-unzip : ∀ {c d n} {C : Set c} {D : Set d}
+              (f : A → B) (g : C → D) (xys : Vec (A × C) n) →
+              let xs , ys = unzip xys
+              in (map f xs , map g ys) ≡ unzip (map (Prod.map f g) xys)
+  map-unzip f g []              = refl
+  map-unzip f g ((x , y) ∷ xys) =
+    P.cong (Prod.map (f x ∷_) (g y ∷_)) (map-unzip f g xys)
 
-∈-tabulate : ∀ {n a} {A : Set a} (f : Fin n → A) i → f i ∈ tabulate f
-∈-tabulate f zero    = here
-∈-tabulate f (suc i) = there (∈-tabulate (f ∘ suc) i)
+  -- Products of vectors are isomorphic to vectors of products.
 
--- allFin n contains all elements in Fin n.
+  unzip∘zip : ∀ {n} (xs : Vec A n) (ys : Vec B n) →
+              unzip (zip xs ys) ≡ (xs , ys)
+  unzip∘zip [] []             = refl
+  unzip∘zip (x ∷ xs) (y ∷ ys) =
+    P.cong (Prod.map (x ∷_) (y ∷_)) (unzip∘zip xs ys)
 
-∈-allFin : ∀ {n} (i : Fin n) → i ∈ allFin n
-∈-allFin = ∈-tabulate id
+  zip∘unzip : ∀ {n} (xys : Vec (A × B) n) →
+              uncurry zip (unzip xys) ≡ xys
+  zip∘unzip []              = refl
+  zip∘unzip ((x , y) ∷ xys) = P.cong ((x , y) ∷_) (zip∘unzip xys)
 
-∈-map : ∀ {a b m} {A : Set a} {B : Set b} {x : A} {xs : Vec A m}
-        (f : A → B) → x ∈ xs → f x ∈ map f xs
-∈-map f here         = here
-∈-map f (there x∈xs) = there (∈-map f x∈xs)
+  ×v↔v× : ∀ {n} → (Vec A n × Vec B n) ↔ Vec (A × B) n
+  ×v↔v× = inverse (uncurry zip) unzip (uncurry unzip∘zip) zip∘unzip
 
--- _∈_ is preserved by _++_
-∈-++ₗ : ∀ {a m n} {A : Set a} {x : A} {xs : Vec A m} {ys : Vec A n}
-        → x ∈ xs → x ∈ xs ++ ys
-∈-++ₗ here         = here
-∈-++ₗ (there x∈xs) = there (∈-++ₗ x∈xs)
+------------------------------------------------------------------------
+-- _⊛_
 
-∈-++ᵣ : ∀ {a m n} {A : Set a} {x : A} (xs : Vec A m) {ys : Vec A n}
-        → x ∈ ys → x ∈ xs ++ ys
-∈-++ᵣ []       x∈ys = x∈ys
-∈-++ᵣ (x ∷ xs) x∈ys = there (∈-++ᵣ xs x∈ys)
+module _ {a b} {A : Set a} {B : Set b} where
 
--- allPairs contains every pair of elements
+  lookup-⊛ : ∀ {n} i (fs : Vec (A → B) n) (xs : Vec A n) →
+             lookup i (fs ⊛ xs) ≡ (lookup i fs $ lookup i xs)
+  lookup-⊛ zero    (f ∷ fs) (x ∷ xs) = refl
+  lookup-⊛ (suc i) (f ∷ fs) (x ∷ xs) = lookup-⊛ i fs xs
 
-∈-allPairs : ∀ {a b} {A : Set a} {B : Set b} {m n : ℕ}
-             {xs : Vec A m} {ys : Vec B n}
-             {x y} → x ∈ xs → y ∈ ys → (x , y) ∈ allPairs xs ys
-∈-allPairs {xs = x ∷ xs} {ys} here         y∈ys =
-  ∈-++ₗ (∈-map (x ,_) y∈ys)
-∈-allPairs {xs = x ∷ xs} {ys} (there x∈xs) y∈ys =
-  ∈-++ᵣ (map (x ,_) ys) (∈-allPairs x∈xs y∈ys)
+  map-is-⊛ : ∀ {n} (f : A → B) (xs : Vec A n) →
+             map f xs ≡ (replicate f ⊛ xs)
+  map-is-⊛ f []       = refl
+  map-is-⊛ f (x ∷ xs) = P.cong (_ ∷_) (map-is-⊛ f xs)
 
--- sum commutes with _++_.
+  ⊛-is-zipWith : ∀ {n} (fs : Vec (A → B) n) (xs : Vec A n) →
+                 (fs ⊛ xs) ≡ zipWith _$_ fs xs
+  ⊛-is-zipWith []       []       = refl
+  ⊛-is-zipWith (f ∷ fs) (x ∷ xs) = P.cong (f x ∷_) (⊛-is-zipWith fs xs)
 
-sum-++-commute : ∀ {m n} (xs : Vec ℕ m) {ys : Vec ℕ n} →
-                 sum (xs ++ ys) ≡ sum xs + sum ys
-sum-++-commute []            = refl
-sum-++-commute (x ∷ xs) {ys} = begin
-  x + sum (xs ++ ys)
-    ≡⟨ P.cong (λ p → x + p) (sum-++-commute xs) ⟩
-  x + (sum xs + sum ys)
-    ≡⟨ P.sym (+-assoc x (sum xs) (sum ys)) ⟩
-  sum (x ∷ xs) + sum ys
-    ∎
-  where
-  open P.≡-Reasoning
+  zipWith-is-⊛ : ∀ {c} {C : Set c} {n} (f : A → B → C) →
+                 (xs : Vec A n) (ys : Vec B n) →
+                 zipWith f xs ys ≡ (replicate f ⊛ xs ⊛ ys)
+  zipWith-is-⊛ f []       []       = refl
+  zipWith-is-⊛ f (x ∷ xs) (y ∷ ys) = P.cong (_ ∷_) (zipWith-is-⊛ f xs ys)
 
--- foldr is a congruence.
+------------------------------------------------------------------------
+-- foldr
 
 foldr-cong : ∀ {a b} {A : Set a}
-               {B₁ : ℕ → Set b}
-               {f₁ : ∀ {n} → A → B₁ n → B₁ (suc n)} {e₁}
-               {B₂ : ℕ → Set b}
-               {f₂ : ∀ {n} → A → B₂ n → B₂ (suc n)} {e₂} →
-             (∀ {n x} {y₁ : B₁ n} {y₂ : B₂ n} →
-                y₁ ≅ y₂ → f₁ x y₁ ≅ f₂ x y₂) →
-             e₁ ≅ e₂ →
-             ∀ {n} (xs : Vec A n) →
-             foldr B₁ f₁ e₁ xs ≅ foldr B₂ f₂ e₂ xs
-foldr-cong           _     e₁=e₂ []       = e₁=e₂
-foldr-cong {B₁ = B₁} f₁=f₂ e₁=e₂ (x ∷ xs) =
-  f₁=f₂ (foldr-cong {B₁ = B₁} f₁=f₂ e₁=e₂ xs)
-
--- foldl is a congruence.
-
-foldl-cong : ∀ {a b} {A : Set a}
-               {B₁ : ℕ → Set b}
-               {f₁ : ∀ {n} → B₁ n → A → B₁ (suc n)} {e₁}
-               {B₂ : ℕ → Set b}
-               {f₂ : ∀ {n} → B₂ n → A → B₂ (suc n)} {e₂} →
-             (∀ {n x} {y₁ : B₁ n} {y₂ : B₂ n} →
-                y₁ ≅ y₂ → f₁ y₁ x ≅ f₂ y₂ x) →
-             e₁ ≅ e₂ →
-             ∀ {n} (xs : Vec A n) →
-             foldl B₁ f₁ e₁ xs ≅ foldl B₂ f₂ e₂ xs
-foldl-cong           _     e₁=e₂ []       = e₁=e₂
-foldl-cong {B₁ = B₁} f₁=f₂ e₁=e₂ (x ∷ xs) =
-  foldl-cong {B₁ = B₁ ∘ suc} f₁=f₂ (f₁=f₂ e₁=e₂) xs
+             {B : ℕ → Set b} {f : ∀ {n} → A → B n → B (suc n)} {d}
+             {C : ℕ → Set b} {g : ∀ {n} → A → C n → C (suc n)} {e} →
+             (∀ {n x} {y : B n} {z : C n} → y ≅ z → f x y ≅ g x z) →
+             d ≅ e → ∀ {n} (xs : Vec A n) →
+             foldr B f d xs ≅ foldr C g e xs
+foldr-cong _   d≅e []       = d≅e
+foldr-cong f≅g d≅e (x ∷ xs) = f≅g (foldr-cong f≅g d≅e xs)
 
 -- The (uniqueness part of the) universality property for foldr.
 
@@ -359,9 +443,9 @@ foldr-universal : ∀ {a b} {A : Set a} (B : ℕ → Set b)
                   (f : ∀ {n} → A → B n → B (suc n)) {e}
                   (h : ∀ {n} → Vec A n → B n) →
                   h [] ≡ e →
-                  (∀ {n} x → h ∘ _∷_ x ≗ f {n} x ∘ h) →
+                  (∀ {n} x → h ∘ (x ∷_) ≗ f {n} x ∘ h) →
                   ∀ {n} → h ≗ foldr B {n} f e
-foldr-universal B f     h base step []       = base
+foldr-universal B f {_} h base step []       = base
 foldr-universal B f {e} h base step (x ∷ xs) = begin
   h (x ∷ xs)
     ≡⟨ step x xs ⟩
@@ -371,199 +455,194 @@ foldr-universal B f {e} h base step (x ∷ xs) = begin
     ∎
   where open P.≡-Reasoning
 
--- A fusion law for foldr.
-
 foldr-fusion : ∀ {a b c} {A : Set a}
-                 {B : ℕ → Set b} {f : ∀ {n} → A → B n → B (suc n)} e
-                 {C : ℕ → Set c} {g : ∀ {n} → A → C n → C (suc n)}
+               {B : ℕ → Set b} {f : ∀ {n} → A → B n → B (suc n)} e
+               {C : ℕ → Set c} {g : ∀ {n} → A → C n → C (suc n)}
                (h : ∀ {n} → B n → C n) →
                (∀ {n} x → h ∘ f {n} x ≗ g x ∘ h) →
                ∀ {n} → h ∘ foldr B {n} f e ≗ foldr C g (h e)
 foldr-fusion {B = B} {f} e {C} h fuse =
   foldr-universal C _ _ refl (λ x xs → fuse x (foldr B f e xs))
 
--- The identity function is a fold.
-
 idIsFold : ∀ {a n} {A : Set a} → id ≗ foldr (Vec A) {n} _∷_ []
 idIsFold = foldr-universal _ _ id refl (λ _ _ → refl)
 
--- The _∈_ predicate is equivalent (in the following sense) to the
--- corresponding predicate for lists.
-
-∈⇒List-∈ : ∀ {a} {A : Set a} {n x} {xs : Vec A n} →
-           x ∈ xs → x List.∈ toList xs
-∈⇒List-∈ here       = here P.refl
-∈⇒List-∈ (there x∈) = there (∈⇒List-∈ x∈)
-
-List-∈⇒∈ : ∀ {a} {A : Set a} {x : A} {xs} →
-           x List.∈ xs → x ∈ fromList xs
-List-∈⇒∈ (here P.refl) = here
-List-∈⇒∈ (there x∈)    = there (List-∈⇒∈ x∈)
-
--- Proof irrelevance for _[_]=_.
-
-proof-irrelevance-[]= : ∀ {a} {A : Set a} {n} {xs : Vec A n} {i x} →
-                        (p q : xs [ i ]= x) → p ≡ q
-proof-irrelevance-[]= here            here             = refl
-proof-irrelevance-[]= (there xs[i]=x) (there xs[i]=x') =
-  P.cong there (proof-irrelevance-[]= xs[i]=x xs[i]=x')
-
--- _[_]=_ can be expressed using lookup and _≡_.
-
-[]=↔lookup : ∀ {a n i} {A : Set a} {x} {xs : Vec A n} →
-             xs [ i ]= x ↔ lookup i xs ≡ x
-[]=↔lookup {i = i} {x = x} {xs} = record
-  { to         = P.→-to-⟶ to
-  ; from       = P.→-to-⟶ (from i xs)
-  ; inverse-of = record
-    { left-inverse-of  = λ _ → proof-irrelevance-[]= _ _
-    ; right-inverse-of = λ _ → P.proof-irrelevance _ _
-    }
-  }
-  where
-  to : ∀ {n xs} {i : Fin n} → xs [ i ]= x → lookup i xs ≡ x
-  to here            = refl
-  to (there xs[i]=x) = to xs[i]=x
-
-  from : ∀ {n} (i : Fin n) xs → lookup i xs ≡ x → xs [ i ]= x
-  from zero    (.x ∷ _)  refl = here
-  from (suc i) (_  ∷ xs) p    = there (from i xs p)
+------------------------------------------------------------------------
+-- foldl
+
+foldl-cong : ∀ {a b} {A : Set a}
+             {B : ℕ → Set b} {f : ∀ {n} → B n → A → B (suc n)} {d}
+             {C : ℕ → Set b} {g : ∀ {n} → C n → A → C (suc n)} {e} →
+             (∀ {n x} {y : B n} {z : C n} → y ≅ z → f y x ≅ g z x) →
+             d ≅ e → ∀ {n} (xs : Vec A n) →
+             foldl B f d xs ≅ foldl C g e xs
+foldl-cong _   d≅e []       = d≅e
+foldl-cong f≅g d≅e (x ∷ xs) = foldl-cong f≅g (f≅g d≅e) xs
 
 ------------------------------------------------------------------------
--- Some properties related to _[_]≔_
-
-[]≔-idempotent :
-  ∀ {n a} {A : Set a} (xs : Vec A n) (i : Fin n) {x₁ x₂ : A} →
-  (xs [ i ]≔ x₁) [ i ]≔ x₂ ≡ xs [ i ]≔ x₂
-[]≔-idempotent []       ()
-[]≔-idempotent (x ∷ xs) zero    = refl
-[]≔-idempotent (x ∷ xs) (suc i) = P.cong (_∷_ x) $ []≔-idempotent xs i
-
-[]≔-commutes :
-  ∀ {n a} {A : Set a} (xs : Vec A n) (i j : Fin n) {x y : A} →
-  i ≢ j → (xs [ i ]≔ x) [ j ]≔ y ≡ (xs [ j ]≔ y) [ i ]≔ x
-[]≔-commutes []       ()      ()      _
-[]≔-commutes (x ∷ xs) zero    zero    0≢0 = ⊥-elim $ 0≢0 refl
-[]≔-commutes (x ∷ xs) zero    (suc i) _   = refl
-[]≔-commutes (x ∷ xs) (suc i) zero    _   = refl
-[]≔-commutes (x ∷ xs) (suc i) (suc j) i≢j =
-  P.cong (_∷_ x) $ []≔-commutes xs i j (i≢j ∘ P.cong suc)
-
-[]≔-updates : ∀ {n a} {A : Set a} (xs : Vec A n) (i : Fin n) {x : A} →
-              (xs [ i ]≔ x) [ i ]= x
-[]≔-updates []       ()
-[]≔-updates (x ∷ xs) zero    = here
-[]≔-updates (x ∷ xs) (suc i) = there ([]≔-updates xs i)
-
-[]≔-minimal :
-  ∀ {n a} {A : Set a} (xs : Vec A n) (i j : Fin n) {x y : A} →
-  i ≢ j → xs [ i ]= x → (xs [ j ]≔ y) [ i ]= x
-[]≔-minimal []       ()      ()      _   _
-[]≔-minimal (x ∷ xs) .zero   zero    0≢0 here        = ⊥-elim $ 0≢0 refl
-[]≔-minimal (x ∷ xs) .zero   (suc j) _   here        = here
-[]≔-minimal (x ∷ xs) (suc i) zero    _   (there loc) = there loc
-[]≔-minimal (x ∷ xs) (suc i) (suc j) i≢j (there loc) =
-  there ([]≔-minimal xs i j (i≢j ∘ P.cong suc) loc)
+-- sum
 
-map-[]≔ : ∀ {n a b} {A : Set a} {B : Set b}
-          (f : A → B) (xs : Vec A n) (i : Fin n) {x : A} →
-          map f (xs [ i ]≔ x) ≡ map f xs [ i ]≔ f x
-map-[]≔ f []       ()
-map-[]≔ f (x ∷ xs) zero    = refl
-map-[]≔ f (x ∷ xs) (suc i) = P.cong (_∷_ _) $ map-[]≔ f xs i
-
-[]≔-lookup : ∀ {a} {A : Set a} {n} (xs : Vec A n) (i : Fin n) →
-             xs [ i ]≔ lookup i xs ≡ xs
-[]≔-lookup []       ()
-[]≔-lookup (x ∷ xs) zero    = refl
-[]≔-lookup (x ∷ xs) (suc i) = P.cong (_∷_ x) $ []≔-lookup xs i
-
-[]≔-++-inject+ : ∀ {a} {A : Set a} {m n x}
-                 (xs : Vec A m) (ys : Vec A n) i →
-                 (xs ++ ys) [ Fin.inject+ n i ]≔ x ≡ xs [ i ]≔ x ++ ys
-[]≔-++-inject+ []       ys ()
-[]≔-++-inject+ (x ∷ xs) ys zero    = refl
-[]≔-++-inject+ (x ∷ xs) ys (suc i) =
-  P.cong (_∷_ x) $ []≔-++-inject+ xs ys i
+sum-++-commute : ∀ {m n} (xs : Vec ℕ m) {ys : Vec ℕ n} →
+                 sum (xs ++ ys) ≡ sum xs + sum ys
+sum-++-commute []       {_}  = refl
+sum-++-commute (x ∷ xs) {ys} = begin
+  x + sum (xs ++ ys)     ≡⟨ P.cong (x +_) (sum-++-commute xs) ⟩
+  x + (sum xs + sum ys)  ≡⟨ P.sym (+-assoc x (sum xs) (sum ys)) ⟩
+  sum (x ∷ xs) + sum ys  ∎
+  where open P.≡-Reasoning
 
 ------------------------------------------------------------------------
--- Some properties related to zipping and unzipping.
-
--- Products of vectors are isomorphic to vectors of products.
-
-unzip∘zip : ∀ {a n} {A B : Set a} (xs : Vec A n) (ys : Vec B n) →
-            unzip (zip xs ys) ≡ (xs , ys)
-unzip∘zip [] []             = refl
-unzip∘zip (x ∷ xs) (y ∷ ys) =
-  P.cong (Prod.map (_∷_ x) (_∷_ y)) (unzip∘zip xs ys)
-
-zip∘unzip : ∀ {a n} {A B : Set a} (xys : Vec (A × B) n) →
-            (Prod.uncurry zip) (unzip xys) ≡ xys
-zip∘unzip []              = refl
-zip∘unzip ((x , y) ∷ xys) = P.cong (_∷_ (x , y)) (zip∘unzip xys)
-
-×v↔v× : ∀ {a n} {A B : Set a} → (Vec A n × Vec B n) ↔ Vec (A × B) n
-×v↔v× = record
-  { to         = P.→-to-⟶ (Prod.uncurry zip)
-  ; from       = P.→-to-⟶ unzip
-  ; inverse-of = record
-    { left-inverse-of  = Prod.uncurry unzip∘zip
-    ; right-inverse-of = zip∘unzip
-    }
-  }
-
--- map lifts projections to vectors of products.
-
-map-proj₁-zip : ∀ {a n} {A B : Set a} (xs : Vec A n) (ys : Vec B n) →
-                map proj₁ (zip xs ys) ≡ xs
-map-proj₁-zip []       []       = refl
-map-proj₁-zip (x ∷ xs) (y ∷ ys) = P.cong (_∷_ x) (map-proj₁-zip xs ys)
-
-map-proj₂-zip : ∀ {a n} {A B : Set a} (xs : Vec A n) (ys : Vec B n) →
-                map proj₂ (zip xs ys) ≡ ys
-map-proj₂-zip []       []       = refl
-map-proj₂-zip (x ∷ xs) (y ∷ ys) = P.cong (_∷_ y) (map-proj₂-zip xs ys)
+-- replicate
 
--- map lifts pairing to vectors of products.
+lookup-replicate : ∀ {a n} {A : Set a} (i : Fin n) (x : A) →
+                   lookup i (replicate x) ≡ x
+lookup-replicate zero    = λ _ → refl
+lookup-replicate (suc i) = lookup-replicate i
 
-map-<,>-zip : ∀ {a n} {A B₁ B₂ : Set a}
-              (f : A → B₁) (g : A → B₂) (xs : Vec A n) →
-              map < f , g > xs ≡ zip (map f xs) (map g xs)
-map-<,>-zip f g []       = P.refl
-map-<,>-zip f g (x ∷ xs) = P.cong (_∷_ (f x , g x)) (map-<,>-zip f g xs)
+map-replicate :  ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (x : A) →
+                 ∀ n → map f (replicate x) ≡ replicate {n = n} (f x)
+map-replicate f x zero = refl
+map-replicate f x (suc n) = P.cong (f x ∷_) (map-replicate f x n)
 
-map-zip : ∀ {a n} {A₁ A₂ B₁ B₂ : Set a}
-          (f : A₁ → A₂) (g : B₁ → B₂) (xs : Vec A₁ n) (ys : Vec B₁ n) →
-          map (Prod.map f g) (zip xs ys) ≡ zip (map f xs) (map g ys)
-map-zip f g []       []       = refl
-map-zip f g (x ∷ xs) (y ∷ ys) = P.cong (_∷_ (f x , g y)) (map-zip f g xs ys)
-
-map-unzip : ∀ {a n} {A₁ A₂ B₁ B₂ : Set a}
-            (f : A₁ → A₂) (g : B₁ → B₂) (xys : Vec (A₁ × B₁) n) →
-            let xs , ys = unzip xys
-            in (map f xs , map g ys) ≡ unzip (map (Prod.map f g) xys)
-map-unzip f g []              = refl
-map-unzip f g ((x , y) ∷ xys) =
-  P.cong (Prod.map (_∷_ (f x)) (_∷_ (g y))) (map-unzip f g xys)
-
--- lookup is homomorphic with respect to the product structure.
-
-lookup-unzip : ∀ {a n} {A B : Set a} (i : Fin n) (xys : Vec (A × B) n) →
-               let xs , ys = unzip xys
-               in (lookup i xs , lookup i ys) ≡ lookup i xys
-lookup-unzip ()      []
-lookup-unzip zero    ((x , y) ∷ xys) = refl
-lookup-unzip (suc i) ((x , y) ∷ xys) = lookup-unzip i xys
-
-lookup-zip : ∀ {a n} {A B : Set a}
-             (i : Fin n) (xs : Vec A n) (ys : Vec B n) →
-             lookup i (zip xs ys) ≡ (lookup i xs , lookup i ys)
-lookup-zip i xs ys = begin
-  lookup i (zip xs ys)
-    ≡⟨ P.sym (lookup-unzip i (zip xs ys)) ⟩
-  lookup i (proj₁ (unzip (zip xs ys))) , lookup i (proj₂ (unzip (zip xs ys)))
-    ≡⟨ P.cong₂ _,_ (P.cong (lookup i ∘ proj₁) (unzip∘zip xs ys))
-                   (P.cong (lookup i ∘ proj₂) (unzip∘zip xs ys)) ⟩
-  lookup i xs , lookup i ys
-    ∎
+module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where
+
+  zipWith-replicate₁ : ∀ {n} (_⊕_ : A → B → C) (x : A) (ys : Vec B n) →
+                     zipWith _⊕_ (replicate x) ys ≡ map (x ⊕_) ys
+  zipWith-replicate₁ _⊕_ x []       = refl
+  zipWith-replicate₁ _⊕_ x (y ∷ ys) =
+    P.cong (x ⊕ y ∷_) (zipWith-replicate₁ _⊕_ x ys)
+
+  zipWith-replicate₂ : ∀ {n} (_⊕_ : A → B → C) (xs : Vec A n) (y : B) →
+                     zipWith _⊕_ xs (replicate y) ≡ map (_⊕ y) xs
+  zipWith-replicate₂ _⊕_ []       y = refl
+  zipWith-replicate₂ _⊕_ (x ∷ xs) y =
+    P.cong (x ⊕ y ∷_) (zipWith-replicate₂ _⊕_ xs y)
+
+------------------------------------------------------------------------
+-- tabulate
+
+lookup∘tabulate : ∀ {a n} {A : Set a} (f : Fin n → A) (i : Fin n) →
+                  lookup i (tabulate f) ≡ f i
+lookup∘tabulate f zero    = refl
+lookup∘tabulate f (suc i) = lookup∘tabulate (f ∘ suc) i
+
+tabulate∘lookup : ∀ {a n} {A : Set a} (xs : Vec A n) →
+                  tabulate (flip lookup xs) ≡ xs
+tabulate∘lookup []       = refl
+tabulate∘lookup (x ∷ xs) = P.cong (x ∷_) (tabulate∘lookup xs)
+
+tabulate-∘ : ∀ {n a b} {A : Set a} {B : Set b}
+             (f : A → B) (g : Fin n → A) →
+             tabulate (f ∘ g) ≡ map f (tabulate g)
+tabulate-∘ {zero}  f g = refl
+tabulate-∘ {suc n} f g = P.cong (f (g zero) ∷_) (tabulate-∘ f (g ∘ suc))
+
+tabulate-cong : ∀ {n a} {A : Set a} {f g : Fin n → A} → f ≗ g → tabulate f ≡ tabulate g
+tabulate-cong {zero} p = refl
+tabulate-cong {suc n} p = P.cong₂ _∷_ (p zero) (tabulate-cong (p ∘ suc))
+
+------------------------------------------------------------------------
+-- allFin
+
+lookup-allFin : ∀ {n} (i : Fin n) → lookup i (allFin n) ≡ i
+lookup-allFin = lookup∘tabulate id
+
+allFin-map : ∀ n → allFin (suc n) ≡ zero ∷ map suc (allFin n)
+allFin-map n = P.cong (zero ∷_) $ tabulate-∘ suc id
+
+tabulate-allFin : ∀ {n a} {A : Set a} (f : Fin n → A) →
+                  tabulate f ≡ map f (allFin n)
+tabulate-allFin f = tabulate-∘ f id
+
+-- If you look up every possible index, in increasing order, then you
+-- get back the vector you started with.
+
+map-lookup-allFin : ∀ {a} {A : Set a} {n} (xs : Vec A n) →
+                    map (λ x → lookup x xs) (allFin n) ≡ xs
+map-lookup-allFin {n = n} xs = begin
+  map (λ x → lookup x xs) (allFin n) ≡⟨ P.sym $ tabulate-∘ (λ x → lookup x xs) id ⟩
+  tabulate (λ x → lookup x xs)       ≡⟨ tabulate∘lookup xs ⟩
+  xs                                 ∎
   where open P.≡-Reasoning
+
+------------------------------------------------------------------------
+-- count
+
+module _ {a p} {A : Set a} {P : Pred A p} (P? : Decidable P) where
+
+  count≤n : ∀ {n} (xs : Vec A n) → count P? xs ≤ n
+  count≤n []       = z≤n
+  count≤n (x ∷ xs) with P? x
+  ... | yes _ = s≤s (count≤n xs)
+  ... | no  _ = ≤-step (count≤n xs)
+
+------------------------------------------------------------------------
+-- insert
+
+module _ {a} {A : Set a} where
+
+  insert-lookup : ∀ {n} (i : Fin (suc n)) (x : A)
+                  (xs : Vec A n) → lookup i (insert i x xs) ≡ x
+  insert-lookup zero x xs = refl
+  insert-lookup (suc ()) x []
+  insert-lookup (suc i) x (y ∷ xs) = insert-lookup i x xs
+
+  insert-punchIn : ∀ {n} (i : Fin (suc n)) (x : A) (xs : Vec A n)
+                   (j : Fin n) →
+                   lookup (Fin.punchIn i j) (insert i x xs) ≡ lookup j xs
+  insert-punchIn zero x xs j = refl
+  insert-punchIn (suc ()) x [] j
+  insert-punchIn (suc i) x (y ∷ xs) zero = refl
+  insert-punchIn (suc i) x (y ∷ xs) (suc j) = insert-punchIn i x xs j
+
+  remove-punchOut : ∀ {n} (xs : Vec A (suc n))
+                    {i : Fin (suc n)} {j : Fin (suc n)} (i≢j : i ≢ j) →
+                    lookup (Fin.punchOut i≢j) (remove i xs) ≡ lookup j xs
+  remove-punchOut (x ∷ xs) {zero} {zero} i≢j = ⊥-elim (i≢j refl)
+  remove-punchOut (x ∷ xs) {zero} {suc j} i≢j = refl
+  remove-punchOut (x ∷ []) {suc ()} {j} i≢j
+  remove-punchOut (x ∷ y ∷ xs) {suc i} {zero} i≢j = refl
+  remove-punchOut (x ∷ y ∷ xs) {suc i} {suc j} i≢j =
+    remove-punchOut (y ∷ xs) (i≢j ∘ P.cong suc)
+
+------------------------------------------------------------------------
+-- remove
+
+  remove-insert : ∀ {n} (i : Fin (suc n)) (x : A) (xs : Vec A n) →
+                  remove i (insert i x xs) ≡ xs
+  remove-insert zero x xs = refl
+  remove-insert (suc ()) x []
+  remove-insert (suc zero) x (y ∷ xs) = refl
+  remove-insert (suc (suc ())) x (y ∷ [])
+  remove-insert (suc (suc i)) x (y ∷ z ∷ xs) =
+    P.cong (y ∷_) (remove-insert (suc i) x (z ∷ xs))
+
+  insert-remove : ∀ {n} (i : Fin (suc n)) (xs : Vec A (suc n)) →
+                  insert i (lookup i xs) (remove i xs) ≡ xs
+  insert-remove zero (x ∷ xs) = refl
+  insert-remove (suc ()) (x ∷ [])
+  insert-remove (suc i) (x ∷ y ∷ xs) =
+    P.cong (x ∷_) (insert-remove i (y ∷ xs))
+
+------------------------------------------------------------------------
+-- Conversion function
+
+module _ {a} {A : Set a} where
+
+  toList∘fromList : (xs : List A) → toList (fromList xs) ≡ xs
+  toList∘fromList List.[]       = refl
+  toList∘fromList (x List.∷ xs) = P.cong (x List.∷_) (toList∘fromList xs)
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 0.15
+
+proof-irrelevance-[]= = []=-irrelevance
+{-# WARNING_ON_USAGE proof-irrelevance-[]=
+"Warning: proof-irrelevance-[]= was deprecated in v0.15.
+Please use []=-irrelevance instead."
+#-}
diff --git a/src/Data/Vec/Relation/Equality/DecPropositional.agda b/src/Data/Vec/Relation/Equality/DecPropositional.agda
new file mode 100644
index 0000000..d5b39e6
--- /dev/null
+++ b/src/Data/Vec/Relation/Equality/DecPropositional.agda
@@ -0,0 +1,22 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Decidable vector equality over propositional equality
+------------------------------------------------------------------------
+
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+
+module Data.Vec.Relation.Equality.DecPropositional
+  {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_) where
+
+import Data.Vec.Relation.Equality.Propositional as PEq
+import Data.Vec.Relation.Equality.DecSetoid as DSEq
+
+------------------------------------------------------------------------
+-- Publically re-export everything from decSetoid and propositional
+-- equality
+
+open PEq public
+open DSEq (decSetoid _≟_) public
+  using (_≋?_; ≋-isDecEquivalence; ≋-decSetoid)
diff --git a/src/Data/Vec/Relation/Equality/DecSetoid.agda b/src/Data/Vec/Relation/Equality/DecSetoid.agda
new file mode 100644
index 0000000..6fbba08
--- /dev/null
+++ b/src/Data/Vec/Relation/Equality/DecSetoid.agda
@@ -0,0 +1,37 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Decidable semi-heterogeneous vector equality over setoids
+------------------------------------------------------------------------
+
+open import Relation.Binary
+
+module Data.Vec.Relation.Equality.DecSetoid
+  {a ℓ} (DS : DecSetoid a ℓ) where
+
+open import Data.Nat using (ℕ)
+import Data.Vec.Relation.Equality.Setoid as Equality
+import Data.Vec.Relation.Pointwise.Inductive as PW
+open import Level using (_⊔_)
+open import Relation.Binary using (Decidable)
+
+open DecSetoid DS
+
+------------------------------------------------------------------------
+-- Make all definitions from equality available
+
+open Equality setoid public
+
+------------------------------------------------------------------------
+-- Additional properties
+
+infix 4 _≋?_
+
+_≋?_ : ∀ {m n} → Decidable (_≋_ {m} {n})
+_≋?_ = PW.decidable _≟_
+
+≋-isDecEquivalence : ∀ n → IsDecEquivalence (_≋_ {n})
+≋-isDecEquivalence = PW.isDecEquivalence isDecEquivalence
+
+≋-decSetoid : ℕ → DecSetoid a (a ⊔ ℓ)
+≋-decSetoid = PW.decSetoid DS
diff --git a/src/Data/Vec/Relation/Equality/Propositional.agda b/src/Data/Vec/Relation/Equality/Propositional.agda
new file mode 100644
index 0000000..a87df3d
--- /dev/null
+++ b/src/Data/Vec/Relation/Equality/Propositional.agda
@@ -0,0 +1,36 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Vector equality over propositional equality
+------------------------------------------------------------------------
+
+open import Relation.Binary
+
+module Data.Vec.Relation.Equality.Propositional {a} {A : Set a} where
+
+open import Data.Nat.Base using (ℕ; zero; suc; _+_)
+open import Data.Vec
+open import Data.Vec.Relation.Pointwise.Inductive
+  using (Pointwise-≡⇒≡; ≡⇒Pointwise-≡)
+import Data.Vec.Relation.Equality.Setoid as SEq
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.HeterogeneousEquality as H using (_≅_)
+
+------------------------------------------------------------------------
+-- Publically re-export everything from setoid equality
+
+open SEq (setoid A) public
+
+------------------------------------------------------------------------
+-- ≋ is propositional
+
+≋⇒≡ : ∀ {n} {xs ys : Vec A n} → xs ≋ ys → xs ≡ ys
+≋⇒≡ = Pointwise-≡⇒≡
+
+≡⇒≋ : ∀ {n} {xs ys : Vec A n} → xs ≡ ys → xs ≋ ys
+≡⇒≋ = ≡⇒Pointwise-≡
+
+≋⇒≅ : ∀ {m n} {xs : Vec A m} {ys : Vec A n} →
+          xs ≋ ys → xs ≅ ys
+≋⇒≅ p with length-equal p
+... | refl = H.≡-to-≅ (≋⇒≡ p)
diff --git a/src/Data/Vec/Relation/Equality/Setoid.agda b/src/Data/Vec/Relation/Equality/Setoid.agda
new file mode 100644
index 0000000..0928a39
--- /dev/null
+++ b/src/Data/Vec/Relation/Equality/Setoid.agda
@@ -0,0 +1,87 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Semi-heterogeneous vector equality over setoids
+------------------------------------------------------------------------
+
+open import Relation.Binary
+
+module Data.Vec.Relation.Equality.Setoid {a ℓ} (S : Setoid a ℓ) where
+
+open import Data.Nat.Base using (ℕ; zero; suc; _+_)
+open import Data.Vec
+open import Data.Vec.Relation.Pointwise.Inductive as PW
+  using (Pointwise)
+open import Function
+open import Level using (_⊔_)
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.HeterogeneousEquality as H using (_≅_)
+
+open Setoid S renaming (Carrier to A)
+
+------------------------------------------------------------------------
+-- Definition of equality
+
+infix 4 _≋_
+
+_≋_ : ∀ {m n} → REL (Vec A m) (Vec A n) (a ⊔ ℓ)
+_≋_ = Pointwise _≈_
+
+open Pointwise public using ([]; _∷_)
+open PW public using (length-equal)
+
+------------------------------------------------------------------------
+-- Relational properties
+
+≋-refl : ∀ {n} → Reflexive (_≋_ {n})
+≋-refl = PW.refl refl
+
+≋-sym : ∀ {n m} → Sym _≋_ (_≋_ {m} {n})
+≋-sym = PW.sym sym
+
+≋-trans : ∀ {n m o} → Trans (_≋_ {m}) (_≋_ {n} {o}) (_≋_)
+≋-trans = PW.trans trans
+
+≋-isEquivalence : ∀ n → IsEquivalence (_≋_ {n})
+≋-isEquivalence = PW.isEquivalence isEquivalence
+
+≋-setoid : ℕ → Setoid a (a ⊔ ℓ)
+≋-setoid = PW.setoid S
+
+------------------------------------------------------------------------
+-- map
+
+open PW public using ( map⁺)
+
+------------------------------------------------------------------------
+-- ++
+
+open PW public using (++⁺ ; ++⁻ ; ++ˡ⁻; ++ʳ⁻)
+
+++-identityˡ : ∀ {n} (xs : Vec A n) → [] ++ xs ≋ xs
+++-identityˡ _ = ≋-refl
+
+++-identityʳ : ∀ {n} (xs : Vec A n) → xs ++ [] ≋ xs
+++-identityʳ []       = []
+++-identityʳ (x ∷ xs) = refl ∷ ++-identityʳ xs
+
+map-++-commute : ∀ {b m n} {B : Set b}
+                   (f : B → A) (xs : Vec B m) {ys : Vec B n} →
+                   map f (xs ++ ys) ≋ map f xs ++ map f ys
+map-++-commute f []       = ≋-refl
+map-++-commute f (x ∷ xs) = refl ∷ map-++-commute f xs
+
+------------------------------------------------------------------------
+-- concat
+
+open PW public using (concat⁺; concat⁻)
+
+------------------------------------------------------------------------
+-- replicate
+
+replicate-shiftʳ : ∀ {m} n x (xs : Vec A m) →
+                  replicate {n = n}     x ++ (x ∷ xs) ≋
+                  replicate {n = 1 + n} x ++      xs
+replicate-shiftʳ zero    x xs = ≋-refl
+replicate-shiftʳ (suc n) x xs = refl ∷ (replicate-shiftʳ n x xs)
diff --git a/src/Data/Vec/Relation/Pointwise/Extensional.agda b/src/Data/Vec/Relation/Pointwise/Extensional.agda
new file mode 100644
index 0000000..2291358
--- /dev/null
+++ b/src/Data/Vec/Relation/Pointwise/Extensional.agda
@@ -0,0 +1,227 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Extensional pointwise lifting of relations to vectors
+------------------------------------------------------------------------
+
+module Data.Vec.Relation.Pointwise.Extensional where
+
+open import Data.Fin using (zero; suc)
+open import Data.Nat using (zero; suc)
+open import Data.Vec as Vec hiding ([_]; head; tail; map)
+open import Data.Vec.Relation.Pointwise.Inductive as Inductive
+  using ([]; _∷_)
+  renaming (Pointwise to IPointwise)
+open import Level using (_⊔_)
+open import Function using (_∘_)
+open import Function.Equality using (_⟨$⟩_)
+open import Function.Equivalence as Equiv
+  using (_⇔_; ⇔-setoid; equivalence; module Equivalence)
+open import Level using (_⊔_) renaming (zero to ℓ₀)
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.Construct.Closure.Transitive as Plus
+  hiding (equivalent; map)
+open import Relation.Nullary
+import Relation.Nullary.Decidable as Dec
+
+record Pointwise {a b ℓ} {A : Set a} {B : Set b} (_∼_ : REL A B ℓ)
+                 {n} (xs : Vec A n) (ys : Vec B n) : Set (a ⊔ b ⊔ ℓ)
+                 where
+  constructor ext
+  field app : ∀ i → lookup i xs ∼ lookup i ys
+
+------------------------------------------------------------------------
+-- Operations
+
+head : ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ}
+       {n x y xs} {ys : Vec B n} →
+       Pointwise _∼_ (x ∷ xs) (y ∷ ys) → x ∼ y
+head (ext app) = app zero
+
+tail : ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ}
+       {n x y xs} {ys : Vec B n} →
+       Pointwise _∼_ (x ∷ xs) (y ∷ ys) → Pointwise _∼_ xs ys
+tail (ext app) = ext (app ∘ suc)
+
+map : ∀ {a b ℓ} {A : Set a} {B : Set b} {_~_ _~′_ : REL A B ℓ} {n} →
+      _~_ ⇒ _~′_ → Pointwise _~_ ⇒ Pointwise _~′_ {n}
+map ~⇒~′ xs~ys = ext (~⇒~′ ∘ Pointwise.app xs~ys)
+
+gmap : ∀ {a b ℓ} {A : Set a} {B : Set b}
+       {_~_ : Rel A ℓ} {_~′_ : Rel B ℓ} {f : A → B} {n} →
+       _~_ =[ f ]⇒ _~′_ →
+       Pointwise _~_ =[ Vec.map {n = n} f ]⇒ Pointwise _~′_
+gmap {_}          ~⇒~′ {[]}      {[]}      xs~ys = ext λ()
+gmap {_~′_ = _~′_} ~⇒~′ {x ∷ xs} {y ∷ ys} xs~ys = ext λ
+  { zero    → ~⇒~′ (head xs~ys)
+  ; (suc i) → Pointwise.app (gmap {_~′_ = _~′_} ~⇒~′ (tail xs~ys)) i
+  }
+
+------------------------------------------------------------------------
+-- The inductive and extensional definitions are equivalent.
+
+module _ {a b ℓ} {A : Set a} {B : Set b} {_~_ : REL A B ℓ} where
+
+  extensional⇒inductive : ∀ {n} {xs : Vec A n} {ys : Vec B n} →
+                           Pointwise _~_ xs ys → IPointwise _~_ xs ys
+  extensional⇒inductive {zero} {[]}       {[]}      xs~ys = []
+  extensional⇒inductive {suc n} {x ∷ xs} {y ∷ ys} xs~ys =
+    (head xs~ys) ∷ extensional⇒inductive (tail xs~ys)
+
+  inductive⇒extensional : ∀ {n} {xs : Vec A n} {ys : Vec B n} →
+                           IPointwise _~_ xs ys → Pointwise _~_ xs ys
+  inductive⇒extensional []             = ext λ()
+  inductive⇒extensional (x~y ∷ xs~ys) = ext λ
+    { zero    → x~y
+    ; (suc i) → Pointwise.app (inductive⇒extensional xs~ys) i
+    }
+
+  equivalent : ∀ {n} {xs : Vec A n} {ys : Vec B n} →
+               Pointwise _~_ xs ys ⇔ IPointwise _~_ xs ys
+  equivalent = equivalence extensional⇒inductive inductive⇒extensional
+
+------------------------------------------------------------------------
+-- Relational properties
+
+refl : ∀ {a ℓ} {A : Set a} {_~_ : Rel A ℓ} →
+       ∀ {n} → Reflexive _~_ → Reflexive (Pointwise _~_ {n = n})
+refl ~-rfl = ext (λ _ → ~-rfl)
+
+sym : ∀ {a b ℓ} {A : Set a} {B : Set b} {P : REL A B ℓ} {Q : REL B A ℓ}
+      {n} → Sym P Q → Sym (Pointwise P) (Pointwise Q {n = n})
+sym sm xs∼ys = ext λ i → sm (Pointwise.app xs∼ys i)
+
+trans : ∀ {a b c ℓ} {A : Set a} {B : Set b} {C : Set c}
+        {P : REL A B ℓ} {Q : REL B C ℓ} {R : REL A C ℓ} {n} →
+        Trans P Q R →
+        Trans (Pointwise P) (Pointwise Q) (Pointwise R {n = n})
+trans trns xs∼ys ys∼zs = ext λ i →
+  trns (Pointwise.app xs∼ys i) (Pointwise.app ys∼zs i)
+
+decidable : ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} →
+            Decidable _∼_ → ∀ {n} → Decidable (Pointwise _∼_ {n = n})
+decidable dec xs ys = Dec.map
+  (Setoid.sym (⇔-setoid _) equivalent)
+  (Inductive.decidable dec xs ys)
+
+isEquivalence : ∀ {a ℓ} {A : Set a} {_~_ : Rel A ℓ} →
+                ∀ {n} → IsEquivalence _~_ →
+                IsEquivalence (Pointwise _~_ {n = n})
+isEquivalence equiv = record
+  { refl  = refl  (IsEquivalence.refl  equiv)
+  ; sym   = sym   (IsEquivalence.sym   equiv)
+  ; trans = trans (IsEquivalence.trans equiv)
+  }
+
+isDecEquivalence : ∀ {a ℓ} {A : Set a} {_~_ : Rel A ℓ} →
+                   ∀ {n} → IsDecEquivalence _~_ →
+                   IsDecEquivalence (Pointwise _~_ {n = n})
+isDecEquivalence decEquiv = record
+  { isEquivalence = isEquivalence (IsDecEquivalence.isEquivalence decEquiv)
+  ; _≟_           = decidable (IsDecEquivalence._≟_ decEquiv)
+  }
+
+------------------------------------------------------------------------
+-- Pointwise _≡_ is equivalent to _≡_.
+
+module _ {a} {A : Set a} where
+
+  Pointwise-≡⇒≡ : ∀ {n} {xs ys : Vec A n} →
+                     Pointwise _≡_ xs ys → xs ≡ ys
+  Pointwise-≡⇒≡ {zero}  {[]}      {[]}      (ext app) = P.refl
+  Pointwise-≡⇒≡ {suc n} {x ∷ xs} {y ∷ ys} xs~ys =
+    P.cong₂ _∷_ (head xs~ys) (Pointwise-≡⇒≡ (tail xs~ys))
+
+  ≡⇒Pointwise-≡ : ∀ {n} {xs ys : Vec A n} →
+                     xs ≡ ys → Pointwise _≡_ xs ys
+  ≡⇒Pointwise-≡ P.refl = refl P.refl
+
+  Pointwise-≡↔≡ : ∀ {n} {xs ys : Vec A n} →
+                Pointwise _≡_ xs ys ⇔ xs ≡ ys
+  Pointwise-≡↔≡ {ℓ} {A} =
+    Equiv.equivalence Pointwise-≡⇒≡ ≡⇒Pointwise-≡
+
+------------------------------------------------------------------------
+-- Pointwise and Plus commute when the underlying relation is
+-- reflexive.
+module _ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} where
+
+  ⁺∙⇒∙⁺ : ∀ {n} {xs ys : Vec A n} →
+          Plus (Pointwise _∼_) xs ys → Pointwise (Plus _∼_) xs ys
+  ⁺∙⇒∙⁺ [ ρ≈ρ′ ]            = ext (λ x → [ Pointwise.app ρ≈ρ′ x ])
+  ⁺∙⇒∙⁺ (ρ ∼⁺⟨ ρ≈ρ′ ⟩ ρ′≈ρ″) =  ext (λ x →
+    _ ∼⁺⟨ Pointwise.app (⁺∙⇒∙⁺ ρ≈ρ′ ) x ⟩
+         Pointwise.app (⁺∙⇒∙⁺ ρ′≈ρ″) x)
+
+  ∙⁺⇒⁺∙ : ∀ {n} {xs ys : Vec A n} → Reflexive _∼_ →
+          Pointwise (Plus _∼_) xs ys → Plus (Pointwise _∼_) xs ys
+  ∙⁺⇒⁺∙ rfl =
+    Plus.map (_⟨$⟩_ (Equivalence.from equivalent)) ∘
+    helper ∘
+    _⟨$⟩_ (Equivalence.to equivalent)
+    where
+    helper : ∀ {n} {xs ys : Vec A n} →
+             IPointwise (Plus _∼_) xs ys → Plus (IPointwise _∼_) xs ys
+    helper []                                                  = [ [] ]
+    helper (_∷_ {x = x} {y = y} {xs = xs} {ys = ys} x∼y xs∼ys) =
+      x ∷ xs  ∼⁺⟨ Plus.map (_∷ Inductive.refl rfl) x∼y ⟩
+      y ∷ xs  ∼⁺⟨ Plus.map (rfl ∷_) (helper xs∼ys) ⟩∎
+      y ∷ ys  ∎
+
+-- ∙⁺⇒⁺∙ cannot be defined if the requirement of reflexivity
+-- is dropped.
+private
+
+ module Counterexample where
+
+  data D : Set where
+    i j x y z : D
+
+  data _R_ : Rel D ℓ₀ where
+    iRj : i R j
+    xRy : x R y
+    yRz : y R z
+
+  xR⁺z : x [ _R_ ]⁺ z
+  xR⁺z =
+    x  ∼⁺⟨ [ xRy ] ⟩
+    y  ∼⁺⟨ [ yRz ] ⟩∎
+    z  ∎
+
+  ix : Vec D 2
+  ix = i ∷ x ∷ []
+
+  jz : Vec D 2
+  jz = j ∷ z ∷ []
+
+  ix∙⁺jz : IPointwise (Plus _R_) ix jz
+  ix∙⁺jz = [ iRj ] ∷ xR⁺z ∷ []
+
+  ¬ix⁺∙jz : ¬ Plus′ (IPointwise _R_) ix jz
+  ¬ix⁺∙jz [ iRj ∷ () ∷ [] ]
+  ¬ix⁺∙jz ((iRj ∷ xRy ∷ []) ∷ [ () ∷ yRz ∷ [] ])
+  ¬ix⁺∙jz ((iRj ∷ xRy ∷ []) ∷ (() ∷ yRz ∷ []) ∷ _)
+
+  counterexample :
+    ¬ (∀ {n} {xs ys : Vec D n} →
+         Pointwise (Plus _R_) xs ys →
+         Plus (Pointwise _R_) xs ys)
+  counterexample ∙⁺⇒⁺∙ =
+    ¬ix⁺∙jz (Equivalence.to Plus.equivalent ⟨$⟩
+               Plus.map (_⟨$⟩_ (Equivalence.to equivalent))
+                 (∙⁺⇒⁺∙ (Equivalence.from equivalent ⟨$⟩ ix∙⁺jz)))
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 0.15
+
+Pointwise-≡ = Pointwise-≡↔≡
+{-# WARNING_ON_USAGE Pointwise-≡
+"Warning: Pointwise-≡ was deprecated in v0.15.
+Please use Pointwise-≡↔≡ instead."
+#-}
diff --git a/src/Data/Vec/Relation/Pointwise/Inductive.agda b/src/Data/Vec/Relation/Pointwise/Inductive.agda
new file mode 100644
index 0000000..d837c09
--- /dev/null
+++ b/src/Data/Vec/Relation/Pointwise/Inductive.agda
@@ -0,0 +1,258 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Inductive pointwise lifting of relations to vectors
+------------------------------------------------------------------------
+
+module Data.Vec.Relation.Pointwise.Inductive where
+
+open import Algebra.FunctionProperties
+open import Data.Fin using (Fin; zero; suc)
+open import Data.Nat using (ℕ; zero; suc)
+open import Data.Product using (_×_; _,_)
+open import Data.Vec as Vec hiding ([_]; head; tail; map; lookup)
+open import Data.Vec.All using (All; []; _∷_)
+open import Level using (_⊔_)
+open import Function using (_∘_)
+open import Function.Equivalence using (_⇔_; equivalence)
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Nullary
+
+------------------------------------------------------------------------
+-- Relation
+
+infixr 5 _∷_
+
+data Pointwise {a b ℓ} {A : Set a} {B : Set b} (_∼_ : REL A B ℓ) :
+               ∀ {m n} (xs : Vec A m) (ys : Vec B n) → Set (a ⊔ b ⊔ ℓ)
+               where
+  []  : Pointwise _∼_ [] []
+  _∷_ : ∀ {m n x y} {xs : Vec A m} {ys : Vec B n}
+        (x∼y : x ∼ y) (xs∼ys : Pointwise _∼_ xs ys) →
+        Pointwise _∼_ (x ∷ xs) (y ∷ ys)
+
+length-equal : ∀ {a b m n ℓ} {A : Set a} {B : Set b} {_~_ : REL A B ℓ}
+               {xs : Vec A m} {ys : Vec B n} →
+               Pointwise _~_ xs ys → m ≡ n
+length-equal []          = P.refl
+length-equal (_ ∷ xs~ys) = P.cong suc (length-equal xs~ys)
+
+------------------------------------------------------------------------
+-- Operations
+
+module _ {a b ℓ} {A : Set a} {B : Set b} {_~_ : REL A B ℓ} where
+
+  head : ∀ {m n x y} {xs : Vec A m} {ys : Vec B n} →
+         Pointwise _~_ (x ∷ xs) (y ∷ ys) → x ~ y
+  head (x∼y ∷ xs∼ys) = x∼y
+
+  tail : ∀ {m n x y} {xs : Vec A m} {ys : Vec B n} →
+         Pointwise _~_ (x ∷ xs) (y ∷ ys) → Pointwise _~_ xs ys
+  tail (x∼y ∷ xs∼ys) = xs∼ys
+
+  lookup : ∀ {n} {xs : Vec A n} {ys : Vec B n} → Pointwise _~_ xs ys →
+           ∀ i → (Vec.lookup i xs) ~ (Vec.lookup i ys)
+  lookup (x~y ∷ _)     zero    = x~y
+  lookup (_   ∷ xs~ys) (suc i) = lookup xs~ys i
+
+  map : ∀ {ℓ₂} {_≈_ : REL A B ℓ₂} →
+        _≈_ ⇒ _~_ → ∀ {m n} → Pointwise _≈_ ⇒ Pointwise _~_ {m} {n}
+  map ~₁⇒~₂ []             = []
+  map ~₁⇒~₂ (x∼y ∷ xs~ys) = ~₁⇒~₂ x∼y ∷ map ~₁⇒~₂ xs~ys
+
+------------------------------------------------------------------------
+-- Relational properties
+
+refl : ∀ {a ℓ} {A : Set a} {_~_ : Rel A ℓ} →
+       ∀ {n} → Reflexive _~_ → Reflexive (Pointwise _~_ {n})
+refl ~-refl {[]}      = []
+refl ~-refl {x ∷ xs} = ~-refl ∷ refl ~-refl
+
+sym : ∀ {a b ℓ} {A : Set a} {B : Set b}
+      {P : REL A B ℓ} {Q : REL B A ℓ} {m n} →
+      Sym P Q → Sym (Pointwise P) (Pointwise Q {m} {n})
+sym sm []             = []
+sym sm (x∼y ∷ xs~ys) = sm x∼y ∷ sym sm xs~ys
+
+trans : ∀ {a b c ℓ} {A : Set a} {B : Set b} {C : Set c}
+        {P : REL A B ℓ} {Q : REL B C ℓ} {R : REL A C ℓ} {m n o} →
+        Trans P Q R →
+        Trans (Pointwise P {m}) (Pointwise Q {n} {o}) (Pointwise R)
+trans trns []             []             = []
+trans trns (x∼y ∷ xs~ys) (y∼z ∷ ys~zs) =
+  trns x∼y y∼z ∷ trans trns xs~ys ys~zs
+
+decidable : ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} →
+            Decidable _∼_ → ∀ {m n} → Decidable (Pointwise _∼_ {m} {n})
+decidable dec []       []       = yes []
+decidable dec []       (y ∷ ys) = no λ()
+decidable dec (x ∷ xs) []       = no λ()
+decidable dec (x ∷ xs) (y ∷ ys) with dec x y
+... | no ¬x∼y = no (¬x∼y ∘ head)
+... | yes x∼y with decidable dec xs ys
+...   | no ¬xs∼ys = no (¬xs∼ys ∘ tail)
+...   | yes xs∼ys = yes (x∼y ∷ xs∼ys)
+
+isEquivalence : ∀ {a ℓ} {A : Set a} {_~_ : Rel A ℓ} →
+                IsEquivalence _~_ → ∀ n →
+                IsEquivalence (Pointwise _~_ {n})
+isEquivalence equiv n = record
+  { refl  = refl  (IsEquivalence.refl  equiv)
+  ; sym   = sym   (IsEquivalence.sym   equiv)
+  ; trans = trans (IsEquivalence.trans equiv)
+  }
+
+isDecEquivalence : ∀ {a ℓ} {A : Set a} {_~_ : Rel A ℓ} →
+                   IsDecEquivalence _~_ → ∀ n →
+                   IsDecEquivalence (Pointwise _~_ {n})
+isDecEquivalence decEquiv n = record
+  { isEquivalence = isEquivalence (IsDecEquivalence.isEquivalence decEquiv) n
+  ; _≟_           = decidable (IsDecEquivalence._≟_ decEquiv)
+  }
+
+setoid : ∀ {a ℓ} → Setoid a ℓ → ℕ → Setoid a (a ⊔ ℓ)
+setoid S n = record
+   { isEquivalence = isEquivalence (Setoid.isEquivalence S) n
+   }
+
+decSetoid : ∀ {a ℓ} → DecSetoid a ℓ → ℕ → DecSetoid a (a ⊔ ℓ)
+decSetoid S n = record
+   { isDecEquivalence = isDecEquivalence (DecSetoid.isDecEquivalence S) n
+   }
+
+------------------------------------------------------------------------
+-- map
+
+module _ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} where
+
+  map⁺ : ∀ {ℓ₁ ℓ₂} {_~₁_ : REL A B ℓ₁} {_~₂_ : REL C D ℓ₂}
+         {f : A → C} {g : B → D} →
+         (∀ {x y} → x ~₁ y → f x ~₂ g y) →
+         ∀ {m n xs ys} → Pointwise _~₁_ {m} {n} xs ys →
+         Pointwise _~₂_ (Vec.map f xs) (Vec.map g ys)
+  map⁺ ~₁⇒~₂ []             = []
+  map⁺ ~₁⇒~₂ (x∼y ∷ xs~ys) = ~₁⇒~₂ x∼y ∷ map⁺ ~₁⇒~₂ xs~ys
+
+------------------------------------------------------------------------
+-- _++_
+
+module _ {a b ℓ} {A : Set a} {B : Set b} {_~_ : REL A B ℓ} where
+
+  ++⁺ : ∀ {m n p q}
+        {ws : Vec A m} {xs : Vec B p} {ys : Vec A n} {zs : Vec B q} →
+        Pointwise _~_ ws xs → Pointwise _~_ ys zs →
+        Pointwise _~_ (ws ++ ys) (xs ++ zs)
+  ++⁺ []            ys~zs = ys~zs
+  ++⁺ (w~x ∷ ws~xs) ys~zs = w~x ∷ (++⁺ ws~xs ys~zs)
+
+  ++ˡ⁻ : ∀ {m n}
+         (ws : Vec A m) (xs : Vec B m) {ys : Vec A n} {zs : Vec B n} →
+         Pointwise _~_ (ws ++ ys) (xs ++ zs) → Pointwise _~_ ws xs
+  ++ˡ⁻ []       []        _                    = []
+  ++ˡ⁻ (w ∷ ws) (x ∷ xs) (w~x ∷ ps) = w~x ∷ ++ˡ⁻ ws xs ps
+
+  ++ʳ⁻ : ∀ {m n}
+         (ws : Vec A m) (xs : Vec B m) {ys : Vec A n} {zs : Vec B n} →
+         Pointwise _~_ (ws ++ ys) (xs ++ zs) → Pointwise _~_ ys zs
+  ++ʳ⁻ [] [] ys~zs = ys~zs
+  ++ʳ⁻ (w ∷ ws) (x ∷ xs) (_ ∷ ps) = ++ʳ⁻ ws xs ps
+
+  ++⁻ : ∀ {m n}
+        (ws : Vec A m) (xs : Vec B m) {ys : Vec A n} {zs : Vec B n} →
+        Pointwise _~_ (ws ++ ys) (xs ++ zs) →
+        Pointwise _~_ ws xs × Pointwise _~_ ys zs
+  ++⁻ ws xs ps = ++ˡ⁻ ws xs ps , ++ʳ⁻ ws xs ps
+
+------------------------------------------------------------------------
+-- concat
+
+module _ {a b ℓ} {A : Set a} {B : Set b} {_~_ : REL A B ℓ} where
+
+  concat⁺ : ∀ {m n p q}
+            {xss : Vec (Vec A m) n} {yss : Vec (Vec B p) q} →
+            Pointwise (Pointwise _~_) xss yss →
+            Pointwise _~_ (concat xss) (concat yss)
+  concat⁺ []           = []
+  concat⁺ (xs~ys ∷ ps) = ++⁺ xs~ys (concat⁺ ps)
+
+  concat⁻ : ∀ {m n} (xss : Vec (Vec A m) n) (yss : Vec (Vec B m) n) →
+            Pointwise _~_ (concat xss) (concat yss) →
+            Pointwise (Pointwise _~_) xss yss
+  concat⁻ []         []         [] = []
+  concat⁻ (xs ∷ xss) (ys ∷ yss) ps =
+    ++ˡ⁻ xs ys ps ∷ concat⁻ xss yss (++ʳ⁻ xs ys ps)
+
+------------------------------------------------------------------------
+-- tabulate
+
+module _ {a b ℓ} {A : Set a} {B : Set b} {_~_ : REL A B ℓ} where
+
+  tabulate⁺ : ∀ {n} {f : Fin n → A} {g : Fin n → B} →
+              (∀ i → f i ~ g i) →
+              Pointwise _~_ (tabulate f) (tabulate g)
+  tabulate⁺ {zero}  f~g = []
+  tabulate⁺ {suc n} f~g = f~g zero ∷ tabulate⁺ (f~g ∘ suc)
+
+  tabulate⁻ : ∀ {n} {f : Fin n → A} {g : Fin n → B} →
+              Pointwise _~_ (tabulate f) (tabulate g) →
+              (∀ i → f i ~ g i)
+  tabulate⁻ (f₀~g₀ ∷ _)   zero    = f₀~g₀
+  tabulate⁻ (_     ∷ f~g) (suc i) = tabulate⁻ f~g i
+
+------------------------------------------------------------------------
+-- Degenerate pointwise relations
+
+module _ {a b ℓ} {A : Set a} {B : Set b} {P : A → Set ℓ} where
+
+  Pointwiseˡ⇒All : ∀ {m n} {xs : Vec A m} {ys : Vec B n} →
+                   Pointwise (λ x y → P x) xs ys → All P xs
+  Pointwiseˡ⇒All []       = []
+  Pointwiseˡ⇒All (p ∷ ps) = p ∷ Pointwiseˡ⇒All ps
+
+  Pointwiseʳ⇒All : ∀ {n} {xs : Vec B n} {ys : Vec A n} →
+                   Pointwise (λ x y → P y) xs ys → All P ys
+  Pointwiseʳ⇒All []       = []
+  Pointwiseʳ⇒All (p ∷ ps) = p ∷ Pointwiseʳ⇒All ps
+
+  All⇒Pointwiseˡ : ∀ {n} {xs : Vec A n} {ys : Vec B n} →
+                   All P xs → Pointwise (λ x y → P x) xs ys
+  All⇒Pointwiseˡ {ys = []}    []       = []
+  All⇒Pointwiseˡ {ys = _ ∷ _} (p ∷ ps) = p ∷ All⇒Pointwiseˡ ps
+
+  All⇒Pointwiseʳ : ∀ {n} {xs : Vec B n} {ys : Vec A n} →
+                   All P ys → Pointwise (λ x y → P y) xs ys
+  All⇒Pointwiseʳ {xs = []}    []       = []
+  All⇒Pointwiseʳ {xs = _ ∷ _} (p ∷ ps) = p ∷ All⇒Pointwiseʳ ps
+
+------------------------------------------------------------------------
+-- Pointwise _≡_ is equivalent to _≡_
+
+module _ {a} {A : Set a} where
+
+  Pointwise-≡⇒≡ : ∀ {n} {xs ys : Vec A n} →
+                  Pointwise _≡_ xs ys → xs ≡ ys
+  Pointwise-≡⇒≡ []               = P.refl
+  Pointwise-≡⇒≡ (P.refl ∷ xs~ys) = P.cong (_ ∷_) (Pointwise-≡⇒≡ xs~ys)
+
+  ≡⇒Pointwise-≡ : ∀ {n} {xs ys : Vec A n} →
+                  xs ≡ ys → Pointwise _≡_ xs ys
+  ≡⇒Pointwise-≡ P.refl = refl P.refl
+
+  Pointwise-≡↔≡ : ∀ {n} {xs ys : Vec A n} →
+                  Pointwise _≡_ xs ys ⇔ xs ≡ ys
+  Pointwise-≡↔≡ = equivalence Pointwise-≡⇒≡ ≡⇒Pointwise-≡
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 0.15
+
+Pointwise-≡ = Pointwise-≡↔≡
+{-# WARNING_ON_USAGE Pointwise-≡
+"Warning: Pointwise-≡ was deprecated in v0.15.
+Please use Pointwise-≡↔≡ instead."
+#-}