More list properties about catMaybes/mapMaybe (#2389)

* More list properties about `catMaybes/mapMaybe`

- Follow-up to PR #2361
- Ported from my [formal-prelude](https://github.com/omelkonian/formal-prelude/tree/c10fe94876a7378088f2e4cf68d9b18858dcc256)

* Revert irrefutable `with`s for inductive hypotheses.

Author: omelkonian

CHANGELOG.md

@@ -414,47 +414,55 @@ Additions to existing modules
 
 * In `Data.List.Properties`:
   ```agda
-  length-catMaybes      : length (catMaybes xs) ≤ length xs
-  applyUpTo-∷ʳ          : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)
-  applyDownFrom-∷ʳ      : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n)
-  upTo-∷ʳ               : upTo n ∷ʳ n ≡ upTo (suc n)
-  downFrom-∷ʳ           : applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n)
-  reverse-selfInverse   : SelfInverse {A = List A} _≡_ reverse
-  reverse-applyUpTo     : reverse (applyUpTo f n) ≡ applyDownFrom f n
-  reverse-upTo          : reverse (upTo n) ≡ downFrom n
-  reverse-applyDownFrom : reverse (applyDownFrom f n) ≡ applyUpTo f n
-  reverse-downFrom      : reverse (downFrom n) ≡ upTo n
-  mapMaybe-map          : mapMaybe f ∘ map g ≗ mapMaybe (f ∘ g)
-  map-mapMaybe          : map g ∘ mapMaybe f ≗ mapMaybe (Maybe.map g ∘ f)
-  align-map             : align (map f xs) (map g ys) ≡ map (map f g) (align xs ys)
-  zip-map               : zip (map f xs) (map g ys) ≡ map (map f g) (zip xs ys)
-  unzipWith-map         : unzipWith f ∘ map g ≗ unzipWith (f ∘ g)
-  map-unzipWith         : map (map g) (map h) ∘ unzipWith f ≗ unzipWith (map g h ∘ f)
-  unzip-map             : unzip ∘ map (map f g) ≗ map (map f) (map g) ∘ unzip
-  splitAt-map           : splitAt n ∘ map f ≗ map (map f) (map f) ∘ splitAt n
-  uncons-map            : uncons ∘ map f ≗ map (map f (map f)) ∘ uncons
-  last-map              : last ∘ map f ≗ map f ∘ last
-  tail-map              : tail ∘ map f ≗ map (map f) ∘ tail
-  mapMaybe-cong         : f ≗ g → mapMaybe f ≗ mapMaybe g
-  zipWith-cong          : (∀ a b → f a b ≡ g a b) → ∀ as → zipWith f as ≗ zipWith g as
-  unzipWith-cong        : f ≗ g → unzipWith f ≗ unzipWith g
-  foldl-cong            : (∀ x y → f x y ≡ g x y) → ∀ x → foldl f x ≗ foldl g x
-  alignWith-flip        : alignWith f xs ys ≡ alignWith (f ∘ swap) ys xs
-  alignWith-comm        : f ∘ swap ≗ f → alignWith f xs ys ≡ alignWith f ys xs
-  align-flip            : align xs ys ≡ map swap (align ys xs)
-  zip-flip              : zip xs ys ≡ map swap (zip ys xs)
-  unzipWith-swap        : unzipWith (swap ∘ f) ≗ swap ∘ unzipWith f
-  unzip-swap            : unzip ∘ map swap ≗ swap ∘ unzip
-  take-take             : take n (take m xs) ≡ take (n ⊓ m) xs
-  take-drop             : take n (drop m xs) ≡ drop m (take (m + n) xs)
-  zip-unzip             : uncurry′ zip ∘ unzip ≗ id
-  unzipWith-zipWith     : f ∘ uncurry′ g ≗ id → length xs ≡ length ys → unzipWith f (zipWith g xs ys) ≡ (xs , ys)
-  unzip-zip             : length xs ≡ length ys → unzip (zip xs ys) ≡ (xs , ys)
-  mapMaybe-++           : mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys
-  unzipWith-++          : unzipWith f (xs ++ ys) ≡ zip _++_ _++_ (unzipWith f xs) (unzipWith f ys)
-  catMaybes-concatMap   : catMaybes ≗ concatMap fromMaybe
-  catMaybes-++          : catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys
-  map-catMaybes         : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f)
+  length-catMaybes       : length (catMaybes xs) ≤ length xs
+  applyUpTo-∷ʳ           : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)
+  applyDownFrom-∷ʳ       : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n)
+  upTo-∷ʳ                : upTo n ∷ʳ n ≡ upTo (suc n)
+  downFrom-∷ʳ            : applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n)
+  reverse-selfInverse    : SelfInverse {A = List A} _≡_ reverse
+  reverse-applyUpTo      : reverse (applyUpTo f n) ≡ applyDownFrom f n
+  reverse-upTo           : reverse (upTo n) ≡ downFrom n
+  reverse-applyDownFrom  : reverse (applyDownFrom f n) ≡ applyUpTo f n
+  reverse-downFrom       : reverse (downFrom n) ≡ upTo n
+  mapMaybe-map           : mapMaybe f ∘ map g ≗ mapMaybe (f ∘ g)
+  map-mapMaybe           : map g ∘ mapMaybe f ≗ mapMaybe (Maybe.map g ∘ f)
+  align-map              : align (map f xs) (map g ys) ≡ map (map f g) (align xs ys)
+  zip-map                : zip (map f xs) (map g ys) ≡ map (map f g) (zip xs ys)
+  unzipWith-map          : unzipWith f ∘ map g ≗ unzipWith (f ∘ g)
+  map-unzipWith          : map (map g) (map h) ∘ unzipWith f ≗ unzipWith (map g h ∘ f)
+  unzip-map              : unzip ∘ map (map f g) ≗ map (map f) (map g) ∘ unzip
+  splitAt-map            : splitAt n ∘ map f ≗ map (map f) (map f) ∘ splitAt n
+  uncons-map             : uncons ∘ map f ≗ map (map f (map f)) ∘ uncons
+  last-map               : last ∘ map f ≗ map f ∘ last
+  tail-map               : tail ∘ map f ≗ map (map f) ∘ tail
+  mapMaybe-cong          : f ≗ g → mapMaybe f ≗ mapMaybe g
+  zipWith-cong           : (∀ a b → f a b ≡ g a b) → ∀ as → zipWith f as ≗ zipWith g as
+  unzipWith-cong         : f ≗ g → unzipWith f ≗ unzipWith g
+  foldl-cong             : (∀ x y → f x y ≡ g x y) → ∀ x → foldl f x ≗ foldl g x
+  alignWith-flip         : alignWith f xs ys ≡ alignWith (f ∘ swap) ys xs
+  alignWith-comm         : f ∘ swap ≗ f → alignWith f xs ys ≡ alignWith f ys xs
+  align-flip             : align xs ys ≡ map swap (align ys xs)
+  zip-flip               : zip xs ys ≡ map swap (zip ys xs)
+  unzipWith-swap         : unzipWith (swap ∘ f) ≗ swap ∘ unzipWith f
+  unzip-swap             : unzip ∘ map swap ≗ swap ∘ unzip
+  take-take              : take n (take m xs) ≡ take (n ⊓ m) xs
+  take-drop              : take n (drop m xs) ≡ drop m (take (m + n) xs)
+  zip-unzip              : uncurry′ zip ∘ unzip ≗ id
+  unzipWith-zipWith      : f ∘ uncurry′ g ≗ id →
+                           length xs ≡ length ys →
+                           unzipWith f (zipWith g xs ys) ≡ (xs , ys)
+  unzip-zip              : length xs ≡ length ys → unzip (zip xs ys) ≡ (xs , ys)
+  mapMaybe-++            : mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys
+  unzipWith-++           : unzipWith f (xs ++ ys) ≡
+                           zip _++_ _++_ (unzipWith f xs) (unzipWith f ys)
+  catMaybes-concatMap    : catMaybes ≗ concatMap fromMaybe
+  catMaybes-++           : catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys
+  map-catMaybes          : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f)
+  Any-catMaybes⁺         : Any (M.Any P) xs → Any P (catMaybes xs)
+  mapMaybeIsInj₁∘mapInj₁ : mapMaybe isInj₁ (map inj₁ xs) ≡ xs
+  mapMaybeIsInj₁∘mapInj₂ : mapMaybe isInj₁ (map inj₂ xs) ≡ []
+  mapMaybeIsInj₂∘mapInj₂ : mapMaybe isInj₂ (map inj₂ xs) ≡ xs
+  mapMaybeIsInj₂∘mapInj₁ : mapMaybe isInj₂ (map inj₁ xs) ≡ []
   ```
 
 * In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
@@ -567,7 +575,15 @@ Additions to existing modules
 
 * Added new proofs to `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
   ```agda
-  product-↭ : product Preserves _↭_ ⟶ _≡_
+  product-↭   : product Preserves _↭_ ⟶ _≡_
+  catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys
+  mapMaybe-↭  : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
+  ```
+
+* Added new proofs to `Data.List.Relation.Binary.Permutation.Setoid.Properties.Maybe`:
+  ```agda
+  catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys
+  mapMaybe-↭  : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
   ```
 
 * In `Data.Rational.Properties`:

src/Data/List/Properties.agda

@@ -24,14 +24,15 @@ open import Data.List.Base as List
 open import Data.List.Membership.Propositional using (_∈_)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
-open import Data.Maybe.Base as Maybe using (Maybe; just; nothing; maybe)
+open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
+open import Data.Maybe.Relation.Unary.Any using (just) renaming (Any to MAny)
 open import Data.Nat.Base
 open import Data.Nat.Divisibility using (_∣_; divides; ∣n⇒∣m*n)
 open import Data.Nat.Properties
 open import Data.Product.Base as Product
   using (_×_; _,_; uncurry; uncurry′; proj₁; proj₂; <_,_>)
 import Data.Product.Relation.Unary.All as Product using (All)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Data.Sum using (_⊎_; inj₁; inj₂; isInj₁; isInj₂)
 open import Data.These.Base as These using (These; this; that; these)
 open import Data.Fin.Properties using (toℕ-cast)
 open import Function.Base using (id; _∘_; _∘′_; _∋_; _-⟨_∣; ∣_⟩-_; _$_; const; flip)
@@ -49,12 +50,11 @@ open import Relation.Unary using (Pred; Decidable; ∁)
 open import Relation.Unary.Properties using (∁?)
 import Data.Nat.GeneralisedArithmetic as ℕ
 
-
 open ≡-Reasoning
 
 private
   variable
-    a b c d e p : Level
+    a b c d e p ℓ : Level
     A : Set a
     B : Set b
     C : Set c
@@ -123,32 +123,6 @@ map-injective finj {x ∷ xs} {y ∷ ys} eq =
   let fx≡fy , fxs≡fys = ∷-injective eq in
   cong₂ _∷_ (finj fx≡fy) (map-injective finj fxs≡fys)
 
-------------------------------------------------------------------------
--- catMaybes
-
-catMaybes-concatMap : catMaybes {A = A} ≗ concatMap fromMaybe
-catMaybes-concatMap []             = refl
-catMaybes-concatMap (just x  ∷ xs) = cong (x ∷_) (catMaybes-concatMap xs)
-catMaybes-concatMap (nothing ∷ xs) = catMaybes-concatMap xs
-
-length-catMaybes : ∀ xs → length (catMaybes {A = A} xs) ≤ length xs
-length-catMaybes []             = ≤-refl
-length-catMaybes (just x  ∷ xs) = s≤s (length-catMaybes xs)
-length-catMaybes (nothing ∷ xs) = m≤n⇒m≤1+n (length-catMaybes xs)
-
-catMaybes-++ : (xs ys : List (Maybe A)) →
-               catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys
-catMaybes-++ []             ys = refl
-catMaybes-++ (just x  ∷ xs) ys = cong (x ∷_) (catMaybes-++ xs ys)
-catMaybes-++ (nothing ∷ xs) ys = catMaybes-++ xs ys
-
-module _ (f : A → B) where
-
-  map-catMaybes : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f)
-  map-catMaybes []             = refl
-  map-catMaybes (just x  ∷ xs) = cong (f x ∷_) (map-catMaybes xs)
-  map-catMaybes (nothing ∷ xs) = map-catMaybes xs
-
 ------------------------------------------------------------------------
 -- _++_
 
@@ -742,12 +716,40 @@ map-concatMap f g xs = begin
     ∎
 
 ------------------------------------------------------------------------
--- mapMaybe
+-- catMaybes
+
+catMaybes-concatMap : catMaybes {A = A} ≗ concatMap fromMaybe
+catMaybes-concatMap []             = refl
+catMaybes-concatMap (just x  ∷ xs) = cong (x ∷_) $ catMaybes-concatMap xs
+catMaybes-concatMap (nothing ∷ xs) = catMaybes-concatMap xs
+
+length-catMaybes : ∀ xs → length (catMaybes {A = A} xs) ≤ length xs
+length-catMaybes []             = ≤-refl
+length-catMaybes (just _  ∷ xs) = s≤s $ length-catMaybes xs
+length-catMaybes (nothing ∷ xs) = m≤n⇒m≤1+n $ length-catMaybes xs
 
-module _ {f g : A → Maybe B} where
+catMaybes-++ : (xs ys : List (Maybe A)) →
+               catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys
+catMaybes-++ []             _  = refl
+catMaybes-++ (just x  ∷ xs) ys = cong (x ∷_) $ catMaybes-++ xs ys
+catMaybes-++ (nothing ∷ xs) ys = catMaybes-++ xs ys
 
-  mapMaybe-cong : f ≗ g → mapMaybe f ≗ mapMaybe g
-  mapMaybe-cong f≗g = cong catMaybes ∘ map-cong f≗g
+map-catMaybes : (f : A → B) → map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f)
+map-catMaybes _ []             = refl
+map-catMaybes f (just x  ∷ xs) = cong (f x ∷_) $ map-catMaybes f xs
+map-catMaybes f (nothing ∷ xs) = map-catMaybes f xs
+
+Any-catMaybes⁺ : ∀ {P : Pred A ℓ} {xs : List (Maybe A)} →
+                 Any (MAny P) xs → Any P (catMaybes xs)
+Any-catMaybes⁺ {xs = nothing ∷ xs} (there x∈)       = Any-catMaybes⁺ x∈
+Any-catMaybes⁺ {xs = just x  ∷ xs} (here (just px)) = here px
+Any-catMaybes⁺ {xs = just x  ∷ xs} (there x∈)       = there $ Any-catMaybes⁺ x∈
+
+------------------------------------------------------------------------
+-- mapMaybe
+
+mapMaybe-cong : {f g : A → Maybe B} → f ≗ g → mapMaybe f ≗ mapMaybe g
+mapMaybe-cong f≗g = cong catMaybes ∘ map-cong f≗g
 
 mapMaybe-just : (xs : List A) → mapMaybe just xs ≡ xs
 mapMaybe-just []       = refl
@@ -793,6 +795,36 @@ module _ (g : B → C) (f : A → Maybe B) where
     mapMaybe (Maybe.map g) (map f xs)  ≡⟨ mapMaybe-map _ f xs ⟩
     mapMaybe (Maybe.map g ∘ f) xs      ∎
 
+-- embedding-projection pairs
+module _ {proj : B → Maybe A} {emb : A → B} where
+  mapMaybe-map-retract : proj ∘ emb ≗ just → mapMaybe proj ∘ map emb ≗ id
+  mapMaybe-map-retract retract xs = begin
+    mapMaybe proj (map emb xs) ≡⟨ mapMaybe-map _ _ xs ⟩
+    mapMaybe (proj ∘ emb) xs   ≡⟨ mapMaybe-cong retract xs ⟩
+    mapMaybe just xs           ≡⟨ mapMaybe-just _ ⟩
+    xs                         ∎
+
+module _ {proj : C → Maybe B} {emb : A → C} where
+  mapMaybe-map-none : proj ∘ emb ≗ const nothing → mapMaybe proj ∘ map emb ≗ const []
+  mapMaybe-map-none retract xs = begin
+    mapMaybe proj (map emb xs)  ≡⟨ mapMaybe-map _ _ xs ⟩
+    mapMaybe (proj ∘ emb) xs    ≡⟨ mapMaybe-cong retract xs ⟩
+    mapMaybe (const nothing) xs ≡⟨ mapMaybe-nothing xs ⟩
+    []                          ∎
+
+-- embedding-projection pairs on sums
+mapMaybeIsInj₁∘mapInj₁ : (xs : List A) → mapMaybe (isInj₁ {B = B}) (map inj₁ xs) ≡ xs
+mapMaybeIsInj₁∘mapInj₁ = mapMaybe-map-retract λ _ → refl
+
+mapMaybeIsInj₁∘mapInj₂ : (xs : List B) → mapMaybe (isInj₁ {A = A}) (map inj₂ xs) ≡ []
+mapMaybeIsInj₁∘mapInj₂ = mapMaybe-map-none λ _ → refl
+
+mapMaybeIsInj₂∘mapInj₂ : (xs : List B) → mapMaybe (isInj₂ {A = A}) (map inj₂ xs) ≡ xs
+mapMaybeIsInj₂∘mapInj₂ = mapMaybe-map-retract λ _ → refl
+
+mapMaybeIsInj₂∘mapInj₁ : (xs : List A) → mapMaybe (isInj₂ {B = B}) (map inj₁ xs) ≡ []
+mapMaybeIsInj₂∘mapInj₁ = mapMaybe-map-none λ _ → refl
+
 ------------------------------------------------------------------------
 -- sum
 

src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda

@@ -23,7 +23,8 @@ open import Data.List.Membership.Propositional
 open import Data.List.Membership.Propositional.Properties
 import Data.List.Properties as Lₚ
 open import Data.Product.Base using (_,_; _×_; ∃; ∃₂)
-open import Function.Base using (_∘_; _⟨_⟩_)
+open import Data.Maybe.Base using (Maybe; just; nothing)
+open import Function.Base using (_∘_; _⟨_⟩_; _$_)
 open import Level using (Level)
 open import Relation.Unary using (Pred)
 open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
@@ -38,6 +39,7 @@ private
     a b p : Level
     A : Set a
     B : Set b
+    xs ys : List A
 
 ------------------------------------------------------------------------
 -- Permutations of empty and singleton lists
@@ -373,3 +375,22 @@ product-↭ (swap {xs} {ys} x y r) = begin
   (y * x) * product ys ≡⟨ *-assoc y x (product ys) ⟩
   y * (x * product ys) ∎
   where open ≡-Reasoning
+
+------------------------------------------------------------------------
+-- catMaybes
+
+catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys
+catMaybes-↭ refl                         = refl
+catMaybes-↭ (trans xs↭ ↭ys)              = trans (catMaybes-↭ xs↭) (catMaybes-↭ ↭ys)
+catMaybes-↭ (prep nothing  xs↭)          = catMaybes-↭ xs↭
+catMaybes-↭ (prep (just x) xs↭)          = prep x $ catMaybes-↭ xs↭
+catMaybes-↭ (swap nothing  nothing  xs↭) = catMaybes-↭ xs↭
+catMaybes-↭ (swap nothing  (just y) xs↭) = prep y $ catMaybes-↭ xs↭
+catMaybes-↭ (swap (just x) nothing  xs↭) = prep x $ catMaybes-↭ xs↭
+catMaybes-↭ (swap (just x) (just y) xs↭) = swap x y $ catMaybes-↭ xs↭
+
+------------------------------------------------------------------------
+-- mapMaybe
+
+mapMaybe-↭ : (f : A → Maybe B) → xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
+mapMaybe-↭ f = catMaybes-↭ ∘ map⁺ f

src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda

@@ -144,7 +144,7 @@ steps-respʳ ys≋xs           (trans ys↭ws ws↭zs) = cong (steps ys↭ws +_)
 ------------------------------------------------------------------------
 -- map
 
-module _ (T : Setoid b ℓ) where
+module _ {ℓ} (T : Setoid b ℓ) where
 
   open Setoid T using () renaming (_≈_ to _≈′_)
   open Permutation T using () renaming (_↭_ to _↭′_)

src/Data/List/Relation/Binary/Permutation/Setoid/Properties/Maybe.agda

@@ -0,0 +1,70 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of permutations using setoid equality (on Maybe elements)
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.Relation.Binary.Permutation.Setoid.Properties.Maybe where
+
+open import Relation.Binary.Core using (_Preserves_⟶_)
+open import Relation.Binary.Bundles using (Setoid)
+
+open import Level using (Level)
+open import Function.Base using (_∘_; _$_)
+
+open import Data.List.Base using (catMaybes; mapMaybe)
+open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
+import Data.List.Relation.Binary.Permutation.Setoid as Permutation
+open import Data.List.Relation.Binary.Permutation.Setoid.Properties
+
+open import Data.Maybe using (Maybe; nothing; just)
+open import Data.Maybe.Relation.Binary.Pointwise using (nothing; just)
+  renaming (setoid to setoidᴹ)
+
+private
+  variable
+    a b ℓ ℓ′ : Level
+
+------------------------------------------------------------------------
+-- catMaybes
+
+module _ (sᴬ : Setoid a ℓ) where
+  open Setoid sᴬ using (_≈_)
+  open Permutation sᴬ
+
+  private sᴹ = setoidᴹ sᴬ
+  open Setoid sᴹ using () renaming (_≈_ to _≈ᴹ_)
+  open Permutation sᴹ using () renaming (_↭_ to _↭ᴹ_)
+
+  catMaybes-↭ : ∀ {xs ys} → xs ↭ᴹ ys → catMaybes xs ↭ catMaybes ys
+  catMaybes-↭ (refl p) = refl (pointwise p)
+    where
+    pointwise : ∀ {xs ys} → Pointwise _≈ᴹ_ xs ys →
+                Pointwise _≈_ (catMaybes xs) (catMaybes ys)
+    pointwise []             = []
+    pointwise (just p  ∷ ps) = p ∷ pointwise ps
+    pointwise (nothing ∷ ps) = pointwise ps
+  catMaybes-↭ (trans xs↭ ↭ys)              = trans (catMaybes-↭ xs↭) (catMaybes-↭ ↭ys)
+  catMaybes-↭ (prep nothing    xs↭)        = catMaybes-↭ xs↭
+  catMaybes-↭ (prep (just x~y) xs↭)        = prep x~y $ catMaybes-↭ xs↭
+  catMaybes-↭ (swap nothing  nothing  xs↭) = catMaybes-↭ xs↭
+  catMaybes-↭ (swap nothing  (just y) xs↭) = prep y $ catMaybes-↭ xs↭
+  catMaybes-↭ (swap (just x) nothing  xs↭) = prep x $ catMaybes-↭ xs↭
+  catMaybes-↭ (swap (just x) (just y) xs↭) = swap x y $ catMaybes-↭ xs↭
+
+------------------------------------------------------------------------
+-- mapMaybe
+
+module _ (sᴬ : Setoid a ℓ) (sᴮ : Setoid b ℓ′) where
+  open Setoid sᴬ using () renaming (_≈_ to _≈ᴬ_)
+  open Permutation sᴬ using () renaming (_↭_ to _↭ᴬ_)
+  open Permutation sᴮ using () renaming (_↭_ to _↭ᴮ_)
+
+  private sᴹᴮ = setoidᴹ sᴮ
+  open Setoid sᴹᴮ using () renaming (_≈_ to _≈ᴹᴮ_)
+
+  mapMaybe-↭ : ∀ {f} → f Preserves _≈ᴬ_ ⟶ _≈ᴹᴮ_ →
+               ∀ {xs ys} → xs ↭ᴬ ys → mapMaybe f xs ↭ᴮ mapMaybe f ys
+  mapMaybe-↭ pres = catMaybes-↭ sᴮ ∘ map⁺ sᴬ sᴹᴮ pres