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/22] [ 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/22] [ 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/22] [ 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/22] [ 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/22] [ 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/22] [ 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/22] [ 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/22] [ 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/22] [ 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/22] [ 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/22] [ 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/22] [ 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 (λ ())

From 61cd0afea6a19f9b708bcf569ae619f311957dbb Mon Sep 17 00:00:00 2001
From: Arjen Rouvoet <a.j.rouvoet@gmail.com>
Date: Fri, 23 Nov 2018 00:12:20 +0100
Subject: [PATCH 13/22] [ new ] Prefix is a preorder on lists

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

diff --git a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
index 4f57a7d5ad..532f41e3f4 100644
--- a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
@@ -11,7 +11,7 @@ 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.Pointwise using (Pointwise; []; _∷_; isEquivalence)
 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)
@@ -54,6 +54,17 @@ 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
 
+module _ {a e} {A : Set a} {_≈_ : Rel A e} (≈-equiv : IsEquivalence _≈_) where
+
+  isPreorder : IsPreorder {A = List A} (Pointwise _≈_) (Prefix _≈_)
+  isPreorder = record
+    { isEquivalence = isEquivalence ≈-equiv
+    ; reflexive = fromPointwise
+    ; trans = trans (IsEquivalence.trans ≈-equiv) }
+
+  preorder : Preorder _ _ _
+  preorder = record { isPreorder = isPreorder }
+
 ------------------------------------------------------------------------
 -- length
 

From c98c2a1a7d98097fb0319fc8f06a6fb51f44296a Mon Sep 17 00:00:00 2001
From: Arjen Rouvoet <a.j.rouvoet@gmail.com>
Date: Fri, 23 Nov 2018 00:15:34 +0100
Subject: [PATCH 14/22] [ new ] append and updateAt on List.All

---
 CHANGELOG.md           |  7 +++++++
 src/Data/List/All.agda | 28 ++++++++++++++++++++++++++++
 2 files changed, 35 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 26a2fa43fd..cca3d4decd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -161,6 +161,13 @@ Other minor additions
   mapM      : (Q ⊆ M ∘′ P) → All Q ⊆ (M ∘′ All P)
   forA      : All Q xs → (Q ⊆ F ∘′ P) → F (All P xs)
   forM      : All Q xs → (Q ⊆ M ∘′ P) → M (All P xs)
+
+  _++_      : ∀ {l m} → All P l → All P m → All P (l List.++ m)
+  _∷ʳ_      : ∀ {l : List A}{x} → All P l → P x → All P (l List.∷ʳ x)
+
+  updateAt  : ∀ {x xs} → x ∈ xs → (P x → P x) → All P xs → All P xs
+  _[_]%=_   : ∀ {x xs} → All P xs → x ∈ xs → (P x → P x) → All P xs
+  _[_]≔_    : ∀ {x xs} → All P xs → x ∈ xs → P x → All P xs
   ```
 
 * Added new operators to `Data.List.Base`:
diff --git a/src/Data/List/All.agda b/src/Data/List/All.agda
index c6e1609159..8dd4916090 100644
--- a/src/Data/List/All.agda
+++ b/src/Data/List/All.agda
@@ -54,6 +54,34 @@ map : ∀ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} →
 map g []         = []
 map g (px ∷ pxs) = g px ∷ map g pxs
 
+------------------------------------------------------------------------
+-- concat and append
+
+module _ {a p}{A : Set a}{P : Pred A p} where
+
+  _++_ : ∀ {l m} → All P l → All P m → All P (l List.++ m)
+  [] ++ pm = pm
+  (px ∷ pl) ++ pm = px ∷ (pl ++ pm)
+
+  _∷ʳ_ : ∀ {l : List A}{x} → All P l → P x → All P (l List.∷ʳ x)
+  pxs ∷ʳ px = pxs ++ (px ∷ [])
+
+------------------------------------------------------------------------
+-- (weak) updateAt
+module _ {a p}{A : Set a}{P : Pred A p} where
+  infixl 6 _[_]%=_ _[_]≔_
+
+  updateAt : ∀ {x xs} → x ∈ xs → (P x → P x) → All P xs → All P xs
+  updateAt () f []
+  updateAt (here refl) f (px ∷ pxs) = f px ∷ pxs
+  updateAt (there i)   f (px ∷ pxs) =   px ∷ updateAt i f pxs
+
+  _[_]%=_ : ∀ {x xs} → All P xs → x ∈ xs → (P x → P x) → All P xs
+  pxs [ i ]%= f = updateAt i f pxs
+
+  _[_]≔_ : ∀ {x xs} → All P xs → x ∈ xs → P x → All P xs
+  pxs [ i ]≔ px = pxs [ i ]%= const px
+
 ------------------------------------------------------------------------
 -- (un/)zip(With/)
 

From ae40db508541fc83e1cf11e7208accee4e25230f Mon Sep 17 00:00:00 2001
From: Arjen Rouvoet <a.j.rouvoet@gmail.com>
Date: Fri, 23 Nov 2018 11:41:21 +0100
Subject: [PATCH 15/22] =?UTF-8?q?[=20new=20]=20Add=20=E2=88=B7=CA=B3?=
 =?UTF-8?q?=E2=81=BB=20for=20Data.All=20and=20move=20to=20Properties?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/List/All.agda            | 13 +------------
 src/Data/List/All/Properties.agda | 13 ++++++++++++-
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/src/Data/List/All.agda b/src/Data/List/All.agda
index 8dd4916090..7f3dcd92fe 100644
--- a/src/Data/List/All.agda
+++ b/src/Data/List/All.agda
@@ -54,20 +54,9 @@ map : ∀ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} →
 map g []         = []
 map g (px ∷ pxs) = g px ∷ map g pxs
 
-------------------------------------------------------------------------
--- concat and append
-
-module _ {a p}{A : Set a}{P : Pred A p} where
-
-  _++_ : ∀ {l m} → All P l → All P m → All P (l List.++ m)
-  [] ++ pm = pm
-  (px ∷ pl) ++ pm = px ∷ (pl ++ pm)
-
-  _∷ʳ_ : ∀ {l : List A}{x} → All P l → P x → All P (l List.∷ʳ x)
-  pxs ∷ʳ px = pxs ++ (px ∷ [])
-
 ------------------------------------------------------------------------
 -- (weak) updateAt
+
 module _ {a p}{A : Set a}{P : Pred A p} where
   infixl 6 _[_]%=_ _[_]≔_
 
diff --git a/src/Data/List/All/Properties.agda b/src/Data/List/All/Properties.agda
index d7719f78b0..9e6477d39f 100644
--- a/src/Data/List/All/Properties.agda
+++ b/src/Data/List/All/Properties.agda
@@ -20,7 +20,7 @@ open import Data.List.Relation.Subset.Propositional using (_⊆_)
 open import Data.Maybe as Maybe using (Maybe; just; nothing)
 open import Data.Maybe.All as MAll using (just; nothing)
 open import Data.Nat using (zero; suc; z≤n; s≤s; _<_)
-open import Data.Product as Prod using (_×_; _,_; uncurry; uncurry′)
+open import Data.Product as Prod using (_×_; _,_; uncurry; uncurry′; map₂)
 open import Function
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Equivalence using (_⇔_; equivalence; Equivalence)
@@ -254,6 +254,17 @@ module _ {a p} {A : Set a} {P : A → Set p} where
   singleton⁻ : ∀ {x} → All P [ x ] → P x
   singleton⁻ (px ∷ []) = px
 
+------------------------------------------------------------------------
+-- snoc
+
+module _ {a p} {A : Set a} {P : A → Set p} where
+
+  ∷ʳ⁺ : ∀ {xs x} → All P xs → P x → All P (xs ∷ʳ x)
+  ∷ʳ⁺ pxs px = ++⁺ pxs (px ∷ [])
+
+  ∷ʳ⁻ : ∀ {xs x} → All P (xs ∷ʳ x) → All P xs × P x
+  ∷ʳ⁻ {xs} pxs = map₂ singleton⁻ $ ++⁻ xs pxs
+
 ------------------------------------------------------------------------
 -- fromMaybe
 

From f93728bf154d19cfd736cf434e5d0a9ae182c861 Mon Sep 17 00:00:00 2001
From: Arjen Rouvoet <a.j.rouvoet@gmail.com>
Date: Fri, 23 Nov 2018 12:03:34 +0100
Subject: [PATCH 16/22] [ new ] All.map properties

---
 src/Data/List/All/Properties.agda | 21 ++++++++++++++++++++-
 1 file changed, 20 insertions(+), 1 deletion(-)

diff --git a/src/Data/List/All/Properties.agda b/src/Data/List/All/Properties.agda
index 9e6477d39f..51c0a2029c 100644
--- a/src/Data/List/All/Properties.agda
+++ b/src/Data/List/All/Properties.agda
@@ -27,7 +27,7 @@ open import Function.Equivalence using (_⇔_; equivalence; Equivalence)
 open import Function.Inverse using (_↔_; inverse)
 open import Function.Surjection using (_↠_; surjection)
 open import Relation.Binary using (Setoid; _Respects_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)
 open import Relation.Nullary
 open import Relation.Unary
   using (Decidable; Pred; Universal) renaming (_⊆_ to _⋐_)
@@ -98,6 +98,25 @@ module _ {a b p} {A : Set a} {B : Set b} {P : B → Set p} {f : A → B} where
   map⁻ {xs = []}    []       = []
   map⁻ {xs = _ ∷ _} (p ∷ ps) = p ∷ map⁻ ps
 
+------------------------------------------------------------------------
+-- All.map
+
+module _ {a p} {A : Set a} {P Q : Pred A p} {f : P ⋐ Q} where
+  map-cong : ∀ {xs}{g : P ⋐ Q} → (ps : All P xs) →
+             (∀ {x} → f {x} ≗ g {x}) → All.map f ps ≡ All.map g ps
+  map-cong [] _          = P.refl
+  map-cong (px ∷ ps) feq = P.cong₂ _∷_ (feq px) (map-cong ps feq)
+
+  map-id : ∀ {xs} {f : P ⋐ P} → (ps : All P xs) →
+           (∀ {x} p → f {x} p ≡ p) → All.map f ps ≡ ps
+  map-id [] feq        = P.refl
+  map-id (px ∷ ps) feq = P.cong₂ _∷_ (feq px) (map-id ps feq)
+
+  map-compose : ∀ {Q R : Pred A p}{xs}{f : P ⋐ Q}{g : Q ⋐ R}(ps : All P xs) →
+                All.map g (All.map f ps) ≡ All.map (g ∘ f) ps
+  map-compose []        = P.refl
+  map-compose (px ∷ ps) = P.cong (_ ∷_) (map-compose ps)
+
 -- A variant of All.map.
 
 module _ {a b p q} {A : Set a} {B : Set b} {f : A → B}

From 4a3390eabad4326dd65cd7bdfc5fbf1dc2496574 Mon Sep 17 00:00:00 2001
From: Arjen Rouvoet <a.j.rouvoet@gmail.com>
Date: Fri, 23 Nov 2018 12:53:52 +0100
Subject: [PATCH 17/22] [ new ] Data.All.Properties.lookup-map

---
 src/Data/List/All/Properties.agda | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/Data/List/All/Properties.agda b/src/Data/List/All/Properties.agda
index 51c0a2029c..1be50b00e5 100644
--- a/src/Data/List/All/Properties.agda
+++ b/src/Data/List/All/Properties.agda
@@ -101,7 +101,8 @@ module _ {a b p} {A : Set a} {B : Set b} {P : B → Set p} {f : A → B} where
 ------------------------------------------------------------------------
 -- All.map
 
-module _ {a p} {A : Set a} {P Q : Pred A p} {f : P ⋐ Q} where
+module _ {a p q} {A : Set a} {P : Pred A p}{Q : Pred A q} {f : P ⋐ Q} where
+
   map-cong : ∀ {xs}{g : P ⋐ Q} → (ps : All P xs) →
              (∀ {x} → f {x} ≗ g {x}) → All.map f ps ≡ All.map g ps
   map-cong [] _          = P.refl
@@ -112,11 +113,17 @@ module _ {a p} {A : Set a} {P Q : Pred A p} {f : P ⋐ Q} where
   map-id [] feq        = P.refl
   map-id (px ∷ ps) feq = P.cong₂ _∷_ (feq px) (map-id ps feq)
 
-  map-compose : ∀ {Q R : Pred A p}{xs}{f : P ⋐ Q}{g : Q ⋐ R}(ps : All P xs) →
+  map-compose : ∀ {r}{R : Pred A r}{xs}{f : P ⋐ Q}{g : Q ⋐ R}(ps : All P xs) →
                 All.map g (All.map f ps) ≡ All.map (g ∘ f) ps
   map-compose []        = P.refl
   map-compose (px ∷ ps) = P.cong (_ ∷_) (map-compose ps)
 
+  lookup-map : ∀ {xs}{x : A}(ps : All P xs)(i : x ∈ xs) →
+               All.lookup (All.map f ps) i ≡ f (All.lookup ps i)
+  lookup-map [] ()
+  lookup-map (px ∷ pxs) (here P.refl) = P.refl
+  lookup-map (px ∷ pxs) (there i) = lookup-map pxs i
+
 -- A variant of All.map.
 
 module _ {a b p q} {A : Set a} {B : Set b} {f : A → B}

From 96bdb4caafea5b9785422316fc62ac0b49dac063 Mon Sep 17 00:00:00 2001
From: Arjen Rouvoet <a.j.rouvoet@gmail.com>
Date: Fri, 23 Nov 2018 15:58:48 +0100
Subject: [PATCH 18/22] [ new ] Monotone predicate monads

---
 CHANGELOG.md                             |  5 ++
 src/Category/Monad/Monotone.agda         | 66 ++++++++++++++++++++++++
 src/Relation/Unary/Closure/Preorder.agda |  4 ++
 3 files changed, 75 insertions(+)
 create mode 100644 src/Category/Monad/Monotone.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index da56b5a773..26b8663e2b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -121,6 +121,11 @@ Other minor additions
   record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ)
   ```
 
+* Added new module `Category.Monad.Monotone`:
+  ```agda
+  record RawMPMonad (M : Pt I ℓ) : Set (suc ℓ)
+  ```
+
 * Added new functions to `Codata.Colist`:
   ```agda
   fromCowriter : Cowriter W A i → Colist W i
diff --git a/src/Category/Monad/Monotone.agda b/src/Category/Monad/Monotone.agda
new file mode 100644
index 0000000000..b2e692913b
--- /dev/null
+++ b/src/Category/Monad/Monotone.agda
@@ -0,0 +1,66 @@
+open import Relation.Binary using (Preorder)
+
+module Category.Monad.Monotone {ℓ}(pre : Preorder ℓ ℓ ℓ) where
+
+open Preorder pre renaming (Carrier to I)
+
+open import Level
+open import Function
+
+open import Data.Product hiding (map)
+
+open import Relation.Unary
+open import Relation.Unary.PredicateTransformer using (Pt)
+open import Relation.Unary.Closure.Preorder pre hiding (map)
+
+open import Category.Monad.Predicate
+
+open Closed ⦃...⦄
+
+record RawMPMonad (M : Pt I ℓ) : Set (suc ℓ) where
+
+  infixl 1 _≥=_
+  field
+    return : ∀ {P} → P ⊆ M P
+    _≥=_   : ∀ {P Q} → M P ⊆ (□ (P ⇒ M Q) ⇒ M Q)
+
+  {- predicate monad -}
+  module _ {P : Pred I ℓ} where
+
+    map : ∀ {Q} → M P ⊆ (□ (P ⇒ Q) ⇒ M Q)
+    map m f = m ≥= (λ w p → return (f w p))
+
+    _>>=_ : ∀ {Q : Pred I ℓ} → M P ⊆ (λ i → (P ⊆ M Q) → M Q i)
+    c >>= f = c ≥= λ i≤j pj → f pj
+
+    -- infix monadic strength
+    infixl 10 _^_
+    _^_ : ∀ {Q : Pred I ℓ}⦃ m : Closed Q ⦄ → M P ⊆ (Q ⇒ M (P ∩ Q))
+    c ^ qi = c ≥= λ {j} x≤j pj → return (pj , next qi x≤j)
+
+    -- prefix monadic strength; useful when Q cannot be inferred
+    ts : ∀ Q ⦃ m : Closed Q ⦄ → M P ⊆ (Q ⇒ M (P ∩ Q))
+    ts _ c qi = c ^ qi
+
+  pmonad : RawPMonad {ℓ = ℓ} M
+  pmonad = record
+    { return? = return
+    ; _=<?_ = λ f px → px >>= f }
+
+  {- sequencing -}
+  module _ {A : Set ℓ}{P : A → Pred I ℓ} ⦃ mp : ∀ {a} → Closed (P a) ⦄  where
+    open import Data.List.All
+
+    instance
+      _ = ∼-closed
+
+    sequence′ : ∀ {as}{i k} → i ∼ k →
+                All (λ a → □ (M (P a)) i) as → M (λ j → All (λ a → P a j) as) k
+    sequence′ _ [] = return []
+    sequence′ le (x ∷ xs) = do
+      px  , le  ← x le ^ le
+      pxs , px  ← sequence′ le xs ^ px
+      return (px ∷ pxs)
+
+    sequence : ∀ {as i} → All (λ a → □ (M (P a)) i) as → M (λ j → All (λ a → P a j) as) i
+    sequence = sequence′ refl
diff --git a/src/Relation/Unary/Closure/Preorder.agda b/src/Relation/Unary/Closure/Preorder.agda
index 2d16751886..339e2224fe 100644
--- a/src/Relation/Unary/Closure/Preorder.agda
+++ b/src/Relation/Unary/Closure/Preorder.agda
@@ -9,6 +9,7 @@ open import Relation.Binary
 module Relation.Unary.Closure.Preorder {a r e} (P : Preorder a e r) where
 
 open Preorder P
+
 open import Relation.Unary using (Pred)
 
 -- Specialising the results proven generically in `Base`.
@@ -28,3 +29,6 @@ module _ {t} {T : Pred Carrier t} where
 
 □-closed : ∀ {t} {T : Pred Carrier t} → Closed (□ T)
 □-closed = Base.□-closed trans
+
+∼-closed : ∀ {x} → Closed (x ∼_)
+∼-closed = record { next = λ x∼y y∼z → trans x∼y y∼z }

From 1a1aa2be4048c7ae81962e6afd01904a23f6fbb9 Mon Sep 17 00:00:00 2001
From: Arjen Rouvoet <a.j.rouvoet@gmail.com>
Date: Fri, 23 Nov 2018 16:15:42 +0100
Subject: [PATCH 19/22] [ new ] Monotone predicate monads instances

Identity, Reader, Error, State
---
 CHANGELOG.md                              |  7 ++-
 src/Category/Monad/Monotone/Error.agda    | 48 ++++++++++++++++++++
 src/Category/Monad/Monotone/Identity.agda | 16 +++++++
 src/Category/Monad/Monotone/Reader.agda   | 54 +++++++++++++++++++++++
 src/Category/Monad/Monotone/State.agda    | 48 ++++++++++++++++++++
 5 files changed, 172 insertions(+), 1 deletion(-)
 create mode 100644 src/Category/Monad/Monotone/Error.agda
 create mode 100644 src/Category/Monad/Monotone/Identity.agda
 create mode 100644 src/Category/Monad/Monotone/Reader.agda
 create mode 100644 src/Category/Monad/Monotone/State.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 26b8663e2b..129c9bf3c8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -121,9 +121,14 @@ Other minor additions
   record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ)
   ```
 
-* Added new module `Category.Monad.Monotone`:
+* Added new modules `Category.Monad.Monotone(.*)`:
   ```agda
   record RawMPMonad (M : Pt I ℓ) : Set (suc ℓ)
+  Identity : Pt I i
+  record Identity
+  record ReaderMonad E (M : Pred I ℓ → Pt I ℓ) : Set (suc ℓ) where
+  record ErrorMonad (M : Pt I ℓ) : Set (suc ℓ) where
+  record StateMonad (M : Pt I ℓ) : Set (suc ℓ) where
   ```
 
 * Added new functions to `Codata.Colist`:
diff --git a/src/Category/Monad/Monotone/Error.agda b/src/Category/Monad/Monotone/Error.agda
new file mode 100644
index 0000000000..56a2518872
--- /dev/null
+++ b/src/Category/Monad/Monotone/Error.agda
@@ -0,0 +1,48 @@
+open import Relation.Binary hiding (_⇒_)
+
+module Category.Monad.Monotone.Error {ℓ}(pre : Preorder ℓ ℓ ℓ)(Exc : Set ℓ) where
+
+open import Function
+open import Level hiding (lift)
+open import Data.Sum
+
+open import Relation.Unary
+open import Relation.Unary.Closure.Preorder pre
+open import Relation.Unary.PredicateTransformer
+
+open import Category.Monad.Monotone pre
+open import Category.Monad.Monotone.Identity pre
+
+open Preorder pre renaming (Carrier to I)
+
+ErrorT : Pt I ℓ → Pt I ℓ
+ErrorT M P = M (λ i → Exc ⊎ P i)
+
+Error = ErrorT Identity
+
+record ErrorMonad (M : Pt I ℓ) : Set (suc ℓ) where
+  field
+    throw      : ∀ {P i} → Exc → M P i
+    try_catch_ : ∀ {P}   → M P ⊆ (□ (const Exc ⇒ M P)) ⇒ M P
+
+module _ {M} (Mon : RawMPMonad M) where
+  private module M = RawMPMonad Mon
+
+  open RawMPMonad
+  errorT-monad : RawMPMonad (ErrorT M)
+  return errorT-monad px   = M.return (inj₂ px)
+  _≥=_   errorT-monad px f =
+    px M.≥= λ where
+      v (inj₁ e) → M.return (inj₁ e)
+      v (inj₂ x) → f v x
+
+  open ErrorMonad
+  errorT-monad-ops : ErrorMonad (ErrorT M)
+  throw      errorT-monad-ops e   = M.return (inj₁ e)
+  try_catch_ errorT-monad-ops c f =
+    c M.≥= λ where
+      v (inj₁ e) → f v e
+      v (inj₂ x) → M.return (inj₂ x)
+
+  lift-error : ∀ {P} → M P ⊆ ErrorT M P
+  lift-error x = x M.>>= (λ z → M.return (inj₂ z))
diff --git a/src/Category/Monad/Monotone/Identity.agda b/src/Category/Monad/Monotone/Identity.agda
new file mode 100644
index 0000000000..830c9b906e
--- /dev/null
+++ b/src/Category/Monad/Monotone/Identity.agda
@@ -0,0 +1,16 @@
+open import Relation.Binary
+
+module Category.Monad.Monotone.Identity {i}(pre : Preorder i i i) where
+
+open Preorder pre renaming (Carrier to I)
+
+open import Relation.Unary.PredicateTransformer using (Pt)
+open import Category.Monad.Monotone pre
+open RawMPMonad
+
+Identity : Pt I i
+Identity = λ P i → P i
+
+id-monad : RawMPMonad Identity
+return id-monad px = px
+_≥=_ id-monad c f = f refl c
diff --git a/src/Category/Monad/Monotone/Reader.agda b/src/Category/Monad/Monotone/Reader.agda
new file mode 100644
index 0000000000..2605db3173
--- /dev/null
+++ b/src/Category/Monad/Monotone/Reader.agda
@@ -0,0 +1,54 @@
+open import Relation.Binary using (Preorder)
+
+module Category.Monad.Monotone.Reader {ℓ}(pre : Preorder ℓ ℓ ℓ) where
+
+open import Function
+open import Level
+
+open import Data.Product
+
+open import Relation.Unary.PredicateTransformer using (Pt)
+open import Relation.Unary
+open import Relation.Unary.Closure.Preorder pre
+
+open import Category.Monad
+open import Category.Monad.Monotone.Identity pre
+open import Category.Monad.Monotone pre
+
+open Preorder pre renaming (Carrier to I)
+open Closed ⦃...⦄
+
+ReaderT : Pred I ℓ → Pt I ℓ → Pt I ℓ
+ReaderT E M P = λ i → E i → M P i
+
+Reader : (Pred I ℓ) → Pt I ℓ
+Reader E = ReaderT E Identity
+
+record ReaderMonad E (M : Pred I ℓ → Pt I ℓ) : Set (suc ℓ) where
+  field
+    ask    : ∀ {i}    → M E E i
+    reader : ∀ {P}    → (E ⇒ P) ⊆ M E P
+    local  : ∀ {P E'} → (E ⇒ E') ⊆ (M E' P ⇒ M E P)
+
+  asks : ∀ {A} → (E ⇒ A) ⊆ M E A
+  asks = reader
+
+module _ {M : Pt I ℓ}(Mon : RawMPMonad M) where
+  private module M = RawMPMonad Mon
+
+  module _ {E}⦃ _ : Closed E ⦄ where
+    open RawMPMonad
+    reader-monad : RawMPMonad (ReaderT E M)
+    return reader-monad x e   = M.return x
+    _≥=_   reader-monad m f e =
+      m e M.≥= λ
+        i≤j px → f i≤j px (next e i≤j)
+
+    open ReaderMonad
+    reader-monad-ops : ReaderMonad E (λ E → ReaderT E M)
+    ask    reader-monad-ops e     = M.return e
+    reader reader-monad-ops f e   = M.return (f e)
+    local  reader-monad-ops f c e = c (f e)
+
+  lift-reader : ∀ {P} E → M P ⊆ ReaderT E M P
+  lift-reader _ z _ = z
diff --git a/src/Category/Monad/Monotone/State.agda b/src/Category/Monad/Monotone/State.agda
new file mode 100644
index 0000000000..ab77234bf8
--- /dev/null
+++ b/src/Category/Monad/Monotone/State.agda
@@ -0,0 +1,48 @@
+open import Relation.Binary using (Preorder)
+
+module Category.Monad.Monotone.State {ℓ}(pre : Preorder ℓ ℓ ℓ)
+  (H : Preorder.Carrier pre → Set ℓ)
+  where
+
+open Preorder pre renaming (Carrier to I)
+
+open import Level
+open import Function
+open import Data.Product
+
+open import Relation.Unary
+open import Relation.Unary.PredicateTransformer using (Pt)
+open import Relation.Unary.Closure.Preorder pre
+
+open import Category.Monad
+open import Category.Monad.Monotone pre
+open import Category.Monad.Monotone.Identity pre
+
+MST : (Set ℓ → Set ℓ) → Pt I ℓ
+MST M P = H ⇒ (λ i → M (∃ λ j → i ∼ j × H j × P j))
+
+MSt : Pt I ℓ
+MSt = MST id
+
+record StateMonad (M : Pt I ℓ) : Set (suc ℓ) where
+  field
+    runState : ∀ {P} → □ (H ⇒ (H ∩ P)) ⊆ M P
+
+  get : ∀ {i} → M H i
+  get = runState λ _ μ → μ , μ
+
+module _ {M}(Mon : RawMonad {ℓ} M) where
+  private module M = RawMonad Mon
+
+  open RawMPMonad
+  mst-monad : RawMPMonad (MST M)
+  return mst-monad px  μ = M.return (_ , refl , μ , px)
+  _≥=_   mst-monad c f μ = c μ M.>>= λ where
+    (i₁ , ext₁ , μ₁ , pv) → (f ext₁ pv μ₁) M.>>= λ where
+      (i₂ , ext₂ , μ₂ , pw) → M.return (i₂ , trans ext₁ ext₂ , μ₂ , pw)
+
+  open StateMonad
+  mst-monad-ops : StateMonad (MST M)
+  runState (mst-monad-ops) f μ =
+    let (μ' , p) = f refl μ
+    in M.return (_ , refl , μ' , p)

From 3176534fc45e228539ab822c00ca341330dd698a Mon Sep 17 00:00:00 2001
From: Arjen Rouvoet <a.j.rouvoet@gmail.com>
Date: Fri, 23 Nov 2018 16:30:13 +0100
Subject: [PATCH 20/22] [ new ] Monotone Heap Monad

Includes a necessary Any property.
---
 CHANGELOG.md                                |  2 +
 src/Category/Monad/Monotone/Heap.agda       | 47 +++++++++++++
 src/Category/Monad/Monotone/Heap/HList.agda | 75 +++++++++++++++++++++
 src/Data/List/Any/Properties.agda           | 12 ++++
 4 files changed, 136 insertions(+)
 create mode 100644 src/Category/Monad/Monotone/Heap.agda
 create mode 100644 src/Category/Monad/Monotone/Heap/HList.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 129c9bf3c8..f91e67f75f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -129,6 +129,7 @@ Other minor additions
   record ReaderMonad E (M : Pred I ℓ → Pt I ℓ) : Set (suc ℓ) where
   record ErrorMonad (M : Pt I ℓ) : Set (suc ℓ) where
   record StateMonad (M : Pt I ℓ) : Set (suc ℓ) where
+  record HeapMonad  (M : Pt I ℓ) : Set (suc ℓ) where
   ```
 
 * Added new functions to `Codata.Colist`:
@@ -288,6 +289,7 @@ Other minor additions
   fromList⁻    : Any P (fromList xs) → List.Any P xs
   toList⁺      : Any P xs → List.Any P (toList xs)
   toList⁻      : List.Any P (toList xs) → Any P xs
+  prefix⁺      : ∀ {xs ys} → Prefix R xs ys → Any P xs → Any P ys
   ```
 
 * Added new functions to `Data.Vec.Membership.Propositional.Properties`:
diff --git a/src/Category/Monad/Monotone/Heap.agda b/src/Category/Monad/Monotone/Heap.agda
new file mode 100644
index 0000000000..1ef4c5ecea
--- /dev/null
+++ b/src/Category/Monad/Monotone/Heap.agda
@@ -0,0 +1,47 @@
+import Relation.Unary.Closure.Preorder as Closure
+open import Relation.Binary using (Preorder)
+
+module Category.Monad.Monotone.Heap
+  -- ordered heap types
+  {ℓ}(pre : Preorder ℓ ℓ ℓ)
+  -- types
+  (T : Set ℓ)
+  -- weakenable values
+  (V : T → Preorder.Carrier pre → Set ℓ) ⦃ wkV : ∀ {a} → Closure.Closed pre (V a) ⦄
+  -- heaps indexed by the heap type
+  (H : Preorder.Carrier pre → Set ℓ)
+  -- weakenable heap type membership
+  (_∈_ : T → Preorder.Carrier pre → Set ℓ) ⦃ wk∈ : ∀ {a} → Closure.Closed pre (_∈_ a) ⦄ where
+
+open Preorder pre renaming (Carrier to I)
+
+open import Level
+open import Data.Unit using (⊤; tt)
+open import Data.Product
+
+open import Relation.Unary hiding (_∈_)
+open import Relation.Unary.PredicateTransformer using (Pt)
+open import Relation.Unary.Closure.Preorder pre
+
+open import Category.Monad.Monotone pre
+open import Category.Monad.Monotone.State pre H
+
+open Closed ⦃...⦄
+
+record HeapMonad (M : Pt I ℓ) : Set (suc ℓ) where
+  field
+    super : StateMonad M
+
+  open StateMonad super public
+
+  field
+    store  : ∀ {a} → V a ⊆ M (λ W → a ∈ W)
+    modify : ∀ {a} → _∈_ a ⊆ V a ⇒ M (V a)
+    deref  : ∀ {a} → _∈_ a ⊆ M (V a)
+
+  module HeapMonadOps (m : RawMPMonad M) where
+    open RawMPMonad m
+    open import Data.List.All as All
+
+    storeₙ  : ∀ {W as} → All (λ a → V a W) as → M (λ W' → All (λ a → a ∈ W') as) W
+    storeₙ vs = sequence (All.map (λ v {x} ext → store (next v ext)) vs)
diff --git a/src/Category/Monad/Monotone/Heap/HList.agda b/src/Category/Monad/Monotone/Heap/HList.agda
new file mode 100644
index 0000000000..8202430a03
--- /dev/null
+++ b/src/Category/Monad/Monotone/Heap/HList.agda
@@ -0,0 +1,75 @@
+-- An example implementation of the monotone HeapMonad
+-- using heterogeneous lists as a memory model.
+
+import Relation.Unary.Closure.Preorder as Closure
+import Relation.Binary.PropositionalEquality as P
+open import Data.List.Relation.Prefix.Heterogeneous.Properties using (preorder)
+open import Data.List
+
+module Category.Monad.Monotone.Heap.HList
+  (T : Set)
+  (V : T → List T → Set)
+  ⦃ wkV : ∀ {a} → Closure.Closed (preorder P.isEquivalence) (V a) ⦄ where
+
+open import Function
+open import Data.Product
+open import Data.List.All as All
+open import Data.List.All.Properties
+open import Data.List.Any
+open import Data.List.Any.Properties
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Relation.Prefix.Heterogeneous
+import Data.List.Relation.Pointwise as PW
+
+open import Relation.Unary using (Pred)
+open import Relation.Binary using (Preorder)
+
+open import Category.Monad using (RawMonad)
+
+ord : Preorder _ _ _
+ord = (preorder {A = T} P.isEquivalence)
+
+open Preorder ord renaming (refl to ∼-refl)
+open import Relation.Unary.Closure.Preorder ord
+open Closed ⦃...⦄
+
+instance
+  _ = ∼-closed
+
+  ∈-closed : ∀ {x} → Closed (x ∈_)
+  ∈-closed = record
+    { next = λ x∈xs xs∼ys → prefix⁺ (flip P.trans) xs∼ys x∈xs }
+
+  All-closed : ∀ {ys} → Closed (λ xs → All (λ y → V y xs) ys)
+  All-closed = record
+    { next = λ pys xs∼zs → All.map (λ p → next p xs∼zs) pys }
+
+HeapT : Set
+HeapT = List T
+
+Heap : Pred HeapT _
+Heap = λ W → All (λ a → V a W) W
+
+open import Category.Monad.Monotone ord
+open import Category.Monad.Monotone.State ord Heap
+open import Category.Monad.Monotone.Heap ord T V Heap _∈_
+
+module _ {M : Set → Set}(mon : RawMonad M) where
+  private module M = RawMonad mon
+
+  open HeapMonad
+  hlist-heap-monad : HeapMonad (MST M)
+  super  hlist-heap-monad             = mst-monad-ops mon
+  store  hlist-heap-monad {x}{xs} v μ =
+    let ext = fromView (PW.refl P.refl PrefixView.++ [ x ])
+    in M.return (
+      xs ∷ʳ x ,
+      ext ,
+      ∷ʳ⁺ (next μ ext) (next v ext) ,
+      ++⁺ʳ xs (here P.refl))
+  modify hlist-heap-monad ptr v μ     =
+    M.return (-, ∼-refl , μ [ ptr ]≔ v , All.lookup μ ptr)
+  deref  hlist-heap-monad ptr μ       =
+    M.return (-, ∼-refl , μ , All.lookup μ ptr)
+
+  open HeapMonadOps hlist-heap-monad public
diff --git a/src/Data/List/Any/Properties.agda b/src/Data/List/Any/Properties.agda
index 8b35779e27..52a1b6cbe4 100644
--- a/src/Data/List/Any/Properties.agda
+++ b/src/Data/List/Any/Properties.agda
@@ -579,3 +579,15 @@ module _ {ℓ} {A B : Set ℓ} where
     (Any P xs × Any Q ys)                    ↔⟨ ×↔ ⟩
     Any (λ x → Any (λ y → P x × Q y) ys) xs  ↔⟨ ⊗↔ ⟩
     Any (P ⟨×⟩ Q) (xs ⊗ ys)                  ∎
+
+------------------------------------------------------------------------
+-- Prefix
+
+module _ {a r p} {A : Set a} {R : Rel A r} {P : Pred A p}
+         (resp : P Respects R) where
+
+ open import Data.List.Relation.Prefix.Heterogeneous as Prefix
+
+ prefix⁺ : ∀ {xs ys} → Prefix R xs ys → Any P xs → Any P ys
+ prefix⁺ rs e with toView rs
+ prefix⁺ rs e | ss Prefix.++ ts = ++⁺ˡ (lift-resp resp ss e)

From 2d4a87df28808a7d06310d938b896a5eb1ed3053 Mon Sep 17 00:00:00 2001
From: Arjen Rouvoet <a.j.rouvoet@gmail.com>
Date: Fri, 23 Nov 2018 18:05:54 +0100
Subject: [PATCH 21/22] [ refactor ] Move prefix preorder Prefix.Setoid

---
 .../Prefix/Heterogeneous/Properties.agda      | 11 -------
 src/Data/List/Relation/Prefix/Setoid.agda     | 33 +++++++++++++++++++
 2 files changed, 33 insertions(+), 11 deletions(-)
 create mode 100644 src/Data/List/Relation/Prefix/Setoid.agda

diff --git a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
index 532f41e3f4..8cd575cef9 100644
--- a/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Prefix/Heterogeneous/Properties.agda
@@ -54,17 +54,6 @@ 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
 
-module _ {a e} {A : Set a} {_≈_ : Rel A e} (≈-equiv : IsEquivalence _≈_) where
-
-  isPreorder : IsPreorder {A = List A} (Pointwise _≈_) (Prefix _≈_)
-  isPreorder = record
-    { isEquivalence = isEquivalence ≈-equiv
-    ; reflexive = fromPointwise
-    ; trans = trans (IsEquivalence.trans ≈-equiv) }
-
-  preorder : Preorder _ _ _
-  preorder = record { isPreorder = isPreorder }
-
 ------------------------------------------------------------------------
 -- length
 
diff --git a/src/Data/List/Relation/Prefix/Setoid.agda b/src/Data/List/Relation/Prefix/Setoid.agda
new file mode 100644
index 0000000000..b56357d2cd
--- /dev/null
+++ b/src/Data/List/Relation/Prefix/Setoid.agda
@@ -0,0 +1,33 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The prefix relation over setoid equality.
+------------------------------------------------------------------------
+
+open import Relation.Binary using (Setoid; IsPreorder; Preorder; IsEquivalence)
+
+module Data.List.Relation.Prefix.Setoid
+  {c ℓ} (S : Setoid c ℓ) where
+
+open import Data.List using (List)
+open import Data.List.Membership.Setoid S using (_∈_)
+open import Data.List.Relation.Prefix.Heterogeneous
+open import Data.List.Relation.Prefix.Heterogeneous.Properties
+open import Data.List.Relation.Pointwise hiding (isPreorder; preorder)
+open import Level using (_⊔_)
+open import Relation.Nullary using (¬_)
+
+open Setoid S using () renaming (Carrier to A)
+module S = Setoid S
+
+------------------------------------------------------------------------
+-- Definitions
+
+isPreorder : IsPreorder {A = List A} (Pointwise S._≈_) (Prefix S._≈_)
+isPreorder = record
+  { isEquivalence = isEquivalence S.isEquivalence
+  ; reflexive     = fromPointwise
+  ; trans         = trans S.trans }
+
+preorder : Preorder _ _ _
+preorder = record { isPreorder = isPreorder }

From 458b0d54b98fd5bd4c58c99ef7ce73babf31e9b3 Mon Sep 17 00:00:00 2001
From: Arjen Rouvoet <a.j.rouvoet@gmail.com>
Date: Fri, 23 Nov 2018 18:06:56 +0100
Subject: [PATCH 22/22] Fix HeapMonad instance imports

---
 src/Category/Monad/Monotone/Heap/HList.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Category/Monad/Monotone/Heap/HList.agda b/src/Category/Monad/Monotone/Heap/HList.agda
index 8202430a03..7daa956194 100644
--- a/src/Category/Monad/Monotone/Heap/HList.agda
+++ b/src/Category/Monad/Monotone/Heap/HList.agda
@@ -3,13 +3,13 @@
 
 import Relation.Unary.Closure.Preorder as Closure
 import Relation.Binary.PropositionalEquality as P
-open import Data.List.Relation.Prefix.Heterogeneous.Properties using (preorder)
+open import Data.List.Relation.Prefix.Setoid using (preorder)
 open import Data.List
 
 module Category.Monad.Monotone.Heap.HList
   (T : Set)
   (V : T → List T → Set)
-  ⦃ wkV : ∀ {a} → Closure.Closed (preorder P.isEquivalence) (V a) ⦄ where
+  ⦃ wkV : ∀ {a} → Closure.Closed (preorder (P.setoid T)) (V a) ⦄ where
 
 open import Function
 open import Data.Product
@@ -27,7 +27,7 @@ open import Relation.Binary using (Preorder)
 open import Category.Monad using (RawMonad)
 
 ord : Preorder _ _ _
-ord = (preorder {A = T} P.isEquivalence)
+ord = preorder (P.setoid T)
 
 open Preorder ord renaming (refl to ∼-refl)
 open import Relation.Unary.Closure.Preorder ord