From def66050cf356af35547acc02b61433d212ef414 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Sat, 3 Nov 2018 14:08:49 +0100
Subject: [PATCH 01/12] [ re #517 ] First steps towards formalizing Prefix

---
 .../List/Relation/Prefix/Heterogeneous.agda   | 23 +++++++++
 .../Prefix/Heterogeneous/Properties.agda      | 47 +++++++++++++++++++
 2 files changed, 70 insertions(+)
 create mode 100644 src/Data/List/Relation/Prefix/Heterogeneous.agda
 create mode 100644 src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda

diff --git a/src/Data/List/Relation/Prefix/Heterogeneous.agda b/src/Data/List/Relation/Prefix/Heterogeneous.agda
new file mode 100644
index 0000000000..b4e4affe29
--- /dev/null
+++ b/src/Data/List/Relation/Prefix/Heterogeneous.agda
@@ -0,0 +1,23 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- An inductive definition of the heterogeneous prefix relation
+------------------------------------------------------------------------
+
+module Data.List.Relation.Prefix.Heterogeneous where
+
+open import Data.List.Base as List using (List; []; _∷_)
+open import Data.List.Relation.Pointwise using (Pointwise; []; _∷_)
+open import Relation.Binary using (REL; _⇒_)
+
+data Prefix {a b r} {A : Set a} {B : Set b} (R : REL A B r)
+          : REL (List A) (List B) r where
+  []  : ∀ {bs} → Prefix R [] bs
+  _∷_ : ∀ {a b as bs} → R a b → Prefix R as bs → Prefix R (a ∷ as) (b ∷ bs)
+
+module _ {a b r s} {A : Set a} {B : Set b} {R : REL A B r} {S : REL A B s} where
+
+  map : R ⇒ S → Prefix R ⇒ Prefix S
+  map f []       = []
+  map f (x ∷ xs) = f x ∷ map f xs
+
diff --git a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
new file mode 100644
index 0000000000..9542aabe29
--- /dev/null
+++ b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
@@ -0,0 +1,47 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of the heterogeneous prefix relation
+------------------------------------------------------------------------
+
+module Data.List.Relation.Prefix.Heterogeneous.Properties where
+
+open import Data.List.Base as List using (List; []; _∷_)
+open import Data.List.Relation.Pointwise using (Pointwise; []; _∷_)
+open import Data.List.Relation.Prefix.Heterogeneous
+open import Relation.Binary
+
+module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
+
+  refl : Pointwise R ⇒ Prefix R
+  refl []       = []
+  refl (x ∷ xs) = x ∷ refl xs
+
+  infixl 5 _++_
+  _++_ : ∀ {as bs cs ds} → Pointwise R as bs → Prefix R cs ds →
+         Prefix R (as List.++ cs) (bs List.++ ds)
+  []            ++ cs⊆ds = cs⊆ds
+  (a∼b ∷ as∼bs) ++ cs⊆ds = a∼b ∷ (as∼bs ++ cs⊆ds)
+
+module _ {a b c r s t} {A : Set a} {B : Set b} {C : Set c}
+         {R : REL A B r} {S : REL B C s} {T : REL A C t} where
+
+  trans : Trans R S T → Trans (Prefix R) (Prefix S) (Prefix T)
+  trans rs⇒t []            bs~cs         = []
+  trans rs⇒t (a∼b ∷ as∼bs) (b∼c ∷ bs∼cs) = rs⇒t a∼b b∼c ∷ trans rs⇒t as∼bs bs∼cs
+
+module _ {a b c d r} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
+         {R : REL C D r} where
+
+  map⁺ : ∀ {as bs} (f : A → C) (g : B → D) →
+         Prefix (λ a b → R (f a) (g b)) as bs →
+         Prefix R (List.map f as) (List.map g bs)
+  map⁺ f g []       = []
+  map⁺ f g (x ∷ xs) = x ∷ map⁺ f g xs
+
+  map⁻ : ∀ {as bs} (f : A → C) (g : B → D) →
+         Prefix R (List.map f as) (List.map g bs) →
+         Prefix (λ a b → R (f a) (g b)) as bs
+  map⁻ {[]}     {bs}     f g xs = []
+  map⁻ {a ∷ as} {[]}     f g ()
+  map⁻ {a ∷ as} {b ∷ bs} f g (x ∷ xs) = x ∷ map⁻ f g xs

From bfe1db8bd1447eafafd65b05f5d9fb8b59d781d5 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Sat, 3 Nov 2018 14:19:59 +0100
Subject: [PATCH 02/12] [ new ] prefix is decidable

---
 CHANGELOG.md                                    |  2 ++
 .../Prefix/Heterogeneous/Properties.agda        | 17 +++++++++++++++++
 2 files changed, 19 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2d5a8d83b4..e209170aa6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -48,6 +48,8 @@ Other major changes
 
 * Added new modules `Codata.M.Properties` and `Codata.M.Bisimilarity`
 
+* Added new modules `Data.List.Relation.Prefix.Heterogeneous(.Properties)`
+
 * Added new module `Data.Vec.Any.Properties`
 
 * Added new module `Relation.Binary.Properties.BoundedLattice`
diff --git a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
index 9542aabe29..63be08117e 100644
--- a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
@@ -9,10 +9,19 @@ module Data.List.Relation.Prefix.Heterogeneous.Properties where
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Pointwise using (Pointwise; []; _∷_)
 open import Data.List.Relation.Prefix.Heterogeneous
+open import Data.Product using (_×_; _,_; uncurry)
+open import Function
+
+open import Relation.Nullary using (yes; no)
+import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Product using (_×-dec_)
 open import Relation.Binary
 
 module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
 
+  uncons : ∀ {a b as bs} → Prefix R (a ∷ as) (b ∷ bs) → R a b × Prefix R as bs
+  uncons (x ∷ xs) = x , xs
+
   refl : Pointwise R ⇒ Prefix R
   refl []       = []
   refl (x ∷ xs) = x ∷ refl xs
@@ -45,3 +54,11 @@ module _ {a b c d r} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
   map⁻ {[]}     {bs}     f g xs = []
   map⁻ {a ∷ as} {[]}     f g ()
   map⁻ {a ∷ as} {b ∷ bs} f g (x ∷ xs) = x ∷ map⁻ f g xs
+
+module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
+
+  prefix? : Decidable R → Decidable (Prefix R)
+  prefix? R? []       bs       = yes []
+  prefix? R? (a ∷ as) []       = no (λ ())
+  prefix? R? (a ∷ as) (b ∷ bs) = Dec.map′ (uncurry _∷_) uncons
+                               $ R? a b ×-dec prefix? R? as bs

From 5fe594ba7eb5611de64bf0bde285763349e1b171 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Sat, 3 Nov 2018 17:39:53 +0100
Subject: [PATCH 03/12] [ refactor, new ] antisymmetry, cancellation of ++

---
 CHANGELOG.md                                  |  5 +++
 .../List/Relation/Prefix/Heterogeneous.agda   |  7 ++++
 .../Prefix/Heterogeneous/Properties.agda      | 42 ++++++++++++++-----
 src/Relation/Binary/Core.agda                 |  6 ++-
 4 files changed, 49 insertions(+), 11 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e209170aa6..46d6bc75ba 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -190,6 +190,11 @@ Other minor additions
   toAny   : x ∈ xs → P x → Any P xs
   ```
 
+* Added new definition to `Relation.Binary.Core`:
+  ```agda
+  Antisym R S E = ∀ {i j} → R i j → S j i → E i j
+  ```
+
 * Added new proofs to `Relation.Binary.Lattice`:
   ```agda
   Lattice.setoid        : Setoid c ℓ
diff --git a/src/Data/List/Relation/Prefix/Heterogeneous.agda b/src/Data/List/Relation/Prefix/Heterogeneous.agda
index b4e4affe29..3007914cab 100644
--- a/src/Data/List/Relation/Prefix/Heterogeneous.agda
+++ b/src/Data/List/Relation/Prefix/Heterogeneous.agda
@@ -8,6 +8,7 @@ module Data.List.Relation.Prefix.Heterogeneous where
 
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Pointwise using (Pointwise; []; _∷_)
+open import Data.Product using (_×_; _,_)
 open import Relation.Binary using (REL; _⇒_)
 
 data Prefix {a b r} {A : Set a} {B : Set b} (R : REL A B r)
@@ -15,6 +16,12 @@ data Prefix {a b r} {A : Set a} {B : Set b} (R : REL A B r)
   []  : ∀ {bs} → Prefix R [] bs
   _∷_ : ∀ {a b as bs} → R a b → Prefix R as bs → Prefix R (a ∷ as) (b ∷ bs)
 
+
+module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
+
+  uncons : ∀ {a b as bs} → Prefix R (a ∷ as) (b ∷ bs) → R a b × Prefix R as bs
+  uncons (x ∷ xs) = x , xs
+
 module _ {a b r s} {A : Set a} {B : Set b} {R : REL A B r} {S : REL A B s} where
 
   map : R ⇒ S → Prefix R ⇒ Prefix S
diff --git a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
index 63be08117e..0131adf471 100644
--- a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
@@ -9,7 +9,7 @@ module Data.List.Relation.Prefix.Heterogeneous.Properties where
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Pointwise using (Pointwise; []; _∷_)
 open import Data.List.Relation.Prefix.Heterogeneous
-open import Data.Product using (_×_; _,_; uncurry)
+open import Data.Product using (uncurry)
 open import Function
 
 open import Relation.Nullary using (yes; no)
@@ -17,21 +17,15 @@ import Relation.Nullary.Decidable as Dec
 open import Relation.Nullary.Product using (_×-dec_)
 open import Relation.Binary
 
-module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
+------------------------------------------------------------------------
+-- First as a decidable partial order (once made homogeneous)
 
-  uncons : ∀ {a b as bs} → Prefix R (a ∷ as) (b ∷ bs) → R a b × Prefix R as bs
-  uncons (x ∷ xs) = x , xs
+module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
 
   refl : Pointwise R ⇒ Prefix R
   refl []       = []
   refl (x ∷ xs) = x ∷ refl xs
 
-  infixl 5 _++_
-  _++_ : ∀ {as bs cs ds} → Pointwise R as bs → Prefix R cs ds →
-         Prefix R (as List.++ cs) (bs List.++ ds)
-  []            ++ cs⊆ds = cs⊆ds
-  (a∼b ∷ as∼bs) ++ cs⊆ds = a∼b ∷ (as∼bs ++ cs⊆ds)
-
 module _ {a b c r s t} {A : Set a} {B : Set b} {C : Set c}
          {R : REL A B r} {S : REL B C s} {T : REL A C t} where
 
@@ -39,6 +33,31 @@ module _ {a b c r s t} {A : Set a} {B : Set b} {C : Set c}
   trans rs⇒t []            bs~cs         = []
   trans rs⇒t (a∼b ∷ as∼bs) (b∼c ∷ bs∼cs) = rs⇒t a∼b b∼c ∷ trans rs⇒t as∼bs bs∼cs
 
+module _ {a b r s e} {A : Set a} {B : Set b}
+         {R : REL A B r} {S : REL B A s} {E : REL A B e} where
+
+  antisym : Antisym R S E → Antisym (Prefix R) (Prefix S) (Pointwise E)
+  antisym rs⇒e []            []            = []
+  antisym rs⇒e (a∼b ∷ as∼bs) (b∼a ∷ bs∼as) = rs⇒e a∼b b∼a ∷ antisym rs⇒e as∼bs bs∼as
+
+------------------------------------------------------------------------
+-- _++_
+
+module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
+
+  ++⁺ : ∀ {as bs cs ds} → Pointwise R as bs →
+        Prefix R cs ds → Prefix R (as List.++ cs) (bs List.++ ds)
+  ++⁺ []            cs⊆ds = cs⊆ds
+  ++⁺ (a∼b ∷ as∼bs) cs⊆ds = a∼b ∷ (++⁺ as∼bs cs⊆ds)
+
+  ++⁻ : ∀ {as bs cs ds} → Pointwise R as bs →
+        Prefix R (as List.++ cs) (bs List.++ ds) → Prefix R cs ds
+  ++⁻ []            cs⊆ds         = cs⊆ds
+  ++⁻ (a∼b ∷ as∼bs) (_ ∷ acs⊆bds) = ++⁻ as∼bs acs⊆bds
+
+------------------------------------------------------------------------
+-- map
+
 module _ {a b c d r} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
          {R : REL C D r} where
 
@@ -55,6 +74,9 @@ module _ {a b c d r} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
   map⁻ {a ∷ as} {[]}     f g ()
   map⁻ {a ∷ as} {b ∷ bs} f g (x ∷ xs) = x ∷ map⁻ f g xs
 
+------------------------------------------------------------------------
+-- Decidability
+
 module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
 
   prefix? : Decidable R → Decidable (Prefix R)
diff --git a/src/Relation/Binary/Core.agda b/src/Relation/Binary/Core.agda
index 76deae6bc7..8c3666454c 100644
--- a/src/Relation/Binary/Core.agda
+++ b/src/Relation/Binary/Core.agda
@@ -96,8 +96,12 @@ TransFlip P Q R = ∀ {i j k} → Q j k → P i j → R i k
 Transitive : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
 Transitive _∼_ = Trans _∼_ _∼_ _∼_
 
+Antisym : ∀ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} →
+          REL A B ℓ₁ → REL B A ℓ₂ → REL A B ℓ₃ → Set _
+Antisym R S E = ∀ {i j} → R i j → S j i → E i j
+
 Antisymmetric : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _
-Antisymmetric _≈_ _≤_ = ∀ {x y} → x ≤ y → y ≤ x → x ≈ y
+Antisymmetric _≈_ _≤_ = Antisym _≤_ _≤_ _≈_
 
 Asymmetric : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
 Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x)

From 195a1cd9005a820a16bf229f9504a5fbd7cd0809 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Sat, 3 Nov 2018 18:15:49 +0100
Subject: [PATCH 04/12] [ fix ] Antisymmetric's implicit names have changed

because it is now defined in terms of Antisym which uses the *same*
convention as the rest of the combinators in the file.
---
 src/Data/Fin/Subset/Properties.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda
index 68c03957b6..2dd397df8a 100644
--- a/src/Data/Fin/Subset/Properties.agda
+++ b/src/Data/Fin/Subset/Properties.agda
@@ -134,8 +134,8 @@ x∈⁅y⁆⇔x≡y {_} {x} {y} = equivalence
 ⊆-trans p⊆q q⊆r x∈p = q⊆r (p⊆q x∈p)
 
 ⊆-antisym : ∀ {n} → Antisymmetric _≡_ (_⊆_ {n})
-⊆-antisym {x = []}           {[]}           p⊆q q⊆p = refl
-⊆-antisym {x = x ∷ xs} {y ∷ ys} p⊆q q⊆p with x | y
+⊆-antisym {i = []}     {[]}     p⊆q q⊆p = refl
+⊆-antisym {i = x ∷ xs} {y ∷ ys} p⊆q q⊆p with x | y
 ... | inside  | inside  = cong₂ _∷_ refl (⊆-antisym (drop-∷-⊆ p⊆q) (drop-∷-⊆ q⊆p))
 ... | inside  | outside = contradiction (p⊆q here) λ()
 ... | outside | inside  = contradiction (q⊆p here) λ()

From 94bb804bb13b0e76654508f4e333a1b304f5217b Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Sat, 3 Nov 2018 21:10:36 +0100
Subject: [PATCH 05/12] [ new ] more properties related to list functions

---
 .../Prefix/Heterogeneous/Properties.agda      | 80 ++++++++++++++++---
 1 file changed, 67 insertions(+), 13 deletions(-)

diff --git a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
index 0131adf471..00534ce50e 100644
--- a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
@@ -6,32 +6,44 @@
 
 module Data.List.Relation.Prefix.Heterogeneous.Properties where
 
-open import Data.List.Base as List using (List; []; _∷_)
+open import Data.Empty
+open import Data.List.Base as List hiding (map; uncons)
+-- using (List; []; _∷_; _++_; filter; take)
 open import Data.List.Relation.Pointwise using (Pointwise; []; _∷_)
 open import Data.List.Relation.Prefix.Heterogeneous
-open import Data.Product using (uncurry)
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Nat.Properties using (suc-injective)
+open import Data.Product using (proj₁; proj₂; uncurry)
 open import Function
 
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary using (yes; no; ¬_)
 import Relation.Nullary.Decidable as Dec
 open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Unary as U using (Pred)
 open import Relation.Binary
+open import Relation.Binary.PropositionalEquality using (_≡_)
 
 ------------------------------------------------------------------------
 -- First as a decidable partial order (once made homogeneous)
 
 module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
 
-  refl : Pointwise R ⇒ Prefix R
-  refl []       = []
-  refl (x ∷ xs) = x ∷ refl xs
+  fromPointwise : Pointwise R ⇒ Prefix R
+  fromPointwise []       = []
+  fromPointwise (r ∷ rs) = r ∷ fromPointwise rs
+
+  toPointwise : ∀ {as bs} → length as ≡ length bs →
+                Prefix R as bs → Pointwise R as bs
+  toPointwise {bs = []} eq [] = []
+  toPointwise {bs = _ ∷ _} () []
+  toPointwise eq (r ∷ rs) = r ∷ toPointwise (suc-injective eq) rs
 
 module _ {a b c r s t} {A : Set a} {B : Set b} {C : Set c}
          {R : REL A B r} {S : REL B C s} {T : REL A C t} where
 
   trans : Trans R S T → Trans (Prefix R) (Prefix S) (Prefix T)
-  trans rs⇒t []            bs~cs         = []
-  trans rs⇒t (a∼b ∷ as∼bs) (b∼c ∷ bs∼cs) = rs⇒t a∼b b∼c ∷ trans rs⇒t as∼bs bs∼cs
+  trans rs⇒t []       ss       = []
+  trans rs⇒t (r ∷ rs) (s ∷ ss) = rs⇒t r s ∷ trans rs⇒t rs ss
 
 module _ {a b r s e} {A : Set a} {B : Set b}
          {R : REL A B r} {S : REL B A s} {E : REL A B e} where
@@ -46,12 +58,12 @@ module _ {a b r s e} {A : Set a} {B : Set b}
 module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
 
   ++⁺ : ∀ {as bs cs ds} → Pointwise R as bs →
-        Prefix R cs ds → Prefix R (as List.++ cs) (bs List.++ ds)
+        Prefix R cs ds → Prefix R (as ++ cs) (bs ++ ds)
   ++⁺ []            cs⊆ds = cs⊆ds
   ++⁺ (a∼b ∷ as∼bs) cs⊆ds = a∼b ∷ (++⁺ as∼bs cs⊆ds)
 
   ++⁻ : ∀ {as bs cs ds} → Pointwise R as bs →
-        Prefix R (as List.++ cs) (bs List.++ ds) → Prefix R cs ds
+        Prefix R (as ++ cs) (bs ++ ds) → Prefix R cs ds
   ++⁻ []            cs⊆ds         = cs⊆ds
   ++⁻ (a∼b ∷ as∼bs) (_ ∷ acs⊆bds) = ++⁻ as∼bs acs⊆bds
 
@@ -65,14 +77,56 @@ module _ {a b c d r} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
          Prefix (λ a b → R (f a) (g b)) as bs →
          Prefix R (List.map f as) (List.map g bs)
   map⁺ f g []       = []
-  map⁺ f g (x ∷ xs) = x ∷ map⁺ f g xs
+  map⁺ f g (r ∷ rs) = r ∷ map⁺ f g rs
 
   map⁻ : ∀ {as bs} (f : A → C) (g : B → D) →
          Prefix R (List.map f as) (List.map g bs) →
          Prefix (λ a b → R (f a) (g b)) as bs
-  map⁻ {[]}     {bs}     f g xs = []
+  map⁻ {[]}     {bs}     f g rs       = []
   map⁻ {a ∷ as} {[]}     f g ()
-  map⁻ {a ∷ as} {b ∷ bs} f g (x ∷ xs) = x ∷ map⁻ f g xs
+  map⁻ {a ∷ as} {b ∷ bs} f g (r ∷ rs) = r ∷ map⁻ f g rs
+
+------------------------------------------------------------------------
+-- filter
+
+module _ {a b r p q} {A : Set a} {B : Set b} {R : REL A B r}
+         {P : Pred A p} {Q : Pred B q} (P? : U.Decidable P) (Q? : U.Decidable Q)
+         (P⇒Q : ∀ {a b} → R a b → P a → Q b) (Q⇒P : ∀ {a b} → R a b → Q b → P a)
+         where
+
+  filter⁺ : ∀ {as bs} →
+            Prefix R as bs → Prefix R (filter P? as) (filter Q? bs)
+  filter⁺ [] = []
+  filter⁺ {a ∷ as} {b ∷ bs} (r ∷ rs) with P? a | Q? b
+  ... | yes pa | yes qb = r ∷ filter⁺ rs
+  ... | yes pa | no ¬qb = ⊥-elim (¬qb (P⇒Q r pa))
+  ... | no ¬pa | yes qb = ⊥-elim (¬pa (Q⇒P r qb))
+  ... | no ¬pa | no ¬qb = filter⁺ rs
+
+------------------------------------------------------------------------
+-- take
+
+module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
+
+  take⁺ : ∀ {as bs} n → Prefix R as bs → Prefix R (take n as) (take n bs)
+  take⁺ zero    rs       = []
+  take⁺ (suc n) []       = []
+  take⁺ (suc n) (r ∷ rs) = r ∷ take⁺ n rs
+
+------------------------------------------------------------------------
+-- drop
+
+  drop⁺ : ∀ {as bs} n → Prefix R as bs → Prefix R (drop n as) (drop n bs)
+  drop⁺ zero    rs       = rs
+  drop⁺ (suc n) []       = []
+  drop⁺ (suc n) (r ∷ rs) = drop⁺ n rs
+
+  drop⁻ : ∀ {as bs} n → Pointwise R (take n as) (take n bs) →
+          Prefix R (drop n as) (drop n bs) → Prefix R as bs
+  drop⁻                 zero    hds       tls = tls
+  drop⁻ {[]}            (suc n) hds       tls = []
+  drop⁻ {_ ∷ _} {[]}    (suc n) ()        tls
+  drop⁻ {_ ∷ _} {_ ∷ _} (suc n) (r ∷ hds) tls = r ∷ (drop⁻ n hds tls)
 
 ------------------------------------------------------------------------
 -- Decidability

From d92a21e316fbfcf976ecec3851bb6770011075ba Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Sat, 3 Nov 2018 21:15:07 +0100
Subject: [PATCH 06/12] [ cosmetic ] more renaming from as~bs to rs

---
 .../Relation/Prefix/Heterogeneous/Properties.agda    | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
index 00534ce50e..70962a63d8 100644
--- a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
@@ -49,8 +49,8 @@ module _ {a b r s e} {A : Set a} {B : Set b}
          {R : REL A B r} {S : REL B A s} {E : REL A B e} where
 
   antisym : Antisym R S E → Antisym (Prefix R) (Prefix S) (Pointwise E)
-  antisym rs⇒e []            []            = []
-  antisym rs⇒e (a∼b ∷ as∼bs) (b∼a ∷ bs∼as) = rs⇒e a∼b b∼a ∷ antisym rs⇒e as∼bs bs∼as
+  antisym rs⇒e []       []       = []
+  antisym rs⇒e (r ∷ rs) (s ∷ ss) = rs⇒e r s ∷ antisym rs⇒e rs ss
 
 ------------------------------------------------------------------------
 -- _++_
@@ -59,13 +59,13 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
 
   ++⁺ : ∀ {as bs cs ds} → Pointwise R as bs →
         Prefix R cs ds → Prefix R (as ++ cs) (bs ++ ds)
-  ++⁺ []            cs⊆ds = cs⊆ds
-  ++⁺ (a∼b ∷ as∼bs) cs⊆ds = a∼b ∷ (++⁺ as∼bs cs⊆ds)
+  ++⁺ []       cs⊆ds = cs⊆ds
+  ++⁺ (r ∷ rs) cs⊆ds = r ∷ (++⁺ rs cs⊆ds)
 
   ++⁻ : ∀ {as bs cs ds} → Pointwise R as bs →
         Prefix R (as ++ cs) (bs ++ ds) → Prefix R cs ds
-  ++⁻ []            cs⊆ds         = cs⊆ds
-  ++⁻ (a∼b ∷ as∼bs) (_ ∷ acs⊆bds) = ++⁻ as∼bs acs⊆bds
+  ++⁻ []       cs⊆ds         = cs⊆ds
+  ++⁻ (r ∷ rs) (_ ∷ acs⊆bds) = ++⁻ rs acs⊆bds
 
 ------------------------------------------------------------------------
 -- map

From a8884d429123c875dfbac9073f311ff84ea96597 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Sat, 3 Nov 2018 22:46:53 +0100
Subject: [PATCH 07/12] [ more ] properties of prefix

---
 .../List/Relation/Prefix/Heterogeneous.agda   | 15 ++++++++----
 .../Prefix/Heterogeneous/Properties.agda      | 23 +++++++++++++++----
 2 files changed, 29 insertions(+), 9 deletions(-)

diff --git a/src/Data/List/Relation/Prefix/Heterogeneous.agda b/src/Data/List/Relation/Prefix/Heterogeneous.agda
index 3007914cab..66acdd0458 100644
--- a/src/Data/List/Relation/Prefix/Heterogeneous.agda
+++ b/src/Data/List/Relation/Prefix/Heterogeneous.agda
@@ -16,15 +16,20 @@ data Prefix {a b r} {A : Set a} {B : Set b} (R : REL A B r)
   []  : ∀ {bs} → Prefix R [] bs
   _∷_ : ∀ {a b as bs} → R a b → Prefix R as bs → Prefix R (a ∷ as) (b ∷ bs)
 
+module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} {a b as bs} where
 
-module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
+  head : Prefix R (a ∷ as) (b ∷ bs) → R a b
+  head (r ∷ rs) = r
 
-  uncons : ∀ {a b as bs} → Prefix R (a ∷ as) (b ∷ bs) → R a b × Prefix R as bs
-  uncons (x ∷ xs) = x , xs
+  tail : Prefix R (a ∷ as) (b ∷ bs) → Prefix R as bs
+  tail (r ∷ rs) = rs
+
+  uncons : Prefix R (a ∷ as) (b ∷ bs) → R a b × Prefix R as bs
+  uncons (r ∷ rs) = r , rs
 
 module _ {a b r s} {A : Set a} {B : Set b} {R : REL A B r} {S : REL A B s} where
 
   map : R ⇒ S → Prefix R ⇒ Prefix S
-  map f []       = []
-  map f (x ∷ xs) = f x ∷ map f xs
+  map R⇒S []       = []
+  map R⇒S (r ∷ rs) = R⇒S r ∷ map R⇒S rs
 
diff --git a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
index 70962a63d8..4848cb5639 100644
--- a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
@@ -8,10 +8,9 @@ module Data.List.Relation.Prefix.Heterogeneous.Properties where
 
 open import Data.Empty
 open import Data.List.Base as List hiding (map; uncons)
--- using (List; []; _∷_; _++_; filter; take)
 open import Data.List.Relation.Pointwise using (Pointwise; []; _∷_)
 open import Data.List.Relation.Prefix.Heterogeneous
-open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Nat.Base using (ℕ; zero; suc; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (suc-injective)
 open import Data.Product using (proj₁; proj₂; uncurry)
 open import Function
@@ -52,6 +51,15 @@ module _ {a b r s e} {A : Set a} {B : Set b}
   antisym rs⇒e []       []       = []
   antisym rs⇒e (r ∷ rs) (s ∷ ss) = rs⇒e r s ∷ antisym rs⇒e rs ss
 
+------------------------------------------------------------------------
+-- length
+
+module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
+
+  length-mono-Prefix-≤ : ∀ {as bs} → Prefix R as bs → length as ≤ length bs
+  length-mono-Prefix-≤ []       = z≤n
+  length-mono-Prefix-≤ (r ∷ rs) = s≤s (length-mono-Prefix-≤ rs)
+
 ------------------------------------------------------------------------
 -- _++_
 
@@ -94,8 +102,7 @@ module _ {a b r p q} {A : Set a} {B : Set b} {R : REL A B r}
          (P⇒Q : ∀ {a b} → R a b → P a → Q b) (Q⇒P : ∀ {a b} → R a b → Q b → P a)
          where
 
-  filter⁺ : ∀ {as bs} →
-            Prefix R as bs → Prefix R (filter P? as) (filter Q? bs)
+  filter⁺ : ∀ {as bs} → Prefix R as bs → Prefix R (filter P? as) (filter Q? bs)
   filter⁺ [] = []
   filter⁺ {a ∷ as} {b ∷ bs} (r ∷ rs) with P? a | Q? b
   ... | yes pa | yes qb = r ∷ filter⁺ rs
@@ -113,6 +120,14 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
   take⁺ (suc n) []       = []
   take⁺ (suc n) (r ∷ rs) = r ∷ take⁺ n rs
 
+  take⁻ : ∀ {as bs} n →
+    Prefix R (take n as) (take n bs) → Prefix R (drop n as) (drop n bs) →
+    Prefix R as bs
+  take⁻                   zero    hds       tls = tls
+  take⁻ {[]}              (suc n) hds       tls = []
+  take⁻ {a ∷ as} {[]}     (suc n) ()        tls
+  take⁻ {a ∷ as} {b ∷ bs} (suc n) (r ∷ hds) tls = r ∷ take⁻ n hds tls
+
 ------------------------------------------------------------------------
 -- drop
 

From 508ac09ee5f1b4be61feec72e49ee8c033393f8d Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Sat, 3 Nov 2018 22:52:23 +0100
Subject: [PATCH 08/12] [ refactor ] relax one hypothesis

---
 .../List/Relation/Prefix/Heterogeneous/Properties.agda    | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
index 4848cb5639..aab2d67279 100644
--- a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
@@ -70,10 +70,12 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
   ++⁺ []       cs⊆ds = cs⊆ds
   ++⁺ (r ∷ rs) cs⊆ds = r ∷ (++⁺ rs cs⊆ds)
 
-  ++⁻ : ∀ {as bs cs ds} → Pointwise R as bs →
+  ++⁻ : ∀ {as bs cs ds} → length as ≡ length bs →
         Prefix R (as ++ cs) (bs ++ ds) → Prefix R cs ds
-  ++⁻ []       cs⊆ds         = cs⊆ds
-  ++⁻ (r ∷ rs) (_ ∷ acs⊆bds) = ++⁻ rs acs⊆bds
+  ++⁻ {[]}    {[]}    eq rs       = rs
+  ++⁻ {_ ∷ _} {_ ∷ _} eq (_ ∷ rs) = ++⁻ (suc-injective eq) rs
+  ++⁻ {[]} {_ ∷ _} ()
+  ++⁻ {_ ∷ _} {[]} ()
 
 ------------------------------------------------------------------------
 -- map

From bae5992f2abb2decac84419ba1e367130bdf5dba Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Sat, 3 Nov 2018 23:03:33 +0100
Subject: [PATCH 09/12] [ new ] results about replicate, inits

---
 src/Data/List/Base.agda                       |  2 +-
 .../Prefix/Heterogeneous/Properties.agda      | 27 +++++++++++++++++--
 2 files changed, 26 insertions(+), 3 deletions(-)

diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index eb75c3c74c..3f87499cb3 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -142,7 +142,7 @@ fromMaybe : ∀ {a} {A : Set a} → Maybe A → List A
 fromMaybe (just x) = [ x ]
 fromMaybe nothing  = []
 
-replicate : ∀ {a} {A : Set a} → (n : ℕ) → A → List A
+replicate : ∀ {a} {A : Set a} → ℕ → A → List A
 replicate zero    x = []
 replicate (suc n) x = x ∷ replicate n x
 
diff --git a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
index aab2d67279..c96e977d3b 100644
--- a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
@@ -7,9 +7,11 @@
 module Data.List.Relation.Prefix.Heterogeneous.Properties where
 
 open import Data.Empty
+open import Data.List.All as All using (All; []; _∷_)
+import Data.List.All.Properties as All
 open import Data.List.Base as List hiding (map; uncons)
 open import Data.List.Relation.Pointwise using (Pointwise; []; _∷_)
-open import Data.List.Relation.Prefix.Heterogeneous
+open import Data.List.Relation.Prefix.Heterogeneous as Prefix
 open import Data.Nat.Base using (ℕ; zero; suc; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (suc-injective)
 open import Data.Product using (proj₁; proj₂; uncurry)
@@ -20,7 +22,7 @@ import Relation.Nullary.Decidable as Dec
 open import Relation.Nullary.Product using (_×-dec_)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_)
 
 ------------------------------------------------------------------------
 -- First as a decidable partial order (once made homogeneous)
@@ -145,6 +147,27 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
   drop⁻ {_ ∷ _} {[]}    (suc n) ()        tls
   drop⁻ {_ ∷ _} {_ ∷ _} (suc n) (r ∷ hds) tls = r ∷ (drop⁻ n hds tls)
 
+------------------------------------------------------------------------
+-- replicate
+
+  replicate⁺ : ∀ {m n a b} → m ≤ n → R a b → Prefix R (replicate m a) (replicate n b)
+  replicate⁺ z≤n       r = []
+  replicate⁺ (s≤s m≤n) r = r ∷ replicate⁺ m≤n r
+
+  replicate⁻ : ∀ {m n a b} → m ≢ 0 → Prefix R (replicate m a) (replicate n b) → R a b
+  replicate⁻ {zero}  {n}     m≢0 r  = ⊥-elim (m≢0 P.refl)
+  replicate⁻ {suc m} {zero}  m≢0 ()
+  replicate⁻ {suc m} {suc n} m≢0 rs = Prefix.head rs
+
+------------------------------------------------------------------------
+-- inits
+
+module _ {a r} {A : Set a} {R : Rel A r} where
+
+  inits⁺ : ∀ {as} → Pointwise R as as → All (flip (Prefix R) as) (inits as)
+  inits⁺ []       = [] ∷ []
+  inits⁺ (r ∷ rs) = [] ∷ All.map⁺ (All.map (r ∷_) (inits⁺ rs))
+
 ------------------------------------------------------------------------
 -- Decidability
 

From 1f42f4ea33227ccd03e7b71da748087bfe3975cd Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Sat, 3 Nov 2018 23:28:32 +0100
Subject: [PATCH 10/12] [ more ] about inits and zip(With)

---
 CHANGELOG.md                                  |  3 +-
 .../Membership/Propositional/Properties.agda  |  7 ++++
 .../Prefix/Heterogeneous/Properties.agda      | 36 ++++++++++++++++++-
 3 files changed, 44 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 841aad1b2e..2067d5da58 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -102,9 +102,10 @@ Other minor additions
   respects : P Respects _≈_ → (All P) Respects _≋_
   ```
 
-* Added new proof to `Data.List.Membership.Propositional.Properties`:
+* Added new proofs to `Data.List.Membership.Propositional.Properties`:
   ```agda
   ∈-allFin : (k : Fin n) → k ∈ allFin n
+  []∈inits : [] ∈ inits as
   ```
 
 * Added new function to `Data.List.Membership.(Setoid/Propositional)`:
diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index e1ec06685e..f71eeaeab2 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -249,6 +249,13 @@ module _ {a} {A : Set a} {_•_ : Op₂ A} where
 ∈-allFin : ∀ {n} (k : Fin n) → k ∈ allFin n
 ∈-allFin = ∈-tabulate⁺
 
+------------------------------------------------------------------------
+-- inits
+
+[]∈inits : ∀ {a} {A : Set a} (as : List A) → [] ∈ inits as
+[]∈inits []       = here refl
+[]∈inits (a ∷ as) = here refl
+
 ------------------------------------------------------------------------
 -- Other properties
 
diff --git a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
index c96e977d3b..02da779193 100644
--- a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
@@ -10,11 +10,12 @@ open import Data.Empty
 open import Data.List.All as All using (All; []; _∷_)
 import Data.List.All.Properties as All
 open import Data.List.Base as List hiding (map; uncons)
+open import Data.List.Membership.Propositional.Properties using ([]∈inits)
 open import Data.List.Relation.Pointwise using (Pointwise; []; _∷_)
 open import Data.List.Relation.Prefix.Heterogeneous as Prefix
 open import Data.Nat.Base using (ℕ; zero; suc; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (suc-injective)
-open import Data.Product using (proj₁; proj₂; uncurry)
+open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂; uncurry)
 open import Function
 
 open import Relation.Nullary using (yes; no; ¬_)
@@ -168,6 +169,39 @@ module _ {a r} {A : Set a} {R : Rel A r} where
   inits⁺ []       = [] ∷ []
   inits⁺ (r ∷ rs) = [] ∷ All.map⁺ (All.map (r ∷_) (inits⁺ rs))
 
+  inits⁻ : ∀ {as} → All (flip (Prefix R) as) (inits as) → Pointwise R as as
+  inits⁻ {as = []}     rs       = []
+  inits⁻ {as = a ∷ as} (r ∷ rs) =
+    let (hd , tls) = All.unzip (All.map uncons (All.map⁻ rs)) in
+    All.lookup hd ([]∈inits as) ∷ inits⁻ tls
+
+------------------------------------------------------------------------
+-- zip(With)
+
+module _ {a b c} {A : Set a} {B : Set b} {C : Set c}
+         {d e f} {D : Set d} {E : Set e} {F : Set f}
+         {r s t} {R : REL A D r} {S : REL B E s} {T : REL C F t} where
+
+  zipWith⁺ : ∀ {as bs ds es} {f : A → B → C} {g : D → E → F} →
+    (∀ {a b c d} → R a c → S b d → T (f a b) (g c d)) →
+    Prefix R as ds → Prefix S bs es →
+    Prefix T (zipWith f as bs) (zipWith g ds es)
+  zipWith⁺ f []       ss       = []
+  zipWith⁺ f (r ∷ rs) []       = []
+  zipWith⁺ f (r ∷ rs) (s ∷ ss) = f r s ∷ zipWith⁺ f rs ss
+
+module _ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
+         {r s} {R : REL A C r} {S : REL B D s} where
+
+  private
+    R×S : REL (A × B) (C × D) _
+    R×S (a , b) (c , d) = R a c × S b d
+
+  zip⁺ : ∀ {as bs cs ds} → Prefix R as cs → Prefix S bs ds →
+         Prefix R×S (zip as bs) (zip cs ds)
+  zip⁺ = zipWith⁺ _,_
+
+
 ------------------------------------------------------------------------
 -- Decidability
 

From a051d484a38e52fb2f6e6f4c78e696c33d5be9ca Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Sun, 4 Nov 2018 23:29:55 +0100
Subject: [PATCH 11/12] [ new ] Prefix as a view on lists

---
 .../List/Relation/Prefix/Heterogeneous.agda   | 25 +++++++++++++++----
 1 file changed, 20 insertions(+), 5 deletions(-)

diff --git a/src/Data/List/Relation/Prefix/Heterogeneous.agda b/src/Data/List/Relation/Prefix/Heterogeneous.agda
index 66acdd0458..dd766d79a7 100644
--- a/src/Data/List/Relation/Prefix/Heterogeneous.agda
+++ b/src/Data/List/Relation/Prefix/Heterogeneous.agda
@@ -6,15 +6,20 @@
 
 module Data.List.Relation.Prefix.Heterogeneous where
 
+open import Level
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Pointwise using (Pointwise; []; _∷_)
-open import Data.Product using (_×_; _,_)
+open import Data.Product using (∃; _×_; _,_; uncurry)
 open import Relation.Binary using (REL; _⇒_)
 
-data Prefix {a b r} {A : Set a} {B : Set b} (R : REL A B r)
-          : REL (List A) (List B) r where
-  []  : ∀ {bs} → Prefix R [] bs
-  _∷_ : ∀ {a b as bs} → R a b → Prefix R as bs → Prefix R (a ∷ as) (b ∷ bs)
+module _ {a b r} {A : Set a} {B : Set b} (R : REL A B r) where
+
+  data Prefix : REL (List A) (List B) r where
+    []  : ∀ {bs} → Prefix [] bs
+    _∷_ : ∀ {a b as bs} → R a b → Prefix as bs → Prefix (a ∷ as) (b ∷ bs)
+
+  data PrefixView (as : List A) : List B → Set (b ⊔ r) where
+    _++_ : ∀ {cs} → Pointwise R as cs → ∀ ds → PrefixView as (cs List.++ ds)
 
 module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} {a b as bs} where
 
@@ -33,3 +38,13 @@ module _ {a b r s} {A : Set a} {B : Set b} {R : REL A B r} {S : REL A B s} where
   map R⇒S []       = []
   map R⇒S (r ∷ rs) = R⇒S r ∷ map R⇒S rs
 
+module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
+
+  toView : ∀ {as bs} → Prefix R as bs → PrefixView R as bs
+  toView []       = [] ++ _
+  toView (r ∷ rs) with toView rs
+  ... | rs′ ++ ds = (r ∷ rs′) ++ ds
+
+  fromView : ∀ {as bs} → PrefixView R as bs → Prefix R as bs
+  fromView ([]       ++ ds) = []
+  fromView ((r ∷ rs) ++ ds) = r ∷ fromView (rs ++ ds)

From 0e938a0dd125f5fe5be0fc42a0ec81d4b2851083 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Sun, 4 Nov 2018 23:57:28 +0100
Subject: [PATCH 12/12] [ new ] Prefix R is irrelevant if R is

---
 .../Relation/Prefix/Heterogeneous/Properties.agda   | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
index 02da779193..4f57a7d5ad 100644
--- a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
@@ -12,7 +12,7 @@ import Data.List.All.Properties as All
 open import Data.List.Base as List hiding (map; uncons)
 open import Data.List.Membership.Propositional.Properties using ([]∈inits)
 open import Data.List.Relation.Pointwise using (Pointwise; []; _∷_)
-open import Data.List.Relation.Prefix.Heterogeneous as Prefix
+open import Data.List.Relation.Prefix.Heterogeneous as Prefix hiding (PrefixView; _++_)
 open import Data.Nat.Base using (ℕ; zero; suc; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (suc-injective)
 open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂; uncurry)
@@ -201,12 +201,19 @@ module _ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
          Prefix R×S (zip as bs) (zip cs ds)
   zip⁺ = zipWith⁺ _,_
 
-
 ------------------------------------------------------------------------
--- Decidability
+-- Irrelevant
 
 module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
 
+  irrelevant : Irrelevant R → Irrelevant (Prefix R)
+  irrelevant R-irr []       []         = P.refl
+  irrelevant R-irr (r ∷ rs) (r′ ∷ rs′) =
+    P.cong₂ _∷_ (R-irr r r′) (irrelevant R-irr rs rs′)
+
+------------------------------------------------------------------------
+-- Decidability
+
   prefix? : Decidable R → Decidable (Prefix R)
   prefix? R? []       bs       = yes []
   prefix? R? (a ∷ as) []       = no (λ ())