diff --git a/CHANGELOG.md b/CHANGELOG.md
index a1f857982a..e3ee4439dd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -235,6 +235,23 @@ Additions to existing modules
   ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b
   ```
 
+* In `Data.Fin.Base`:
+  ```agda
+  _≰_ : ∀ {n} → Rel (Fin n) 0ℓ
+  _≮_ : ∀ {n} → Rel (Fin n) 0ℓ
+  ```
+
+* In `Data.Fin.Permutation`:
+  ```agda
+  cast-id : .(m ≡ n) → Permutation m n
+  swap : Permutation m n → Permutation (suc (suc m)) (suc (suc n))
+  ```
+
+* In `Data.Fin.Properties`:
+  ```agda
+  cast-involutive : .(eq₁ : m ≡ n) .(eq₂ : n ≡ m) → ∀ k → cast eq₁ (cast eq₂ k) ≡ k
+  ```
+
 * In `Data.Fin.Subset`:
   ```agda
   _⊇_ : Subset n → Subset n → Set
@@ -266,14 +283,30 @@ Additions to existing modules
   map-downFrom : ∀ (f : ℕ → A) n → map f (downFrom n) ≡ applyDownFrom f n
   ```
 
+* In `Data.List.Relation.Binary.Permutation.Homogeneous`:
+  ```agda
+  toFin : Permutation R xs ys → Fin.Permutation (length xs) (length ys)
+  ```
+
 * In `Data.List.Relation.Binary.Permutation.Propositional`:
   ```agda
   ↭⇒↭ₛ′ : IsEquivalence _≈_ → _↭_ ⇒ _↭ₛ′_
   ```
 
+* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
+  ```agda
+  xs↭ys⇒|xs|≡|ys| : xs ↭ ys → length xs ≡ length ys
+  toFin-lookup : ∀ i → lookup xs i ≈ lookup ys (Inverse.to (toFin xs↭ys) i)
+  ```
+
 * In `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
   ```agda
   filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
+        ```
+
+* In `Data.List.Relation.Binary.Pointwise.Properties`:
+  ```agda
+  lookup-cast : Pointwise R xs ys → .(∣xs∣≡∣ys∣ : length xs ≡ length ys) → ∀ i → R (lookup xs i) (lookup ys (cast ∣xs∣≡∣ys∣ i))
   ```
 
 * In `Data.Product.Function.Dependent.Propositional`:
diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index 8d977d17b9..6d1f85e240 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -19,7 +19,7 @@ open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
 open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
-open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 
 private
   variable
@@ -271,7 +271,7 @@ pinch {suc n} (suc i) (suc j) = suc (pinch i j)
 ------------------------------------------------------------------------
 -- Order relations
 
-infix 4 _≤_ _≥_ _<_ _>_
+infix 4 _≤_ _≥_ _<_ _>_ _≰_ _≮_
 
 _≤_ : IRel Fin 0ℓ
 i ≤ j = toℕ i ℕ.≤ toℕ j
@@ -285,6 +285,11 @@ i < j = toℕ i ℕ.< toℕ j
 _>_ : IRel Fin 0ℓ
 i > j = toℕ i ℕ.> toℕ j
 
+_≰_ : ∀ {n} → Rel (Fin n) 0ℓ
+i ≰ j = ¬ (i ≤ j)
+
+_≮_ : ∀ {n} → Rel (Fin n) 0ℓ
+i ≮ j = ¬ (i < j)
 
 ------------------------------------------------------------------------
 -- An ordering view.
diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 794b93f76b..fa7374a82e 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -9,10 +9,10 @@
 module Data.Fin.Permutation where
 
 open import Data.Bool.Base using (true; false)
-open import Data.Fin.Base using (Fin; suc; opposite; punchIn; punchOut)
-open import Data.Fin.Patterns using (0F)
+open import Data.Fin.Base using (Fin; suc; cast; opposite; punchIn; punchOut)
+open import Data.Fin.Patterns using (0F; 1F)
 open import Data.Fin.Properties using (punchInᵢ≢i; punchOut-punchIn;
-  punchOut-cong; punchOut-cong′; punchIn-punchOut; _≟_; ¬Fin0)
+  punchOut-cong; punchOut-cong′; punchIn-punchOut; _≟_; ¬Fin0; cast-involutive)
 import Data.Fin.Permutation.Components as PC
 open import Data.Nat.Base using (ℕ; suc; zero)
 open import Data.Product.Base using (_,_; proj₂)
@@ -22,7 +22,7 @@ open import Function.Construct.Identity using (↔-id)
 open import Function.Construct.Symmetry using (↔-sym)
 open import Function.Definitions using (StrictlyInverseˡ; StrictlyInverseʳ)
 open import Function.Properties.Inverse using (↔⇒↣)
-open import Function.Base using (_∘_)
+open import Function.Base using (_∘_; _∘′_)
 open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary using (does; ¬_; yes; no)
@@ -57,11 +57,15 @@ Permutation′ n = Permutation n n
 ------------------------------------------------------------------------
 -- Helper functions
 
-permutation : ∀ (f : Fin m → Fin n) (g : Fin n → Fin m) →
-              StrictlyInverseˡ _≡_ f g → StrictlyInverseʳ _≡_ f g → Permutation m n
+permutation : ∀ (f : Fin m → Fin n)
+              (g : Fin n → Fin m) →
+              StrictlyInverseˡ _≡_ f g →
+              StrictlyInverseʳ _≡_ f g →
+              Permutation m n
 permutation = mk↔ₛ′
 
 infixl 5 _⟨$⟩ʳ_ _⟨$⟩ˡ_
+
 _⟨$⟩ʳ_ : Permutation m n → Fin m → Fin n
 _⟨$⟩ʳ_ = Inverse.to
 
@@ -75,44 +79,61 @@ inverseʳ : ∀ (π : Permutation m n) {i} → π ⟨$⟩ʳ (π ⟨$⟩ˡ i) ≡
 inverseʳ π = Inverse.inverseˡ π refl
 
 ------------------------------------------------------------------------
--- Equality
+-- Equality over permutations
 
 infix 6 _≈_
+
 _≈_ : Rel (Permutation m n) 0ℓ
 π ≈ ρ = ∀ i → π ⟨$⟩ʳ i ≡ ρ ⟨$⟩ʳ i
 
 ------------------------------------------------------------------------
--- Example permutations
+-- Permutation properties
 
--- Identity
-
-id : Permutation′ n
+id : Permutation n n
 id = ↔-id _
 
--- Transpose two indices
-
-transpose : Fin n → Fin n → Permutation′ n
-transpose i j = permutation (PC.transpose i j) (PC.transpose j i) (λ _ → PC.transpose-inverse _ _) (λ _ → PC.transpose-inverse _ _)
+flip : Permutation m n → Permutation n m
+flip = ↔-sym
 
--- Reverse the order of indices
+infixr 9 _∘ₚ_
 
-reverse : Permutation′ n
-reverse = permutation opposite opposite PC.reverse-involutive PC.reverse-involutive
+_∘ₚ_ : Permutation m n → Permutation n o → Permutation m o
+π₁ ∘ₚ π₂ = π₂ ↔-∘ π₁
 
 ------------------------------------------------------------------------
--- Operations
+-- Non-trivial identity
 
--- Composition
+cast-id : .(m ≡ n) → Permutation m n
+cast-id m≡n = permutation
+  (cast m≡n)
+  (cast (sym m≡n))
+  (cast-involutive m≡n (sym m≡n))
+  (cast-involutive (sym m≡n) m≡n)
 
-infixr 9 _∘ₚ_
-_∘ₚ_ : Permutation m n → Permutation n o → Permutation m o
-π₁ ∘ₚ π₂ = π₂ ↔-∘ π₁
+------------------------------------------------------------------------
+-- Transposition
 
--- Flip
+-- Transposes two elements in the permutation, keeping the remainder
+-- of the permutation the same
+transpose : Fin n → Fin n → Permutation n n
+transpose i j = permutation
+  (PC.transpose i j)
+  (PC.transpose j i)
+  (λ _ → PC.transpose-inverse _ _)
+  (λ _ → PC.transpose-inverse _ _)
 
-flip : Permutation m n → Permutation n m
-flip = ↔-sym
+------------------------------------------------------------------------
+-- Reverse
 
+-- Reverses a permutation
+reverse : Permutation n n
+reverse = permutation
+  opposite
+  opposite
+  PC.reverse-involutive
+  PC.reverse-involutive
+
+------------------------------------------------------------------------
 -- Element removal
 --
 -- `remove k [0 ↦ i₀, …, k ↦ iₖ, …, n ↦ iₙ]` yields
@@ -159,7 +180,10 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′
     punchOut {i = πʳ i} {punchIn (πʳ i) j}                         _  ≡⟨ punchOut-punchIn (πʳ i) ⟩
     j                                                                 ∎
 
--- lift: takes a permutation m → n and creates a permutation (suc m) → (suc n)
+------------------------------------------------------------------------
+-- Lifting
+
+-- Takes a permutation m → n and creates a permutation (suc m) → (suc n)
 -- by mapping 0 to 0 and applying the input permutation to everything else
 lift₀ : Permutation m n → Permutation (suc m) (suc n)
 lift₀ {m} {n} π = permutation to from inverseˡ′ inverseʳ′
@@ -180,6 +204,9 @@ lift₀ {m} {n} π = permutation to from inverseˡ′ inverseʳ′
   inverseˡ′ 0F      = refl
   inverseˡ′ (suc j) = cong suc (inverseʳ π)
 
+------------------------------------------------------------------------
+-- Insertion
+
 -- insert i j π is the permutation that maps i to j and otherwise looks like π
 -- it's roughly an inverse of remove
 insert : ∀ {m n} → Fin (suc m) → Fin (suc n) → Permutation m n → Permutation (suc m) (suc n)
@@ -221,6 +248,35 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
     punchIn j (punchOut j≢k)                                               ≡⟨ punchIn-punchOut j≢k ⟩
     k                                                                      ∎
 
+------------------------------------------------------------------------
+-- Swapping
+
+-- Takes a permutation m → n and creates a permutation
+-- suc (suc m) → suc (suc n) by mapping 0 to 1 and 1 to 0 and
+-- then applying the input permutation to everything else
+swap : Permutation m n → Permutation (suc (suc m)) (suc (suc n))
+swap {m} {n} π = permutation to from inverseˡ′ inverseʳ′
+  where
+  to : Fin (suc (suc m)) → Fin (suc (suc n))
+  to 0F      = 1F
+  to 1F      = 0F
+  to (suc (suc i)) = suc (suc (π ⟨$⟩ʳ i))
+
+  from : Fin (suc (suc n)) → Fin (suc (suc m))
+  from 0F            = 1F
+  from 1F            = 0F
+  from (suc (suc i)) = suc (suc (π ⟨$⟩ˡ i))
+
+  inverseʳ′ : StrictlyInverseʳ _≡_ to from
+  inverseʳ′ 0F            = refl
+  inverseʳ′ 1F            = refl
+  inverseʳ′ (suc (suc j)) = cong (suc ∘′ suc) (inverseˡ π)
+
+  inverseˡ′ : StrictlyInverseˡ _≡_ to from
+  inverseˡ′ 0F            = refl
+  inverseˡ′ 1F            = refl
+  inverseˡ′ (suc (suc j)) = cong (suc ∘′ suc) (inverseʳ π)
+
 ------------------------------------------------------------------------
 -- Other properties
 
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index e1f2d25d24..4962ed962b 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -279,6 +279,10 @@ cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ zero = refl
 cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (suc k) =
   cong suc (cast-trans (ℕ.suc-injective eq₁) (ℕ.suc-injective eq₂) k)
 
+cast-involutive : .(eq₁ : m ≡ n) .(eq₂ : n ≡ m) →
+                  ∀ k → cast eq₁ (cast eq₂ k) ≡ k
+cast-involutive eq₁ eq₂ k = trans (cast-trans eq₂ eq₁ k) (cast-is-id refl k)
+
 ------------------------------------------------------------------------
 -- Properties of _≤_
 ------------------------------------------------------------------------
diff --git a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
index 686c569423..d227a46da5 100644
--- a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
@@ -8,12 +8,15 @@
 
 module Data.List.Relation.Binary.Permutation.Homogeneous where
 
-open import Data.List.Base using (List; _∷_)
+open import Data.List.Base using (List; _∷_; length)
 open import Data.List.Relation.Binary.Pointwise.Base as Pointwise
   using (Pointwise)
 import Data.List.Relation.Binary.Pointwise.Properties as Pointwise
 open import Data.Nat.Base using (ℕ; suc; _+_)
+open import Data.Fin.Base using (Fin; zero; suc; cast)
+import Data.Fin.Permutation as Fin
 open import Level using (Level; _⊔_)
+open import Function.Base using (_∘_)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Structures using (IsEquivalence)
@@ -23,6 +26,7 @@ private
   variable
     a r s : Level
     A : Set a
+    R S : Rel A r
 
 data Permutation {A : Set a} (R : Rel A r) : Rel (List A) (a ⊔ r) where
   refl  : ∀ {xs ys} → Pointwise R xs ys → Permutation R xs ys
@@ -33,37 +37,39 @@ data Permutation {A : Set a} (R : Rel A r) : Rel (List A) (a ⊔ r) where
 ------------------------------------------------------------------------
 -- The Permutation relation is an equivalence
 
-module _ {R : Rel A r}  where
+sym : Symmetric R → Symmetric (Permutation R)
+sym R-sym (refl xs∼ys)           = refl (Pointwise.symmetric R-sym xs∼ys)
+sym R-sym (prep x∼x′ xs↭ys)      = prep (R-sym x∼x′) (sym R-sym xs↭ys)
+sym R-sym (swap x∼x′ y∼y′ xs↭ys) = swap (R-sym y∼y′) (R-sym x∼x′) (sym R-sym xs↭ys)
+sym R-sym (trans xs↭ys ys↭zs)    = trans (sym R-sym ys↭zs) (sym R-sym xs↭ys)
 
-  sym : Symmetric R → Symmetric (Permutation R)
-  sym R-sym (refl xs∼ys)           = refl (Pointwise.symmetric R-sym xs∼ys)
-  sym R-sym (prep x∼x′ xs↭ys)      = prep (R-sym x∼x′) (sym R-sym xs↭ys)
-  sym R-sym (swap x∼x′ y∼y′ xs↭ys) = swap (R-sym y∼y′) (R-sym x∼x′) (sym R-sym xs↭ys)
-  sym R-sym (trans xs↭ys ys↭zs)    = trans (sym R-sym ys↭zs) (sym R-sym xs↭ys)
+isEquivalence : Reflexive R → Symmetric R → IsEquivalence (Permutation R)
+isEquivalence R-refl R-sym = record
+  { refl  = refl (Pointwise.refl R-refl)
+  ; sym   = sym R-sym
+  ; trans = trans
+  }
 
-  isEquivalence : Reflexive R → Symmetric R → IsEquivalence (Permutation R)
-  isEquivalence R-refl R-sym = record
-    { refl  = refl (Pointwise.refl R-refl)
-    ; sym   = sym R-sym
-    ; trans = trans
-    }
+setoid : Reflexive R → Symmetric R → Setoid _ _
+setoid {R = R} R-refl R-sym = record
+  { isEquivalence = isEquivalence {R = R} R-refl R-sym
+  }
 
-  setoid : Reflexive R → Symmetric R → Setoid _ _
-  setoid R-refl R-sym = record
-    { isEquivalence = isEquivalence R-refl R-sym
-    }
-
-map : ∀ {R : Rel A r} {S : Rel A s} →
-      (R ⇒ S) → (Permutation R ⇒ Permutation S)
+map : (R ⇒ S) → (Permutation R ⇒ Permutation S)
 map R⇒S (refl xs∼ys)         = refl (Pointwise.map R⇒S xs∼ys)
 map R⇒S (prep e xs∼ys)       = prep (R⇒S e) (map R⇒S xs∼ys)
 map R⇒S (swap e₁ e₂ xs∼ys)   = swap (R⇒S e₁) (R⇒S e₂) (map R⇒S xs∼ys)
 map R⇒S (trans xs∼ys ys∼zs)  = trans (map R⇒S xs∼ys) (map R⇒S ys∼zs)
 
 -- Measures the number of constructors, can be useful for termination proofs
-
-steps : ∀ {R : Rel A r} {xs ys} → Permutation R xs ys → ℕ
+steps : ∀ {xs ys} → Permutation R xs ys → ℕ
 steps (refl _)            = 1
 steps (prep _ xs↭ys)      = suc (steps xs↭ys)
 steps (swap _ _ xs↭ys)    = suc (steps xs↭ys)
 steps (trans xs↭ys ys↭zs) = steps xs↭ys + steps ys↭zs
+
+toFin : ∀ {xs ys} → Permutation R xs ys → Fin.Permutation (length xs) (length ys)
+toFin (refl ≋)          = Fin.cast-id (Pointwise.Pointwise-length ≋)
+toFin (prep e xs↭ys)   = Fin.lift₀ (toFin xs↭ys)
+toFin (swap e f xs↭ys) = Fin.swap (toFin xs↭ys)
+toFin (trans ↭₁ ↭₂)   = toFin ↭₁ Fin.∘ₚ toFin ↭₂
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
index 5c81eb6999..9b120ab006 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
@@ -31,7 +31,7 @@ open ≋ S using (_≋_; _∷_; ≋-refl; ≋-sym; ≋-trans)
 -- Definition, based on `Homogeneous`
 
 open Homogeneous public
-  using (refl; prep; swap; trans)
+  using (refl; prep; swap; trans; toFin)
 
 infix 3 _↭_
 
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index d82178dd8b..4d45fba18d 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -17,6 +17,7 @@ module Data.List.Relation.Binary.Permutation.Setoid.Properties
 
 open import Algebra
 open import Data.Bool.Base using (true; false)
+open import Data.Fin using (zero; suc)
 open import Data.List.Base as List hiding (head; tail)
 open import Data.List.Relation.Binary.Pointwise as Pointwise
   using (Pointwise; head; tail)
@@ -34,6 +35,7 @@ open import Data.Nat.Induction
 open import Data.Nat.Properties
 open import Data.Product.Base using (_,_; _×_; ∃; ∃₂; proj₁; proj₂)
 open import Function.Base using (_∘_; _⟨_⟩_; flip)
+open import Function.Bundles using (Inverse)
 open import Level using (Level; _⊔_)
 open import Relation.Unary using (Pred; Decidable)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
@@ -100,6 +102,12 @@ AllPairs-resp-↭ sym resp (trans p₁ p₂)    pxs             =
 Unique-resp-↭ : Unique Respects _↭_
 Unique-resp-↭ = AllPairs-resp-↭ (_∘ ≈-sym) ≉-resp₂
 
+xs↭ys⇒|xs|≡|ys| : ∀ {xs ys} → xs ↭ ys → length xs ≡ length ys
+xs↭ys⇒|xs|≡|ys| (refl eq)            = Pointwise.Pointwise-length eq
+xs↭ys⇒|xs|≡|ys| (prep eq xs↭ys)      = ≡.cong suc (xs↭ys⇒|xs|≡|ys| xs↭ys)
+xs↭ys⇒|xs|≡|ys| (swap eq₁ eq₂ xs↭ys) = ≡.cong (λ x → suc (suc x)) (xs↭ys⇒|xs|≡|ys| xs↭ys)
+xs↭ys⇒|xs|≡|ys| (trans xs↭ys xs↭ys₁) = ≡.trans (xs↭ys⇒|xs|≡|ys| xs↭ys) (xs↭ys⇒|xs|≡|ys| xs↭ys₁)
+
 ------------------------------------------------------------------------
 -- Core properties depending on the representation of _↭_
 ------------------------------------------------------------------------
@@ -429,6 +437,15 @@ module _{_∙_ : Op₂ A} {ε : A}
     where open ≈-Reasoning CM.setoid
   foldr-commMonoid (trans xs↭ys ys↭zs) = CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs)
 
+toFin-lookup : ∀ (xs↭ys : xs ↭ ys) →
+               ∀ i → lookup xs i ≈ lookup ys (Inverse.to (toFin xs↭ys) i)
+toFin-lookup (refl xs≋ys)         i            = Pointwise.lookup-cast xs≋ys _ i
+toFin-lookup (prep eq xs↭ys)     zero          = eq
+toFin-lookup (prep _  xs↭ys)     (suc i)       = toFin-lookup xs↭ys i
+toFin-lookup (swap eq _ xs↭ys)   zero          = eq
+toFin-lookup (swap _ eq xs↭ys)   (suc zero)    = eq
+toFin-lookup (swap _ _  xs↭ys)   (suc (suc i)) = toFin-lookup xs↭ys i
+toFin-lookup (trans xs↭ys ys↭zs) i            = ≈-trans (toFin-lookup xs↭ys i) (toFin-lookup ys↭zs _)
 
 ------------------------------------------------------------------------
 -- TOWARDS DEPRECATION
diff --git a/src/Data/List/Relation/Binary/Pointwise.agda b/src/Data/List/Relation/Binary/Pointwise.agda
index 91ed2eb1c5..c2139dadfc 100644
--- a/src/Data/List/Relation/Binary/Pointwise.agda
+++ b/src/Data/List/Relation/Binary/Pointwise.agda
@@ -130,13 +130,6 @@ AllPairs-resp-Pointwise resp@(respₗ , respᵣ) (x∼y ∷ xs) (px ∷ pxs) =
 
 ------------------------------------------------------------------------
 -- Relationship to functions over lists
-------------------------------------------------------------------------
--- length
-
-Pointwise-length : Pointwise R xs ys → length xs ≡ length ys
-Pointwise-length []            = ≡.refl
-Pointwise-length (x∼y ∷ xs∼ys) = ≡.cong ℕ.suc (Pointwise-length xs∼ys)
-
 ------------------------------------------------------------------------
 -- tabulate
 
diff --git a/src/Data/List/Relation/Binary/Pointwise/Properties.agda b/src/Data/List/Relation/Binary/Pointwise/Properties.agda
index 1761dd3cda..53186c5c3c 100644
--- a/src/Data/List/Relation/Binary/Pointwise/Properties.agda
+++ b/src/Data/List/Relation/Binary/Pointwise/Properties.agda
@@ -8,12 +8,14 @@
 
 module Data.List.Relation.Binary.Pointwise.Properties where
 
+open import Data.Nat.Base using (ℕ)
+open import Data.Fin.Base using (zero; suc; cast)
 open import Data.Product.Base using (_,_; uncurry)
-open import Data.List.Base using (List; []; _∷_)
+open import Data.List.Base using (List; []; _∷_; length; lookup)
 open import Level
 open import Relation.Binary.Core using (REL; _⇒_)
 open import Relation.Binary.Definitions
-import Relation.Binary.PropositionalEquality.Core as ≡
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Nullary using (yes; no; _×-dec_)
 import Relation.Nullary.Decidable as Dec
 
@@ -75,3 +77,15 @@ irrelevant : Irrelevant R → Irrelevant (Pointwise R)
 irrelevant irr []       []         = ≡.refl
 irrelevant irr (r ∷ rs) (r₁ ∷ rs₁) =
   ≡.cong₂ _∷_ (irr r r₁) (irrelevant irr rs rs₁)
+
+Pointwise-length : ∀ {xs ys} → Pointwise R xs ys → length xs ≡ length ys
+Pointwise-length []            = ≡.refl
+Pointwise-length (x∼y ∷ xs∼ys) = ≡.cong ℕ.suc (Pointwise-length xs∼ys)
+
+lookup-cast : ∀ {xs ys} →
+              Pointwise R xs ys →
+              .(∣xs∣≡∣ys∣ : length xs ≡ length ys) →
+              ∀ i →
+              R (lookup xs i) (lookup ys (cast ∣xs∣≡∣ys∣ i))
+lookup-cast (Rxy ∷ Rxsys) eq zero = Rxy
+lookup-cast (Rxy ∷ Rxsys) eq (suc i) = lookup-cast Rxsys _ i
diff --git a/src/Data/List/Relation/Unary/Linked.agda b/src/Data/List/Relation/Unary/Linked.agda
index dc1b7fb87d..6717adebd0 100644
--- a/src/Data/List/Relation/Unary/Linked.agda
+++ b/src/Data/List/Relation/Unary/Linked.agda
@@ -11,6 +11,7 @@ module Data.List.Relation.Unary.Linked {a} {A : Set a} where
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.Product.Base as Prod using (_,_; _×_; uncurry; <_,_>)
+open import Data.Fin.Base using (zero; suc)
 open import Data.Maybe.Base using (just)
 open import Data.Maybe.Relation.Binary.Connected
   using (Connected; just; just-nothing)
@@ -26,6 +27,7 @@ open import Relation.Nullary.Decidable using (yes; no; map′; _×-dec_)
 private
   variable
     p q r ℓ : Level
+    R : Rel A ℓ
 
 ------------------------------------------------------------------------
 -- Definition
@@ -92,6 +94,14 @@ module _ {P : Rel A p} {Q : Rel A q} where
   unzip : Linked (P ∩ᵇ Q) ⊆ Linked P ∩ᵘ Linked Q
   unzip = unzipWith id
 
+lookup : ∀ {x xs} → Transitive R → Linked R xs →
+         Connected R (just x) (List.head xs) →
+         ∀ i → R x (List.lookup xs i)
+lookup trans [-]       (just Rvx) zero    = Rvx
+lookup trans (x ∷ xs↗) (just Rvx) zero    = Rvx
+lookup trans (x ∷ xs↗) (just Rvx) (suc i) =
+  lookup trans xs↗ (just (trans Rvx x)) i
+
 ------------------------------------------------------------------------
 -- Properties of predicates preserved by Linked
 
diff --git a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda
index c8c4210ed6..3e14bb7145 100644
--- a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda
+++ b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda
@@ -14,20 +14,35 @@ open import Data.List.Relation.Unary.AllPairs using (AllPairs)
 open import Data.List.Relation.Unary.Linked as Linked
   using (Linked; []; [-]; _∷_; _∷′_; head′; tail)
 import Data.List.Relation.Unary.Linked.Properties as Linked
+import Data.List.Relation.Binary.Equality.Setoid as Equality
 import Data.List.Relation.Binary.Sublist.Setoid as Sublist
 import Data.List.Relation.Binary.Sublist.Setoid.Properties as SublistProperties
-open import Data.List.Relation.Unary.Sorted.TotalOrder hiding (head)
-
+import Data.List.Relation.Binary.Permutation.Setoid as Permutation
+import Data.List.Relation.Binary.Permutation.Setoid.Properties as PermutationProperties
+import Data.List.Relation.Binary.Pointwise as Pointwise
+open import Data.List.Relation.Unary.Sorted.TotalOrder as Sorted hiding (head)
+
+open import Data.Fin.Base as Fin hiding (_<_; _≤_)
+import Data.Fin.Properties as Fin
+open import Data.Fin.Induction
 open import Data.Maybe.Base using (just; nothing)
 open import Data.Maybe.Relation.Binary.Connected using (Connected; just)
-open import Data.Nat.Base using (ℕ; zero; suc; _<_)
+open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s; zero; suc)
+import Data.Nat.Properties as ℕ
+open import Function.Base using (_∘_; const)
+open import Function.Definitions using (Injective)
+open import Function.Bundles using (_↣_; mk↣; Inverse)
+open import Level using (0ℓ)
 
 open import Level using (Level)
-open import Relation.Binary.Core using (_Preserves_⟶_)
+open import Relation.Binary.Core using (_Preserves_⟶_; Rel)
 open import Relation.Binary.Bundles using (TotalOrder; DecTotalOrder; Preorder)
 import Relation.Binary.Properties.TotalOrder as TotalOrderProperties
+import Relation.Binary.Reasoning.PartialOrder as PosetReasoning
 open import Relation.Unary using (Pred; Decidable)
+open import Relation.Nullary using (contradiction)
 open import Relation.Nullary.Decidable using (yes; no)
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
 private
   variable
@@ -80,7 +95,7 @@ module _ (O : TotalOrder a ℓ₁ ℓ₂) where
 module _ (O : TotalOrder a ℓ₁ ℓ₂) where
   open TotalOrder O
 
-  applyUpTo⁺₁ : ∀ f n → (∀ {i} → suc i < n → f i ≤ f (suc i)) →
+  applyUpTo⁺₁ : ∀ f n → (∀ {i} → suc i ℕ.< n → f i ≤ f (suc i)) →
                 Sorted O (applyUpTo f n)
   applyUpTo⁺₁ = Linked.applyUpTo⁺₁
 
@@ -94,7 +109,7 @@ module _ (O : TotalOrder a ℓ₁ ℓ₂) where
 module _ (O : TotalOrder a ℓ₁ ℓ₂) where
   open TotalOrder O
 
-  applyDownFrom⁺₁ : ∀ f n → (∀ {i} → suc i < n → f (suc i) ≤ f i) →
+  applyDownFrom⁺₁ : ∀ f n → (∀ {i} → suc i ℕ.< n → f (suc i) ≤ f i) →
                     Sorted O (applyDownFrom f n)
   applyDownFrom⁺₁ = Linked.applyDownFrom⁺₁
 
@@ -150,3 +165,115 @@ module _ (O : TotalOrder a ℓ₁ ℓ₂) {P : Pred _ p} (P? : Decidable P) wher
 
   filter⁺ : ∀ {xs} → Sorted O xs → Sorted O (filter P? xs)
   filter⁺ = Linked.filter⁺ P? trans
+
+------------------------------------------------------------------------
+-- lookup
+
+module _ (O : TotalOrder a ℓ₁ ℓ₂) where
+  open TotalOrder O
+
+  lookup-mono-≤ : ∀ {xs} → Sorted O xs →
+                  ∀ {i j} → i Fin.≤ j → lookup xs i ≤ lookup xs j
+  lookup-mono-≤ {x ∷ xs} xs↗ {zero}  {zero}  z≤n       = refl
+  lookup-mono-≤ {x ∷ xs} xs↗ {zero}  {suc j} z≤n       = Linked.lookup trans xs↗ (just refl) (suc j)
+  lookup-mono-≤ {x ∷ xs} xs↗ {suc i} {suc j} (s≤s i≤j) = lookup-mono-≤ (Sorted.tail O {y = x} xs↗) i≤j
+
+------------------------------------------------------------------------
+-- Relationship to binary relations
+------------------------------------------------------------------------
+
+module _ (O : TotalOrder a ℓ₁ ℓ₂) where
+  open TotalOrder O renaming (Carrier to A)
+  open Equality Eq.setoid
+  open module Perm = Permutation Eq.setoid hiding (refl; trans)
+  open PermutationProperties Eq.setoid
+  open PosetReasoning poset
+
+  -- Proof that any two sorted lists that are a permutation of each
+  -- other are pointwise equal
+  private
+    module _ {x y xs′ ys′} (xs↭ys : x ∷ xs′ ↭ y ∷ ys′) where
+      xs ys : List _
+      xs = x ∷ xs′
+      ys = y ∷ ys′
+
+      indices : ∀ {xs ys} → xs ↭ ys → Fin (length xs) → Fin (length ys)
+      indices xs↭ys = Inverse.to (Permutation.toFin xs↭ys)
+
+      indices-injective : ∀ {xs ys} (xs↭ys : xs ↭ ys) → Injective _≡_ _≡_ (indices xs↭ys)
+      indices-injective = {!Inverse.injective ? !}
+
+      lower : ∀ {m n} (i : Fin m) → .(toℕ i ℕ.< n) → Fin n
+      lower {suc _} {suc n} zero    leq = zero
+      lower {suc _} {suc n} (suc i) leq = suc (lower i (ℕ.≤-pred leq))
+
+      lower-injective : ∀ {m n} (i j : Fin m)
+                        (i<n : toℕ i ℕ.< n) (j<n : toℕ j ℕ.< n)  →
+                        lower i i<n ≡ lower j j<n → i ≡ j
+      lower-injective {suc _} {suc n} zero    zero    i<n       j<n       eq = P.refl
+      lower-injective {suc _} {suc n} (suc i) (suc j) (s≤s i<n) (s≤s j<n) eq =
+        P.cong suc (lower-injective i j i<n j<n (Fin.suc-injective eq))
+
+      π : Fin _ → Fin _
+      π = indices xs↭ys
+
+      π-contractingIn[_-_] : Fin (length xs) → Fin (length ys) → Set
+      π-contractingIn[ i - j ] = ∀ {k} → i Fin.< k → toℕ k ℕ.≤ toℕ j → π k Fin.< j
+
+      π-contractingIn-≡ : ∀ {i j} → toℕ i ≡ toℕ j → π-contractingIn[ i - j ]
+      π-contractingIn-≡ i≡j j<k k≤i = contradiction (ℕ.<-≤-trans j<k k≤i) (ℕ.<-irrefl i≡j)
+
+      π-contractingIn-pred : ∀ {i j} → π-contractingIn[ i - j ] →
+                             j Fin.≰ π i → zero {length xs} Fin.< i →
+                             π-contractingIn[ pred i - j ]
+      π-contractingIn-pred i@{suc _} {j} contr j≰πᵢ _ {k} i∸1≤k k≤j with i Fin.≟ k
+      ... | yes P.refl = ℕ.≰⇒> j≰πᵢ
+      ... | no  i≢k    = contr (ℕ.≤∧≢⇒< i≤k (i≢k ∘ Fin.toℕ-injective)) k≤j
+        where i≤k = P.subst (ℕ._≤ toℕ k) (Fin.toℕ-inject₁ i) i∸1≤k
+
+      π-contractingIn-injection : ∀ {j} → π-contractingIn[ zero - j ] →
+                                  j Fin.≰ π zero → Fin′ (suc j) ↣ Fin′ j
+      π-contractingIn-injection {j} π-contracting j≰π₀ = mk↣ f-injective
+        where
+        j<∣xs∣ : toℕ j ℕ.< length xs
+        j<∣xs∣ = P.subst (toℕ j ℕ.<_) (P.sym (xs↭ys⇒|xs|≡|ys| xs↭ys)) (Fin.toℕ<n j)
+
+        k≤j⇒πₖ<j : (k : Fin′ (suc j)) → π (Fin.inject≤ k j<∣xs∣) Fin.< j
+        k≤j⇒πₖ<j zero    = ℕ.≰⇒> j≰π₀
+        k≤j⇒πₖ<j (suc k) = π-contracting (s≤s z≤n) k≤j
+          where k≤j = P.subst (ℕ._≤ toℕ j) (P.sym (Fin.toℕ-inject≤ (suc k) j<∣xs∣)) (Fin.toℕ<n k)
+
+        f : Fin′ (suc j) → Fin′ j
+        f k = lower (π (Fin.inject≤ k j<∣xs∣)) (k≤j⇒πₖ<j k)
+
+        f-injective : ∀ {k l} → f k ≡ f l → k ≡ l
+        f-injective {k} {l} = Fin.inject≤-injective _ _ k l
+          ∘ indices-injective xs↭ys
+          ∘ lower-injective _ _ (k≤j⇒πₖ<j k) (k≤j⇒πₖ<j l)
+
+      ↗↭↗⇒≤ : Sorted O xs → Sorted O ys →
+              ∀ {i} → Acc Fin._<_ i →
+              ∀ {j} → π-contractingIn[ i - j ] →
+              ∀ {v} → lookup xs i ≤ v → lookup ys j ≤ v
+      ↗↭↗⇒≤ xs↗ ys↗ {i} (acc rec) {j} π-contr {v} xsᵢ≤v with j Fin.≤? π i | i Fin.≟ zero
+      ...   | yes j≤πᵢ | _          = begin
+        lookup ys j      ≤⟨  {!!} ⟩ --lookup-mono-≤ O ys↗ {i = π i} {j = j} j≤πᵢ ⟩
+        lookup ys (π i)  ≈˘⟨ indices-lookup xs↭ys i ⟩
+        lookup xs i      ≤⟨  xsᵢ≤v ⟩
+        v                ∎
+      ...   | no  j≰πᵢ | yes P.refl = contradiction (π-contractingIn-injection π-contr j≰πᵢ) {!!} --(Fin.pigeonhole′ ℕ.≤-refl)
+      ...   | no  j≰πᵢ | no  i≢0    = {!!}
+{-
+↗↭↗⇒≤ xs↗ ys↗ (rec (pred i) (ℕ.≤-reflexive ?)) -- (Fin.suc-pred i≢0)))
+        (π-contractingIn-pred π-contr j≰πᵢ ?) --(Fin.i≢0⇒i>0 i≢0))
+        (trans ? ?) --(lookup-mono-≤ O xs↗ (Fin.pred≤ i)) xsᵢ≤v)
+        -}
+{-
+  ↗↭↗⇒≋ : ∀ {xs ys} → Sorted O xs → Sorted O ys → xs ↭ ys → xs ≋ ys
+  ↗↭↗⇒≋ {[]}    {[]}    _   _   _     = []
+  ↗↭↗⇒≋ {[]}    {_ ∷ _} _   _   []↭ys = contradiction []↭ys ¬[]↭x∷xs
+  ↗↭↗⇒≋ {_ ∷ _} {[]}    _   _   xs↭[] = contradiction xs↭[] ¬x∷xs↭[]
+  ↗↭↗⇒≋ {_ ∷ _} {_ ∷ _} xs↗ ys↗ xs↭ys = lookup⁻ (xs↭ys⇒|xs|≡|ys| xs↭ys) (λ i≡j → antisym
+    (↗↭↗⇒≤ (↭-sym xs↭ys) ys↗ xs↗ (<-wellFounded _) (π-contractingIn-≡ (↭-sym xs↭ys) (P.sym i≡j)) refl)
+    (↗↭↗⇒≤        xs↭ys  xs↗ ys↗ (<-wellFounded _) (π-contractingIn-≡        xs↭ys         i≡j)  refl))
+-}