    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- List-related properties
    ------------------------------------------------------------------------

    -- Note that the lemmas below could be generalised to work with other
    -- equalities than _≡_.

    {-# OPTIONS --cubical-compatible --safe #-}
    {-# OPTIONS --warning=noUserWarning #-} -- for deprecated scans

    module Data.List.Properties where

    open import Algebra.Bundles using (Semigroup; Monoid)
    open import Algebra.Consequences.Propositional
     using (selfInverse⇒involutive; selfInverse⇒injective)
    open import Algebra.Definitions as AlgebraicDefinitions using (SelfInverse; Involutive)
    open import Algebra.Morphism.Structures using (IsMagmaHomomorphism; IsMonoidHomomorphism)
    import Algebra.Structures as AlgebraicStructures
    open import Data.Bool.Base using (Bool; false; true; not; if_then_else_)
    open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ)
    open import Data.List.Base as List
    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)
    open import Data.Maybe.Relation.Unary.Any using (just) renaming (Any to MAny)
    open import Data.Nat.Base
    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 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)
    open import Function.Definitions using (Injective)
    open import Level using (Level)
    open import Relation.Binary.Definitions as B using (DecidableEquality)
    import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
    open import Relation.Binary.PropositionalEquality.Core as ≡
    open import Relation.Binary.PropositionalEquality.Properties as ≡
    open import Relation.Binary.Core using (Rel)
    open import Relation.Nullary.Reflects using (invert)
    open import Relation.Nullary.Decidable.Core using (Dec; yes; no; _because_; does)
    open import Relation.Nullary.Negation.Core using (contradiction; ¬_)
    open import Relation.Nullary.Decidable as Decidable
      using (isYes; map′; ⌊_⌋; ¬?; _×-dec_; dec-true; dec-false)
    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 q ℓ : Level
        A : Set a
        B : Set b
        C : Set c
        D : Set d
        E : Set e
        x y z w : A
        xs ys zs ws : List A

    ------------------------------------------------------------------------
    -- _∷_

    ∷-injective : x ∷ xs ≡ y List.∷ ys → x ≡ y × xs ≡ ys
    ∷-injective refl = refl , refl

    ∷-injectiveˡ : x ∷ xs ≡ y List.∷ ys → x ≡ y
    ∷-injectiveˡ refl = refl

    ∷-injectiveʳ : x ∷ xs ≡ y List.∷ ys → xs ≡ ys
    ∷-injectiveʳ refl = refl

    ∷-dec : Dec (x ≡ y) → Dec (xs ≡ ys) → Dec (x ∷ xs ≡ y List.∷ ys)
    ∷-dec x≟y xs≟ys = Decidable.map′ (uncurry (cong₂ _∷_)) ∷-injective (x≟y ×-dec xs≟ys)

    ≡-dec : DecidableEquality A → DecidableEquality (List A)
    ≡-dec _≟_ []       []       = yes refl
    ≡-dec _≟_ (x ∷ xs) []       = no λ()
    ≡-dec _≟_ []       (y ∷ ys) = no λ()
    ≡-dec _≟_ (x ∷ xs) (y ∷ ys) = ∷-dec (x ≟ y) (≡-dec _≟_ xs ys)

    ------------------------------------------------------------------------
    -- map

    map-id : map id ≗ id {A = List A}
    map-id []       = refl
    map-id (x ∷ xs) = cong (x ∷_) (map-id xs)

    map-id-local : ∀ {f : A → A} {xs} → All (λ x → f x ≡ x) xs → map f xs ≡ xs
    map-id-local []           = refl
    map-id-local (fx≡x ∷ pxs) = cong₂ _∷_ fx≡x (map-id-local pxs)

    map-++ : ∀ (f : A → B) xs ys →
                     map f (xs ++ ys) ≡ map f xs ++ map f ys
    map-++ f []       ys = refl
    map-++ f (x ∷ xs) ys = cong (f x ∷_) (map-++ f xs ys)

    map-cong : ∀ {f g : A → B} → f ≗ g → map f ≗ map g
    map-cong f≗g []       = refl
    map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (map-cong f≗g xs)

    map-cong-local : ∀ {f g : A → B} {xs} →
                All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs
    map-cong-local []                = refl
    map-cong-local (fx≡gx ∷ fxs≡gxs) = cong₂ _∷_ fx≡gx (map-cong-local fxs≡gxs)

    length-map : ∀ (f : A → B) xs → length (map f xs) ≡ length xs
    length-map f []       = refl
    length-map f (x ∷ xs) = cong suc (length-map f xs)

    map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f
    map-∘ []       = refl
    map-∘ (x ∷ xs) = cong (_ ∷_) (map-∘ xs)

    map-injective : ∀ {f : A → B} → Injective _≡_ _≡_ f → Injective _≡_ _≡_ (map f)
    map-injective finj {[]} {[]} eq = refl
    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)

    ------------------------------------------------------------------------
    -- _++_

    length-++ : ∀ (xs : List A) {ys} →
                length (xs ++ ys) ≡ length xs + length ys
    length-++ []       = refl
    length-++ (x ∷ xs) = cong suc (length-++ xs)

    module _ {A : Set a} where

      open AlgebraicDefinitions {A = List A} _≡_

      ++-assoc : Associative _++_
      ++-assoc []       ys zs = refl
      ++-assoc (x ∷ xs) ys zs = cong (x ∷_) (++-assoc xs ys zs)

      ++-identityˡ : LeftIdentity [] _++_
      ++-identityˡ xs = refl

      ++-identityʳ : RightIdentity [] _++_
      ++-identityʳ []       = refl
      ++-identityʳ (x ∷ xs) = cong (x ∷_) (++-identityʳ xs)

      ++-identity : Identity [] _++_
      ++-identity = ++-identityˡ , ++-identityʳ

      ++-identityʳ-unique : ∀ (xs : List A) {ys} → xs ≡ xs ++ ys → ys ≡ []
      ++-identityʳ-unique []       refl = refl
      ++-identityʳ-unique (x ∷ xs) eq   =
        ++-identityʳ-unique xs (∷-injectiveʳ eq)

      ++-identityˡ-unique : ∀ {xs} (ys : List A) → xs ≡ ys ++ xs → ys ≡ []
      ++-identityˡ-unique               []       _  = refl
      ++-identityˡ-unique {xs = x ∷ xs} (y ∷ ys) eq
        with ++-identityˡ-unique (ys ++ [ x ]) (begin
             xs                  ≡⟨ ∷-injectiveʳ eq ⟩
             ys ++ x ∷ xs        ≡⟨ ++-assoc ys [ x ] xs ⟨
             (ys ++ [ x ]) ++ xs ∎)
      ++-identityˡ-unique {xs = x ∷ xs} (y ∷ []   ) eq | ()
      ++-identityˡ-unique {xs = x ∷ xs} (y ∷ _ ∷ _) eq | ()

      ++-cancelˡ : LeftCancellative _++_
      ++-cancelˡ []       _ _ ys≡zs             = ys≡zs
      ++-cancelˡ (x ∷ xs) _ _ x∷xs++ys≡x∷xs++zs = ++-cancelˡ xs _ _ (∷-injectiveʳ x∷xs++ys≡x∷xs++zs)

      ++-cancelʳ : RightCancellative _++_
      ++-cancelʳ _  []       []       _             = refl
      ++-cancelʳ xs []       (z ∷ zs) eq =
        contradiction (trans (cong length eq) (length-++ (z ∷ zs))) (m≢1+n+m (length xs))
      ++-cancelʳ xs (y ∷ ys) []       eq =
        contradiction (trans (sym (length-++ (y ∷ ys))) (cong length eq)) (m≢1+n+m (length xs) ∘ sym)
      ++-cancelʳ _  (y ∷ ys) (z ∷ zs) eq =
        cong₂ _∷_ (∷-injectiveˡ eq) (++-cancelʳ _ ys zs (∷-injectiveʳ eq))

      ++-cancel : Cancellative _++_
      ++-cancel = ++-cancelˡ , ++-cancelʳ

      ++-conicalˡ : ∀ (xs ys : List A) → xs ++ ys ≡ [] → xs ≡ []
      ++-conicalˡ []       _ refl = refl

      ++-conicalʳ : ∀ (xs ys : List A) → xs ++ ys ≡ [] → ys ≡ []
      ++-conicalʳ []       _ refl = refl

      ++-conical : Conical [] _++_
      ++-conical = ++-conicalˡ , ++-conicalʳ

    length-++-sucˡ : ∀ (x : A) (xs ys : List A) →
                     length (x ∷ xs ++ ys) ≡ suc (length (xs ++ ys))
    length-++-sucˡ _ _ _ = refl

    length-++-sucʳ : ∀ (xs : List A) (y : A) (ys : List A) →
                     length (xs ++ y ∷ ys) ≡ suc (length (xs ++ ys))
    length-++-sucʳ []       _ _  = refl
    length-++-sucʳ (_ ∷ xs) y ys = cong suc (length-++-sucʳ xs y ys)

    length-++-comm : ∀ (xs ys : List A) →
                     length (xs ++ ys) ≡ length (ys ++ xs)
    length-++-comm xs       []       = cong length (++-identityʳ xs)
    length-++-comm []       (y ∷ ys) = sym (cong length (++-identityʳ (y ∷ ys)))
    length-++-comm (x ∷ xs) (y ∷ ys) =
      begin
        length (x ∷ xs ++ y ∷ ys)
      ≡⟨⟩
        suc (length (xs ++ y ∷ ys))
      ≡⟨ cong suc (length-++-sucʳ xs y ys) ⟩
        suc (suc (length (xs ++ ys)))
      ≡⟨ cong suc (cong suc (length-++-comm xs ys)) ⟩
        suc (suc (length (ys ++ xs)))
      ≡⟨ cong suc (length-++-sucʳ ys x xs) ⟨
        suc (length (ys ++ x ∷ xs))
      ≡⟨⟩
        length (y ∷ ys ++ x ∷ xs)
      ∎

    length-++-≤ˡ : ∀ (xs : List A) {ys} →
                  length xs ≤ length (xs ++ ys)
    length-++-≤ˡ []       = z≤n
    length-++-≤ˡ (x ∷ xs) = s≤s (length-++-≤ˡ xs)

    length-++-≤ʳ : ∀ (ys : List A) {xs} →
                  length ys ≤ length (xs ++ ys)
    length-++-≤ʳ ys {xs} = ≤-trans (length-++-≤ˡ ys) (≤-reflexive (length-++-comm ys xs))

    module _ {A : Set a} where

      open AlgebraicStructures  {A = List A} _≡_

      ++-isMagma : IsMagma _++_
      ++-isMagma = record
        { isEquivalence = isEquivalence
        ; ∙-cong        = cong₂ _++_
        }

      ++-isSemigroup : IsSemigroup _++_
      ++-isSemigroup = record
        { isMagma = ++-isMagma
        ; assoc   = ++-assoc
        }

      ++-isMonoid : IsMonoid _++_ []
      ++-isMonoid = record
        { isSemigroup = ++-isSemigroup
        ; identity    = ++-identity
        }

    module _ (A : Set a) where

      ++-semigroup : Semigroup a a
      ++-semigroup = record
        { Carrier     = List A
        ; isSemigroup = ++-isSemigroup
        }

      ++-monoid : Monoid a a
      ++-monoid = record
        { Carrier  = List A
        ; isMonoid = ++-isMonoid
        }

    module _ (A : Set a) where

      length-isMagmaHomomorphism : IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length
      length-isMagmaHomomorphism = record
        { isRelHomomorphism = record
          { cong = cong length
          }
        ; homo = λ xs ys → length-++ xs {ys}
        }

      length-isMonoidHomomorphism : IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length
      length-isMonoidHomomorphism = record
        { isMagmaHomomorphism = length-isMagmaHomomorphism
        ; ε-homo = refl
        }

    ------------------------------------------------------------------------
    -- cartesianProductWith

    module _ (f : A → B → C) where

      private
        prod = cartesianProductWith f

      cartesianProductWith-zeroˡ : ∀ ys → prod [] ys ≡ []
      cartesianProductWith-zeroˡ _ = refl

      cartesianProductWith-zeroʳ : ∀ xs → prod xs [] ≡ []
      cartesianProductWith-zeroʳ []       = refl
      cartesianProductWith-zeroʳ (x ∷ xs) = cartesianProductWith-zeroʳ xs

      cartesianProductWith-distribʳ-++ : ∀ xs ys zs → prod (xs ++ ys) zs ≡ prod xs zs ++ prod ys zs
      cartesianProductWith-distribʳ-++ []       ys zs = refl
      cartesianProductWith-distribʳ-++ (x ∷ xs) ys zs = begin
        prod (x ∷ xs ++ ys) zs ≡⟨⟩
        map (f x) zs ++ prod (xs ++ ys) zs ≡⟨ cong (map (f x) zs ++_) (cartesianProductWith-distribʳ-++ xs ys zs) ⟩
        map (f x) zs ++ prod xs zs ++ prod ys zs ≡⟨ ++-assoc (map (f x) zs) (prod xs zs) (prod ys zs) ⟨
        (map (f x) zs ++ prod xs zs) ++ prod ys zs ≡⟨⟩
        prod (x ∷ xs) zs ++ prod ys zs ∎

    ------------------------------------------------------------------------
    -- alignWith

    module _ {f g : These A B → C} where

      alignWith-cong : f ≗ g → ∀ as → alignWith f as ≗ alignWith g as
      alignWith-cong f≗g []         bs       = map-cong (f≗g ∘ that) bs
      alignWith-cong f≗g as@(_ ∷ _) []       = map-cong (f≗g ∘ this) as
      alignWith-cong f≗g (a ∷ as)   (b ∷ bs) =
        cong₂ _∷_ (f≗g (these a b)) (alignWith-cong f≗g as bs)

    module _ {f : These A B → C} where

      length-alignWith : ∀ xs ys →
                       length (alignWith f xs ys) ≡ length xs ⊔ length ys
      length-alignWith []         ys       = length-map (f ∘′ that) ys
      length-alignWith xs@(_ ∷ _) []       = length-map (f ∘′ this) xs
      length-alignWith (x ∷ xs)   (y ∷ ys) = cong suc (length-alignWith xs ys)

      alignWith-map : (g : D → A) (h : E → B) →
                      ∀ xs ys → alignWith f (map g xs) (map h ys) ≡
                                alignWith (f ∘′ These.map g h) xs ys
      alignWith-map g h []         ys     = sym (map-∘ ys)
      alignWith-map g h xs@(_ ∷ _) []     = sym (map-∘ xs)
      alignWith-map g h (x ∷ xs) (y ∷ ys) =
        cong₂ _∷_ refl (alignWith-map g h xs ys)

      map-alignWith : ∀ (g : C → D) → ∀ xs ys →
                      map g (alignWith f xs ys) ≡
                      alignWith (g ∘′ f) xs ys
      map-alignWith g []         ys     = sym (map-∘ ys)
      map-alignWith g xs@(_ ∷ _) []     = sym (map-∘ xs)
      map-alignWith g (x ∷ xs) (y ∷ ys) =
        cong₂ _∷_ refl (map-alignWith g xs ys)

      alignWith-flip : ∀ xs ys →
                     alignWith f xs ys ≡ alignWith (f ∘ These.swap) ys xs
      alignWith-flip []       []       = refl
      alignWith-flip []       (y ∷ ys) = refl
      alignWith-flip (x ∷ xs) []       = refl
      alignWith-flip (x ∷ xs) (y ∷ ys) = cong (_ ∷_) (alignWith-flip xs ys)

    module _ {f : These A A → B} where

      alignWith-comm : f ∘ These.swap ≗ f →
                     ∀ xs ys → alignWith f xs ys ≡ alignWith f ys xs
      alignWith-comm f-comm xs ys = begin
        alignWith f xs ys                ≡⟨ alignWith-flip xs ys ⟩
        alignWith (f ∘ These.swap) ys xs ≡⟨ alignWith-cong f-comm ys xs ⟩
        alignWith f ys xs                ∎

    ------------------------------------------------------------------------
    -- align

    align-map : ∀ (f : A → B) (g : C → D) →
                ∀ xs ys → align (map f xs) (map g ys) ≡
                          map (These.map f g) (align xs ys)
    align-map f g xs ys = begin
      align (map f xs) (map g ys)       ≡⟨ alignWith-map f g xs ys ⟩
      alignWith (These.map f g) xs ys   ≡⟨ sym (map-alignWith (These.map f g) xs ys) ⟩
      map (These.map f g) (align xs ys) ∎

    align-flip : ∀ (xs : List A) (ys : List B) →
                 align xs ys ≡ map These.swap (align ys xs)
    align-flip xs ys = begin
      align xs ys                  ≡⟨ alignWith-flip xs ys ⟩
      alignWith These.swap ys xs   ≡⟨ sym (map-alignWith These.swap ys xs) ⟩
      map These.swap (align ys xs) ∎

    ------------------------------------------------------------------------
    -- zipWith

    module _ {f g : A → B → C} where

      zipWith-cong : (∀ a b → f a b ≡ g a b) → ∀ as → zipWith f as ≗ zipWith g as
      zipWith-cong f≗g []         bs       = refl
      zipWith-cong f≗g as@(_ ∷ _) []       = refl
      zipWith-cong f≗g (a ∷ as)   (b ∷ bs) =
        cong₂ _∷_ (f≗g a b) (zipWith-cong f≗g as bs)

    module _ (f : A → B → C) where

      zipWith-zeroˡ : ∀ xs → zipWith f [] xs ≡ []
      zipWith-zeroˡ []       = refl
      zipWith-zeroˡ (x ∷ xs) = refl

      zipWith-zeroʳ : ∀ xs → zipWith f xs [] ≡ []
      zipWith-zeroʳ []       = refl
      zipWith-zeroʳ (x ∷ xs) = refl

      length-zipWith : ∀ xs ys →
                       length (zipWith f xs ys) ≡ length xs ⊓ length ys
      length-zipWith []       []       = refl
      length-zipWith []       (y ∷ ys) = refl
      length-zipWith (x ∷ xs) []       = refl
      length-zipWith (x ∷ xs) (y ∷ ys) = cong suc (length-zipWith xs ys)

      zipWith-map : ∀ (g : D → A) (h : E → B) →
                    ∀ xs ys → zipWith f (map g xs) (map h ys) ≡
                              zipWith (λ x y → f (g x) (h y)) xs ys
      zipWith-map g h []       []       = refl
      zipWith-map g h []       (y ∷ ys) = refl
      zipWith-map g h (x ∷ xs) []       = refl
      zipWith-map g h (x ∷ xs) (y ∷ ys) =
        cong₂ _∷_ refl (zipWith-map g h xs ys)

      map-zipWith : ∀ (g : C → D) → ∀ xs ys →
                    map g (zipWith f xs ys) ≡
                    zipWith (λ x y → g (f x y)) xs ys
      map-zipWith g []       []       = refl
      map-zipWith g []       (y ∷ ys) = refl
      map-zipWith g (x ∷ xs) []       = refl
      map-zipWith g (x ∷ xs) (y ∷ ys) =
        cong₂ _∷_ refl (map-zipWith g xs ys)

      zipWith-flip : ∀ xs ys → zipWith f xs ys ≡ zipWith (flip f) ys xs
      zipWith-flip []       []       = refl
      zipWith-flip []       (x ∷ ys) = refl
      zipWith-flip (x ∷ xs) []       = refl
      zipWith-flip (x ∷ xs) (y ∷ ys) = cong (f x y ∷_) (zipWith-flip xs ys)

    module _ (f : A → A → B) where

      zipWith-comm : (∀ x y → f x y ≡ f y x) →
                     ∀ xs ys → zipWith f xs ys ≡ zipWith f ys xs
      zipWith-comm f-comm xs ys = begin
        zipWith f xs ys        ≡⟨ zipWith-flip f xs ys ⟩
        zipWith (flip f) ys xs ≡⟨ zipWith-cong (flip f-comm) ys xs ⟩
        zipWith f ys xs        ∎

    ------------------------------------------------------------------------
    -- zip

    zip-map : ∀ (f : A → B) (g : C → D) →
              ∀ xs ys → zip (map f xs) (map g ys) ≡
                        map (Product.map f g) (zip xs ys)
    zip-map f g xs ys = begin
      zip (map f xs) (map g ys)         ≡⟨ zipWith-map _,_ f g xs ys ⟩
      zipWith (λ x y → f x , g y) xs ys ≡⟨ sym (map-zipWith _,_ (Product.map f g) xs ys) ⟩
      map (Product.map f g) (zip xs ys) ∎

    zip-flip : ∀ (xs : List A) (ys : List B) →
               zip xs ys ≡ map Product.swap (zip ys xs)
    zip-flip xs ys = begin
      zip xs ys                    ≡⟨ zipWith-flip _,_ xs ys ⟩
      zipWith (flip _,_) ys xs     ≡⟨ sym (map-zipWith _,_ Product.swap ys xs) ⟩
      map Product.swap (zip ys xs) ∎

    ------------------------------------------------------------------------
    -- unalignWith

    unalignWith-this : unalignWith ((A → These A B) ∋ this) ≗ (_, [])
    unalignWith-this []       = refl
    unalignWith-this (a ∷ as) = cong (Product.map₁ (a ∷_)) (unalignWith-this as)

    unalignWith-that : unalignWith ((B → These A B) ∋ that) ≗ ([] ,_)
    unalignWith-that []       = refl
    unalignWith-that (b ∷ bs) = cong (Product.map₂ (b ∷_)) (unalignWith-that bs)

    module _ {f g : C → These A B} where

      unalignWith-cong : f ≗ g → unalignWith f ≗ unalignWith g
      unalignWith-cong f≗g []       = refl
      unalignWith-cong f≗g (c ∷ cs) with f c | g c | f≗g c
      ... | this a    | ._ | refl = cong (Product.map₁ (a ∷_)) (unalignWith-cong f≗g cs)
      ... | that b    | ._ | refl = cong (Product.map₂ (b ∷_)) (unalignWith-cong f≗g cs)
      ... | these a b | ._ | refl = cong (Product.map (a ∷_) (b ∷_)) (unalignWith-cong f≗g cs)

    module _ (f : C → These A B) where

      unalignWith-map : (g : D → C) → ∀ ds →
                        unalignWith f (map g ds) ≡ unalignWith (f ∘′ g) ds
      unalignWith-map g []       = refl
      unalignWith-map g (d ∷ ds) with f (g d)
      ... | this a    = cong (Product.map₁ (a ∷_)) (unalignWith-map g ds)
      ... | that b    = cong (Product.map₂ (b ∷_)) (unalignWith-map g ds)
      ... | these a b = cong (Product.map (a ∷_) (b ∷_)) (unalignWith-map g ds)

      map-unalignWith : (g : A → D) (h : B → E) →
        Product.map (map g) (map h) ∘′ unalignWith f ≗ unalignWith (These.map g h ∘′ f)
      map-unalignWith g h []       = refl
      map-unalignWith g h (c ∷ cs) with f c
      ... | this a    = cong (Product.map₁ (g a ∷_)) (map-unalignWith g h cs)
      ... | that b    = cong (Product.map₂ (h b ∷_)) (map-unalignWith g h cs)
      ... | these a b = cong (Product.map (g a ∷_) (h b ∷_)) (map-unalignWith g h cs)

      unalignWith-alignWith : (g : These A B → C) → f ∘′ g ≗ id → ∀ as bs →
                              unalignWith f (alignWith g as bs) ≡ (as , bs)
      unalignWith-alignWith g g∘f≗id []         bs = begin
        unalignWith f (map (g ∘′ that) bs) ≡⟨ unalignWith-map (g ∘′ that) bs ⟩
        unalignWith (f ∘′ g ∘′ that) bs    ≡⟨ unalignWith-cong (g∘f≗id ∘ that) bs ⟩
        unalignWith that bs                ≡⟨ unalignWith-that bs ⟩
        [] , bs                            ∎
      unalignWith-alignWith g g∘f≗id as@(_ ∷ _) [] = begin
        unalignWith f (map (g ∘′ this) as) ≡⟨ unalignWith-map (g ∘′ this) as ⟩
        unalignWith (f ∘′ g ∘′ this) as    ≡⟨ unalignWith-cong (g∘f≗id ∘ this) as ⟩
        unalignWith this as                ≡⟨ unalignWith-this as ⟩
        as , []                            ∎
      unalignWith-alignWith g g∘f≗id (a ∷ as)   (b ∷ bs)
        rewrite g∘f≗id (these a b) =
        cong (Product.map (a ∷_) (b ∷_)) (unalignWith-alignWith g g∘f≗id as bs)

    ------------------------------------------------------------------------
    -- unzipWith

    module _ {f g : A → B × C} where

      unzipWith-cong : f ≗ g → unzipWith f ≗ unzipWith g
      unzipWith-cong f≗g [] = refl
      unzipWith-cong f≗g (x ∷ xs) =
        cong₂ (Product.zip _∷_ _∷_) (f≗g x) (unzipWith-cong f≗g xs)

    module _ (f : A → B × C) where

      length-unzipWith₁ : ∀ xys →
                         length (proj₁ (unzipWith f xys)) ≡ length xys
      length-unzipWith₁ []        = refl
      length-unzipWith₁ (x ∷ xys) = cong suc (length-unzipWith₁ xys)

      length-unzipWith₂ : ∀ xys →
                         length (proj₂ (unzipWith f xys)) ≡ length xys
      length-unzipWith₂ []        = refl
      length-unzipWith₂ (x ∷ xys) = cong suc (length-unzipWith₂ xys)

      zipWith-unzipWith : (g : B → C → A) → uncurry′ g ∘ f ≗ id →
                          uncurry′ (zipWith g) ∘ (unzipWith f)  ≗ id
      zipWith-unzipWith g g∘f≗id []       = refl
      zipWith-unzipWith g g∘f≗id (x ∷ xs) =
        cong₂ _∷_ (g∘f≗id x) (zipWith-unzipWith g g∘f≗id xs)

      unzipWith-zipWith : (g : B → C → A) → f ∘ uncurry′ g ≗ id →
                          ∀ xs ys → length xs ≡ length ys →
                          unzipWith f (zipWith g xs ys) ≡ (xs , ys)
      unzipWith-zipWith g f∘g≗id []       []       l≡l = refl
      unzipWith-zipWith g f∘g≗id (x ∷ xs) (y ∷ ys) l≡l  =
        cong₂ (Product.zip _∷_ _∷_) (f∘g≗id (x , y))
              (unzipWith-zipWith g f∘g≗id xs ys (suc-injective l≡l))

      unzipWith-map : (g : D → A) → unzipWith f ∘ map g ≗ unzipWith (f ∘ g)
      unzipWith-map g []       = refl
      unzipWith-map g (x ∷ xs) =
        cong (Product.zip _∷_ _∷_ (f (g x))) (unzipWith-map g xs)

      map-unzipWith : (g : B → D) (h : C → E) →
                      Product.map (map g) (map h) ∘ unzipWith f ≗
                      unzipWith (Product.map g h ∘ f)
      map-unzipWith g h []       = refl
      map-unzipWith g h (x ∷ xs) =
        cong (Product.zip _∷_ _∷_ _) (map-unzipWith g h xs)

      unzipWith-swap : unzipWith (Product.swap ∘ f) ≗
                       Product.swap ∘ unzipWith f
      unzipWith-swap []       = refl
      unzipWith-swap (x ∷ xs) =
        cong (Product.zip _∷_ _∷_ _) (unzipWith-swap xs)

      unzipWith-++ : ∀ xs ys →
                     unzipWith f (xs ++ ys) ≡
                     Product.zip _++_ _++_ (unzipWith f xs) (unzipWith f ys)
      unzipWith-++ []       ys = refl
      unzipWith-++ (x ∷ xs) ys =
        cong (Product.zip _∷_ _∷_ (f x)) (unzipWith-++ xs ys)

    ------------------------------------------------------------------------
    -- unzip

    unzip-map : ∀ (f : A → B) (g : C → D) →
                unzip ∘ map (Product.map f g) ≗
                Product.map (map f) (map g) ∘ unzip
    unzip-map f g xs = begin
      unzip (map (Product.map f g) xs)       ≡⟨ unzipWith-map id (Product.map f g) xs ⟩
      unzipWith (Product.map f g) xs         ≡⟨ sym (map-unzipWith id f g xs) ⟩
      Product.map (map f) (map g) (unzip xs) ∎

    unzip-swap : unzip ∘ map Product.swap ≗ Product.swap ∘ unzip {A = A} {B = B}
    unzip-swap xs = begin
      unzip (map Product.swap xs) ≡⟨ unzipWith-map id Product.swap xs ⟩
      unzipWith Product.swap xs   ≡⟨ unzipWith-swap id xs ⟩
      Product.swap (unzip xs)     ∎

    zip-unzip : uncurry′ zip ∘ unzip ≗ id {A = List (A × B)}
    zip-unzip = zipWith-unzipWith id _,_ λ _ → refl

    unzip-zip : ∀ (xs : List A) (ys : List B) →
                length xs ≡ length ys → unzip (zip xs ys) ≡ (xs , ys)
    unzip-zip = unzipWith-zipWith id _,_ λ _ → refl

    ------------------------------------------------------------------------
    -- foldr

    foldr-universal : ∀ (h : List A → B) f e → (h [] ≡ e) →
                      (∀ x xs → h (x ∷ xs) ≡ f x (h xs)) →
                      h ≗ foldr f e
    foldr-universal h f e base step []       = base
    foldr-universal h f e base step (x ∷ xs) = begin
      h (x ∷ xs)          ≡⟨ step x xs ⟩
      f x (h xs)          ≡⟨ cong (f x) (foldr-universal h f e base step xs) ⟩
      f x (foldr f e xs)  ∎

    foldr-cong : ∀ {f g : A → B → B} {d e : B} →
                 (∀ x y → f x y ≡ g x y) → d ≡ e →
                 foldr f d ≗ foldr g e
    foldr-cong f≗g refl []      = refl
    foldr-cong f≗g d≡e (x ∷ xs) rewrite foldr-cong f≗g d≡e xs = f≗g x _

    foldr-fusion : ∀ (h : B → C) {f : A → B → B} {g : A → C → C} (e : B) →
                   (∀ x y → h (f x y) ≡ g x (h y)) →
                   h ∘ foldr f e ≗ foldr g (h e)
    foldr-fusion h {f} {g} e fuse =
      foldr-universal (h ∘ foldr f e) g (h e) refl
                      (λ x xs → fuse x (foldr f e xs))

    id-is-foldr : id {A = List A} ≗ foldr _∷_ []
    id-is-foldr = foldr-universal id _∷_ [] refl (λ _ _ → refl)

    ++-is-foldr : (xs ys : List A) → xs ++ ys ≡ foldr _∷_ ys xs
    ++-is-foldr xs ys = begin
      xs ++ ys                ≡⟨ cong (_++ ys) (id-is-foldr xs) ⟩
      foldr _∷_ [] xs ++ ys   ≡⟨ foldr-fusion (_++ ys) [] (λ _ _ → refl) xs ⟩
      foldr _∷_ ([] ++ ys) xs ≡⟨⟩
      foldr _∷_ ys xs         ∎

    foldr-++ : ∀ (f : A → B → B) x ys zs →
               foldr f x (ys ++ zs) ≡ foldr f (foldr f x zs) ys
    foldr-++ f x []       zs = refl
    foldr-++ f x (y ∷ ys) zs = cong (f y) (foldr-++ f x ys zs)

    map-is-foldr : {f : A → B} → map f ≗ foldr (λ x ys → f x ∷ ys) []
    map-is-foldr {f = f} xs = begin
      map f xs                        ≡⟨ cong (map f) (id-is-foldr xs) ⟩
      map f (foldr _∷_ [] xs)         ≡⟨ foldr-fusion (map f) [] (λ _ _ → refl) xs ⟩
      foldr (λ x ys → f x ∷ ys) [] xs ∎

    foldr-∷ʳ : ∀ (f : A → B → B) x y ys →
               foldr f x (ys ∷ʳ y) ≡ foldr f (f y x) ys
    foldr-∷ʳ f x y []       = refl
    foldr-∷ʳ f x y (z ∷ ys) = cong (f z) (foldr-∷ʳ f x y ys)

    foldr-map : ∀ (f : A → B → B) (g : C → A) x xs → foldr f x (map g xs) ≡ foldr (g -⟨ f ∣) x xs
    foldr-map f g x []       = refl
    foldr-map f g x (y ∷ xs) = cong (f (g y)) (foldr-map f g x xs)

    -- Interaction with predicates

    module _ {P : Pred A p} {f : A → A → A} where

      foldr-forcesᵇ : (∀ x y → P (f x y) → P x × P y) →
                      ∀ e xs → P (foldr f e xs) → All P xs
      foldr-forcesᵇ _      _ []       _     = []
      foldr-forcesᵇ forces _ (x ∷ xs) Pfold =
        let px , pfxs = forces _ _ Pfold in px ∷ foldr-forcesᵇ forces _ xs pfxs

      foldr-preservesᵇ : (∀ {x y} → P x → P y → P (f x y)) →
                         ∀ {e xs} → P e → All P xs → P (foldr f e xs)
      foldr-preservesᵇ _    Pe []         = Pe
      foldr-preservesᵇ pres Pe (px ∷ pxs) = pres px (foldr-preservesᵇ pres Pe pxs)

      foldr-preservesʳ : (∀ x {y} → P y → P (f x y)) →
                         ∀ {e} → P e → ∀ xs → P (foldr f e xs)
      foldr-preservesʳ pres Pe []       = Pe
      foldr-preservesʳ pres Pe (_ ∷ xs) = pres _ (foldr-preservesʳ pres Pe xs)

      foldr-preservesᵒ : (∀ x y → P x ⊎ P y → P (f x y)) →
                         ∀ e xs → P e ⊎ Any P xs → P (foldr f e xs)
      foldr-preservesᵒ pres e []       (inj₁ Pe)          = Pe
      foldr-preservesᵒ pres e (x ∷ xs) (inj₁ Pe)          =
        pres _ _ (inj₂ (foldr-preservesᵒ pres e xs (inj₁ Pe)))
      foldr-preservesᵒ pres e (x ∷ xs) (inj₂ (here px))   = pres _ _ (inj₁ px)
      foldr-preservesᵒ pres e (x ∷ xs) (inj₂ (there pxs)) =
        pres _ _ (inj₂ (foldr-preservesᵒ pres e xs (inj₂ pxs)))

    ------------------------------------------------------------------------
    -- foldl

    foldl-cong : ∀ {f g : B → A → B} → (∀ x y → f x y ≡ g x y) →
                 ∀ x → foldl f x ≗ foldl g x
    foldl-cong f≗g x []       = refl
    foldl-cong f≗g x (y ∷ xs) rewrite f≗g x y = foldl-cong f≗g _ xs

    foldl-++ : ∀ (f : A → B → A) x ys zs →
               foldl f x (ys ++ zs) ≡ foldl f (foldl f x ys) zs
    foldl-++ f x []       zs = refl
    foldl-++ f x (y ∷ ys) zs = foldl-++ f (f x y) ys zs

    foldl-∷ʳ : ∀ (f : A → B → A) x y ys →
               foldl f x (ys ∷ʳ y) ≡ f (foldl f x ys) y
    foldl-∷ʳ f x y []       = refl
    foldl-∷ʳ f x y (z ∷ ys) = foldl-∷ʳ f (f x z) y ys

    foldl-map : ∀ (f : A → B → A) (g : C → B) x xs → foldl f x (map g xs) ≡ foldl (∣ f ⟩- g) x xs
    foldl-map f g x []       = refl
    foldl-map f g x (y ∷ xs) = foldl-map f g (f x (g y)) xs

    ------------------------------------------------------------------------
    -- concat

    concat-map : ∀ {f : A → B} → concat ∘ map (map f) ≗ map f ∘ concat
    concat-map {f = f} xss = begin
      concat (map (map f) xss)                   ≡⟨ cong concat (map-is-foldr xss) ⟩
      concat (foldr (λ xs → map f xs ∷_) [] xss) ≡⟨ foldr-fusion concat [] (λ _ _ → refl) xss ⟩
      foldr (λ ys → map f ys ++_) [] xss         ≡⟨ sym (foldr-fusion (map f) [] (map-++ f) xss) ⟩
      map f (concat xss)                         ∎

    concat-++ : (xss yss : List (List A)) → concat xss ++ concat yss ≡ concat (xss ++ yss)
    concat-++ [] yss = refl
    concat-++ ([] ∷ xss) yss = concat-++ xss yss
    concat-++ ((x ∷ xs) ∷ xss) yss = cong (x ∷_) (concat-++ (xs ∷ xss) yss)

    concat-concat : concat {A = A} ∘ map concat ≗ concat ∘ concat
    concat-concat [] = refl
    concat-concat (xss ∷ xsss) = begin
      concat (map concat (xss ∷ xsss))   ≡⟨ cong (concat xss ++_) (concat-concat xsss) ⟩
      concat xss ++ concat (concat xsss) ≡⟨ concat-++ xss (concat xsss) ⟩
      concat (concat (xss ∷ xsss))       ∎

    concat-map-[_] : concat {A = A} ∘ map [_] ≗ id
    concat-map-[ [] ]     = refl
    concat-map-[ x ∷ xs ] = cong (x ∷_) (concat-map-[ xs ])

    concat-[_] : concat {A = A} ∘ [_] ≗ id
    concat-[ xs ] = ++-identityʳ xs

    ------------------------------------------------------------------------
    -- concatMap

    concatMap-cong : ∀ {f g : A → List B} → f ≗ g → concatMap f ≗ concatMap g
    concatMap-cong eq = cong concat ∘ map-cong eq

    concatMap-pure : concatMap {A = A} [_] ≗ id
    concatMap-pure = concat-map-[_]

    concatMap-map : (g : B → List C) → (f : A → B) →
                    concatMap g ∘′ (map f) ≗ concatMap (g ∘′ f)
    concatMap-map g f = cong concat ∘ sym ∘ map-∘

    map-concatMap : (f : B → C) (g : A → List B) →
                    map f ∘′ concatMap g ≗ concatMap (map f ∘′ g)
    map-concatMap f g xs = begin
      map f (concatMap g xs)
        ≡⟨⟩
      map f (concat (map g xs))
        ≡⟨ concat-map (map g xs) ⟨
      concat (map (map f) (map g xs))
        ≡⟨ concatMap-map (map f) g xs ⟩
      concat (map (map f ∘′ g) xs)
        ≡⟨⟩
      concatMap (map f ∘′ g) xs
        ∎

    concatMap-++ : ∀ (f : A → List B) xs ys →
                   concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys
    concatMap-++ f xs ys = begin
      concatMap f (xs ++ ys)           ≡⟨⟩
      concat (map f (xs ++ ys))        ≡⟨ cong concat $ map-++ f xs ys ⟩
      concat (map f xs ++ map f ys)    ≡⟨ concat-++ (map f xs) (map f ys) ⟨
      concatMap f xs ++ concatMap f ys ∎ where open ≡-Reasoning

    ------------------------------------------------------------------------
    -- 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

    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

    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
    mapMaybe-just (x ∷ xs) = cong (x ∷_) (mapMaybe-just xs)

    mapMaybe-nothing : (xs : List A) →
                       mapMaybe {B = B} (λ _ → nothing) xs ≡ []
    mapMaybe-nothing []       = refl
    mapMaybe-nothing (x ∷ xs) = mapMaybe-nothing xs

    module _ (f : A → Maybe B) where

      mapMaybe-concatMap : mapMaybe f ≗ concatMap (fromMaybe ∘ f)
      mapMaybe-concatMap xs = begin
        catMaybes (map f xs)            ≡⟨ catMaybes-concatMap (map f xs) ⟩
        concatMap fromMaybe (map f xs)  ≡⟨ concatMap-map fromMaybe f xs ⟩
        concatMap (fromMaybe ∘ f) xs    ∎

      length-mapMaybe : ∀ xs → length (mapMaybe f xs) ≤ length xs
      length-mapMaybe xs = ≤-begin
        length (mapMaybe f xs)      ≤⟨ length-catMaybes (map f xs) ⟩
        length (map f xs)           ≤⟨ ≤-reflexive (length-map f xs) ⟩
        length xs                   ≤-∎
        where open ≤-Reasoning renaming (begin_ to ≤-begin_; _∎ to _≤-∎)

      mapMaybe-++ : ∀ xs ys →
                    mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys
      mapMaybe-++ xs ys = begin
        catMaybes (map f (xs ++ ys))     ≡⟨ cong catMaybes (map-++ f xs ys) ⟩
        catMaybes (map f xs ++ map f ys) ≡⟨ catMaybes-++ (map f xs) (map f ys) ⟩
        mapMaybe f xs ++ mapMaybe f ys   ∎

    module _ (f : B → Maybe C) (g : A → B) where

      mapMaybe-map : mapMaybe f ∘ map g ≗ mapMaybe (f ∘ g)
      mapMaybe-map = cong catMaybes ∘ sym ∘ map-∘

    module _ (g : B → C) (f : A → Maybe B) where

      map-mapMaybe : map g ∘ mapMaybe f ≗ mapMaybe (Maybe.map g ∘ f)
      map-mapMaybe xs = begin
        map g (catMaybes (map f xs))       ≡⟨ map-catMaybes g (map f xs) ⟩
        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

    ------------------------------------------------------------------------
    -- applyUpTo

    length-applyUpTo : ∀ (f : ℕ → A) n → length (applyUpTo f n) ≡ n
    length-applyUpTo f zero    = refl
    length-applyUpTo f (suc n) = cong suc (length-applyUpTo (f ∘ suc) n)

    lookup-applyUpTo : ∀ (f : ℕ → A) n i → lookup (applyUpTo f n) i ≡ f (toℕ i)
    lookup-applyUpTo f (suc n) zero    = refl
    lookup-applyUpTo f (suc n) (suc i) = lookup-applyUpTo (f ∘ suc) n i

    applyUpTo-∷ʳ : ∀ (f : ℕ → A) n → applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)
    applyUpTo-∷ʳ f zero = refl
    applyUpTo-∷ʳ f (suc n) = cong (f 0 ∷_) (applyUpTo-∷ʳ (f ∘ suc) n)

    map-applyUpTo : ∀ (f : ℕ → A) (g : A → B) n → map g (applyUpTo f n) ≡ applyUpTo (g ∘ f) n
    map-applyUpTo f g zero = refl
    map-applyUpTo f g (suc n) = cong (g (f 0) ∷_) (map-applyUpTo (f ∘ suc) g n)

    ------------------------------------------------------------------------
    -- applyDownFrom

    module _ (f : ℕ → A) where

      length-applyDownFrom : ∀ n → length (applyDownFrom f n) ≡ n
      length-applyDownFrom zero    = refl
      length-applyDownFrom (suc n) = cong suc (length-applyDownFrom n)

      lookup-applyDownFrom : ∀ n i → lookup (applyDownFrom f n) i ≡ f (n ∸ (suc (toℕ i)))
      lookup-applyDownFrom (suc n) zero    = refl
      lookup-applyDownFrom (suc n) (suc i) = lookup-applyDownFrom n i

      applyDownFrom-∷ʳ : ∀ n → applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n)
      applyDownFrom-∷ʳ zero = refl
      applyDownFrom-∷ʳ (suc n) = cong (f (suc n) ∷_) (applyDownFrom-∷ʳ n)

      map-applyDownFrom : ∀ (g : A → B) n → map g (applyDownFrom f n) ≡ applyDownFrom (g ∘ f) n
      map-applyDownFrom g zero = refl
      map-applyDownFrom g (suc n) = cong (g (f n) ∷_) (map-applyDownFrom g n)

    ------------------------------------------------------------------------
    -- upTo

    length-upTo : ∀ n → length (upTo n) ≡ n
    length-upTo = length-applyUpTo id

    lookup-upTo : ∀ n i → lookup (upTo n) i ≡ toℕ i
    lookup-upTo = lookup-applyUpTo id

    upTo-∷ʳ : ∀ n → upTo n ∷ʳ n ≡ upTo (suc n)
    upTo-∷ʳ = applyUpTo-∷ʳ id

    map-upTo : ∀ (f : ℕ → A) n → map f (upTo n) ≡ applyUpTo f n
    map-upTo = map-applyUpTo id

    ------------------------------------------------------------------------
    -- downFrom

    length-downFrom : ∀ n → length (downFrom n) ≡ n
    length-downFrom = length-applyDownFrom id

    lookup-downFrom : ∀ n i → lookup (downFrom n) i ≡ n ∸ (suc (toℕ i))
    lookup-downFrom = lookup-applyDownFrom id

    downFrom-∷ʳ : ∀ n → applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n)
    downFrom-∷ʳ = applyDownFrom-∷ʳ id

    map-downFrom : ∀ (f : ℕ → A) n → map f (downFrom n) ≡ applyDownFrom f n
    map-downFrom = map-applyDownFrom id

    ------------------------------------------------------------------------
    -- tabulate

    tabulate-cong : ∀ {n} {f g : Fin n → A} →
                    f ≗ g → tabulate f ≡ tabulate g
    tabulate-cong {n = zero}  p = refl
    tabulate-cong {n = suc n} p = cong₂ _∷_ (p zero) (tabulate-cong (p ∘ suc))

    tabulate-lookup : ∀ (xs : List A) → tabulate (lookup xs) ≡ xs
    tabulate-lookup []       = refl
    tabulate-lookup (x ∷ xs) = cong (_ ∷_) (tabulate-lookup xs)

    length-tabulate : ∀ {n} → (f : Fin n → A) →
                      length (tabulate f) ≡ n
    length-tabulate {n = zero} f = refl
    length-tabulate {n = suc n} f = cong suc (length-tabulate (λ z → f (suc z)))

    lookup-tabulate : ∀ {n} → (f : Fin n → A) →
                      ∀ i → let i′ = cast (sym (length-tabulate f)) i
                            in lookup (tabulate f) i′ ≡ f i
    lookup-tabulate f zero    = refl
    lookup-tabulate f (suc i) = lookup-tabulate (f ∘ suc) i

    map-tabulate : ∀ {n} (g : Fin n → A) (f : A → B) →
                   map f (tabulate g) ≡ tabulate (f ∘ g)
    map-tabulate {n = zero}  g f = refl
    map-tabulate {n = suc n} g f = cong (_ ∷_) (map-tabulate (g ∘ suc) f)

    ------------------------------------------------------------------------
    -- _[_]%=_

    length-%= : ∀ xs k (f : A → A) → length (xs [ k ]%= f) ≡ length xs
    length-%= (x ∷ xs) zero    f = refl
    length-%= (x ∷ xs) (suc k) f = cong suc (length-%= xs k f)

    ------------------------------------------------------------------------
    -- _[_]∷=_

    length-∷= : ∀ xs k (v : A) → length (xs [ k ]∷= v) ≡ length xs
    length-∷= xs k v = length-%= xs k (const v)

    map-∷= : ∀ xs k (v : A) (f : A → B) →
             let eq = sym (length-map f xs) in
             map f (xs [ k ]∷= v) ≡ map f xs [ cast eq k ]∷= f v
    map-∷= (x ∷ xs) zero    v f = refl
    map-∷= (x ∷ xs) (suc k) v f = cong (f x ∷_) (map-∷= xs k v f)

    ------------------------------------------------------------------------
    -- insertAt

    length-insertAt : ∀ (xs : List A) (i : Fin (suc (length xs))) v →
                      length (insertAt xs i v) ≡ suc (length xs)
    length-insertAt xs       zero    v = refl
    length-insertAt (x ∷ xs) (suc i) v = cong suc (length-insertAt xs i v)

    ------------------------------------------------------------------------
    -- removeAt

    length-removeAt : ∀ (xs : List A) k → length (removeAt xs k) ≡ pred (length xs)
    length-removeAt (x ∷ xs) zero            = refl
    length-removeAt (x ∷ xs@(_ ∷ _)) (suc k) = cong suc (length-removeAt xs k)

    length-removeAt′ : ∀ (xs : List A) k → length xs ≡ suc (length (removeAt xs k))
    length-removeAt′ xs@(_ ∷ _) k rewrite length-removeAt xs k = refl

    map-removeAt : ∀ xs k (f : A → B) →
                let eq = sym (length-map f xs) in
                map f (removeAt xs k) ≡ removeAt (map f xs) (cast eq k)
    map-removeAt (x ∷ xs) zero    f = refl
    map-removeAt (x ∷ xs) (suc k) f = cong (f x ∷_) (map-removeAt xs k f)

    ------------------------------------------------------------------------
     -- insertAt and removeAt

    removeAt-insertAt : ∀ (xs : List A) (i : Fin (suc (length xs))) v →
      removeAt (insertAt xs i v) ((cast (sym (length-insertAt xs i v)) i)) ≡ xs
    removeAt-insertAt xs       zero    v = refl
    removeAt-insertAt (x ∷ xs) (suc i) v = cong (_ ∷_) (removeAt-insertAt xs i v)

    insertAt-removeAt : (xs : List A) (i : Fin (length xs)) →
      insertAt (removeAt xs i) (cast (length-removeAt′ xs i) i) (lookup xs i) ≡ xs
    insertAt-removeAt (x ∷ xs) zero    = refl
    insertAt-removeAt (x ∷ xs) (suc i) = cong (x ∷_) (insertAt-removeAt xs i)

    ------------------------------------------------------------------------
    -- take

    length-take : ∀ n (xs : List A) → length (take n xs) ≡ n ⊓ (length xs)
    length-take zero    xs       = refl
    length-take (suc n) []       = refl
    length-take (suc n) (x ∷ xs) = cong suc (length-take n xs)

    -- Take commutes with map.
    take-map : ∀ {f : A → B} (n : ℕ) xs → take n (map f xs) ≡ map f (take n xs)
    take-map zero xs = refl
    take-map (suc s) [] = refl
    take-map (suc s) (a ∷ xs) = cong (_ ∷_) (take-map s xs)

    take-suc : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in
               take (suc m) xs ≡ take m xs ∷ʳ lookup xs i
    take-suc (x ∷ xs) zero    = refl
    take-suc (x ∷ xs) (suc i) = cong (x ∷_) (take-suc xs i)

    take-suc-tabulate : ∀ {n} (f : Fin n → A) (i : Fin n) → let m = toℕ i in
                        take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f i
    take-suc-tabulate f i rewrite sym (toℕ-cast (sym (length-tabulate f)) i) | sym (lookup-tabulate f i)
      = take-suc (tabulate f) (cast _ i)

    -- If you take at least as many elements from a list as it has, you get
    -- the whole list.
    take-all : (n : ℕ) (xs : List A) → n ≥ length xs → take n xs ≡ xs
    take-all zero [] _ = refl
    take-all (suc _) [] _ = refl
    take-all (suc n) (x ∷ xs) (s≤s pf) = cong (x ∷_) (take-all n xs pf)

    -- Taking from an empty list does nothing.
    take-[] : ∀ m → take {A = A} m [] ≡ []
    take-[] zero = refl
    take-[] (suc m) = refl

    -- Taking twice takes the minimum of both counts.
    take-take : ∀ n m (xs : List A) → take n (take m xs) ≡ take (n ⊓ m) xs
    take-take zero    m       xs       = refl
    take-take (suc n) zero    xs       = refl
    take-take (suc n) (suc m) []       = refl
    take-take (suc n) (suc m) (x ∷ xs) = cong (x ∷_) (take-take n m xs)

    -- Dropping m elements and then taking n is the same as
    -- taking n + m elements and then dropping m.
    take-drop : ∀ n m (xs : List A) →
                take n (drop m xs) ≡ drop m (take (m + n) xs)
    take-drop n zero    xs       = refl
    take-drop n (suc m) []       = take-[] n
    take-drop n (suc m) (x ∷ xs) = take-drop n m xs

    ------------------------------------------------------------------------
    -- drop

    length-drop : ∀ n (xs : List A) → length (drop n xs) ≡ length xs ∸ n
    length-drop zero    xs       = refl
    length-drop (suc n) []       = refl
    length-drop (suc n) (x ∷ xs) = length-drop n xs

    -- Drop commutes with map.
    drop-map : ∀ {f : A → B} (n : ℕ) xs → drop n (map f xs) ≡ map f (drop n xs)
    drop-map zero xs = refl
    drop-map (suc n) [] = refl
    drop-map (suc n) (a ∷ xs) = drop-map n xs

    -- Dropping from an empty list does nothing.
    drop-[] : ∀ m → drop {A = A} m [] ≡ []
    drop-[] zero = refl
    drop-[] (suc m) = refl

    take++drop≡id : ∀ n (xs : List A) → take n xs ++ drop n xs ≡ xs
    take++drop≡id zero    xs       = refl
    take++drop≡id (suc n) []       = refl
    take++drop≡id (suc n) (x ∷ xs) = cong (x ∷_) (take++drop≡id n xs)

    drop-take-suc : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in
               drop m (take (suc m) xs) ≡ [ lookup xs i ]
    drop-take-suc (x ∷ xs) zero    = refl
    drop-take-suc (x ∷ xs) (suc i) = drop-take-suc xs i

    drop-take-suc-tabulate : ∀ {n} (f : Fin n → A) (i : Fin n) → let m = toℕ i in
                      drop m (take (suc m) (tabulate f)) ≡ [ f i ]
    drop-take-suc-tabulate f i rewrite sym (toℕ-cast (sym (length-tabulate f)) i) | sym (lookup-tabulate f i)
      = drop-take-suc (tabulate f) (cast _ i)

    -- Dropping m elements and then n elements is same as dropping m+n elements
    drop-drop : (m n : ℕ) → (xs : List A) → drop n (drop m xs) ≡ drop (m + n) xs
    drop-drop zero n xs = refl
    drop-drop (suc m) n [] = drop-[] n
    drop-drop (suc m) n (x ∷ xs) = drop-drop m n xs

    drop-all : (n : ℕ) (xs : List A) → n ≥ length xs → drop n xs ≡ []
    drop-all n       []       _ = drop-[] n
    drop-all (suc n) (x ∷ xs) p = drop-all n xs (s≤s⁻¹ p)

    ------------------------------------------------------------------------
    -- replicate

    length-replicate : ∀ n {x : A} → length (replicate n x) ≡ n
    length-replicate zero    = refl
    length-replicate (suc n) = cong suc (length-replicate n)

    lookup-replicate : ∀ n (x : A) (i : Fin n) →
                       lookup (replicate n x) (cast (sym (length-replicate n)) i) ≡ x
    lookup-replicate (suc n) x zero    = refl
    lookup-replicate (suc n) x (suc i) = lookup-replicate n x i

    map-replicate :  ∀ (f : A → B) n (x : A) →
                     map f (replicate n x) ≡ replicate n (f x)
    map-replicate f zero    x = refl
    map-replicate f (suc n) x = cong (_ ∷_) (map-replicate f n x)

    zipWith-replicate : ∀ n (_⊕_ : A → B → C) (x : A) (y : B) →
                        zipWith _⊕_ (replicate n x) (replicate n y) ≡ replicate n (x ⊕ y)
    zipWith-replicate zero    _⊕_ x y = refl
    zipWith-replicate (suc n) _⊕_ x y = cong (x ⊕ y ∷_) (zipWith-replicate n _⊕_ x y)

    ------------------------------------------------------------------------
    -- iterate

    length-iterate : ∀ f (x : A) n → length (iterate f x n) ≡ n
    length-iterate f x zero    = refl
    length-iterate f x (suc n) = cong suc (length-iterate f (f x) n)

    iterate-id : ∀ (x : A) n → iterate id x n ≡ replicate n x
    iterate-id x zero    = refl
    iterate-id x (suc n) = cong (_ ∷_) (iterate-id x n)

    lookup-iterate : ∀ f (x : A) n (i : Fin n) →
      lookup (iterate f x n) (cast (sym (length-iterate f x n)) i) ≡ ℕ.iterate f x (toℕ i)
    lookup-iterate f x (suc n) zero    = refl
    lookup-iterate f x (suc n) (suc i) = lookup-iterate f (f x) n i

    ------------------------------------------------------------------------
    -- splitAt

    splitAt-defn : ∀ n → splitAt {A = A} n ≗ < take n , drop n >
    splitAt-defn zero    xs       = refl
    splitAt-defn (suc n) []       = refl
    splitAt-defn (suc n) (x ∷ xs) = cong (Product.map (x ∷_) id) (splitAt-defn n xs)

    module _ (f : A → B) where

      splitAt-map : ∀ n → splitAt n ∘ map f ≗
                          Product.map (map f) (map f) ∘ splitAt n
      splitAt-map zero    xs       = refl
      splitAt-map (suc n) []       = refl
      splitAt-map (suc n) (x ∷ xs) =
        cong (Product.map₁ (f x ∷_)) (splitAt-map n xs)

    ------------------------------------------------------------------------
    -- takeWhile, dropWhile, and span

    module _ {P : Pred A p} (P? : Decidable P) where

      takeWhile++dropWhile : ∀ xs → takeWhile P? xs ++ dropWhile P? xs ≡ xs
      takeWhile++dropWhile []       = refl
      takeWhile++dropWhile (x ∷ xs) with does (P? x)
      ... | true  = cong (x ∷_) (takeWhile++dropWhile xs)
      ... | false = refl

      span-defn : span P? ≗ < takeWhile P? , dropWhile P? >
      span-defn []       = refl
      span-defn (x ∷ xs) with does (P? x)
      ... | true  = cong (Product.map (x ∷_) id) (span-defn xs)
      ... | false = refl

    ------------------------------------------------------------------------
    -- filter

    module _ {P : Pred A p} (P? : Decidable P) where

      length-filter : ∀ xs → length (filter P? xs) ≤ length xs
      length-filter []       = z≤n
      length-filter (x ∷ xs) with ih ← length-filter xs | does (P? x)
      ... | false = m≤n⇒m≤1+n ih
      ... | true  = s≤s ih

      filter-all : ∀ {xs} → All P xs → filter P? xs ≡ xs
      filter-all {[]}     []         = refl
      filter-all {x ∷ xs} (px ∷ pxs) with P? x
      ... | no          ¬px = contradiction px ¬px
      ... | true  because _ = cong (x ∷_) (filter-all pxs)

      filter-notAll : ∀ xs → Any (∁ P) xs → length (filter P? xs) < length xs
      filter-notAll (x ∷ xs) (here ¬px) with P? x
      ... | false because _ = s≤s (length-filter xs)
      ... | yes          px = contradiction px ¬px
      filter-notAll (x ∷ xs) (there any) with ih ← filter-notAll xs any | does (P? x)
      ... | false = m≤n⇒m≤1+n ih
      ... | true  = s≤s ih

      filter-some : ∀ {xs} → Any P xs → 0 < length (filter P? xs)
      filter-some {x ∷ xs} (here px)   with P? x
      ... | true because _ = z<s
      ... | no         ¬px = contradiction px ¬px
      filter-some {x ∷ xs} (there pxs) with does (P? x)
      ... | true  = m≤n⇒m≤1+n (filter-some pxs)
      ... | false = filter-some pxs

      filter-none : ∀ {xs} → All (∁ P) xs → filter P? xs ≡ []
      filter-none {[]}     []           = refl
      filter-none {x ∷ xs} (¬px ∷ ¬pxs) with P? x
      ... | false because _ = filter-none ¬pxs
      ... | yes          px = contradiction px ¬px

      filter-complete : ∀ {xs} → length (filter P? xs) ≡ length xs →
                        filter P? xs ≡ xs
      filter-complete {[]}     eq = refl
      filter-complete {x ∷ xs} eq with does (P? x)
      ... | false = contradiction eq (<⇒≢ (s≤s (length-filter xs)))
      ... | true  = cong (x ∷_) (filter-complete (suc-injective eq))

      filter-accept : ∀ {x xs} → P x → filter P? (x ∷ xs) ≡ x ∷ (filter P? xs)
      filter-accept {x} Px with P? x
      ... | true because _ = refl
      ... | no         ¬Px = contradiction Px ¬Px

      filter-reject : ∀ {x xs} → ¬ P x → filter P? (x ∷ xs) ≡ filter P? xs
      filter-reject {x} ¬Px with P? x
      ... | yes          Px = contradiction Px ¬Px
      ... | false because _ = refl

      filter-idem : filter P? ∘ filter P? ≗ filter P?
      filter-idem []       = refl
      filter-idem (x ∷ xs) with does (P? x) in eq
      ... | false            = filter-idem xs
      ... | true  rewrite eq = cong (x ∷_) (filter-idem xs)

      filter-++ : ∀ xs ys → filter P? (xs ++ ys) ≡ filter P? xs ++ filter P? ys
      filter-++ []       ys = refl
      filter-++ (x ∷ xs) ys with ih ← filter-++ xs ys | does (P? x)
      ... | true  = cong (x ∷_) ih
      ... | false = ih

    module _ {P : Pred A p} {Q : Pred A q} (P? : Decidable P) (Q? : Decidable Q) where

      filter-≐ : P ≐ Q → filter P? ≗ filter Q?
      filter-≐ P≐Q [] = refl
      filter-≐ P≐Q (x ∷ xs) with P? x
      ... | yes P[x] = trans (cong (x ∷_) (filter-≐ P≐Q xs)) (sym (filter-accept Q? (proj₁ P≐Q P[x])))
      ... | no ¬P[x] = trans (filter-≐ P≐Q xs) (sym (filter-reject Q? (¬P[x] ∘ proj₂ P≐Q)))

    ------------------------------------------------------------------------
    -- derun and deduplicate

    module _ {R : Rel A p} (R? : B.Decidable R) where

      length-derun : ∀ xs → length (derun R? xs) ≤ length xs
      length-derun [] = ≤-refl
      length-derun (x ∷ []) = ≤-refl
      length-derun (x ∷ y ∷ xs) with ih ← length-derun (y ∷ xs) | does (R? x y)
      ... | true  = m≤n⇒m≤1+n ih
      ... | false = s≤s ih

      length-deduplicate : ∀ xs → length (deduplicate R? xs) ≤ length xs
      length-deduplicate [] = z≤n
      length-deduplicate (x ∷ xs) = ≤-begin
        1 + length (filter (¬? ∘ R? x) r) ≤⟨ s≤s (length-filter (¬? ∘ R? x) r) ⟩
        1 + length r                      ≤⟨ s≤s (length-deduplicate xs) ⟩
        1 + length xs                     ≤-∎
        where
        open ≤-Reasoning renaming (begin_ to ≤-begin_; _∎ to _≤-∎)
        r = deduplicate R? xs

      derun-reject : ∀ {x y} xs → R x y → derun R? (x ∷ y ∷ xs) ≡ derun R? (y ∷ xs)
      derun-reject {x} {y} xs Rxy with R? x y
      ... | yes _    = refl
      ... | no  ¬Rxy = contradiction Rxy ¬Rxy

      derun-accept : ∀ {x y} xs → ¬ R x y → derun R? (x ∷ y ∷ xs) ≡ x ∷ derun R? (y ∷ xs)
      derun-accept {x} {y} xs ¬Rxy with R? x y
      ... | yes Rxy = contradiction Rxy ¬Rxy
      ... | no  _   = refl

    ------------------------------------------------------------------------
    -- partition

    module _ {P : Pred A p} (P? : Decidable P) where

      partition-defn : partition P? ≗ < filter P? , filter (∁? P?) >
      partition-defn []       = refl
      partition-defn (x ∷ xs) with ih ← partition-defn xs | does (P? x)
      ...  | true  = cong (Product.map (x ∷_) id) ih
      ...  | false = cong (Product.map id (x ∷_)) ih

      length-partition : ∀ xs → (let (ys , zs) = partition P? xs) →
                         length ys ≤ length xs × length zs ≤ length xs
      length-partition []       = z≤n , z≤n
      length-partition (x ∷ xs) with ih ← length-partition xs | does (P? x)
      ...  | true  = Product.map s≤s m≤n⇒m≤1+n ih
      ...  | false = Product.map m≤n⇒m≤1+n s≤s ih

      partition-is-foldr : partition P? ≗ foldr
        (λ x → if does (P? x) then Product.map₁ (x ∷_) else Product.map₂ (x ∷_))
        ([] , [])
      partition-is-foldr [] = refl
      partition-is-foldr (x ∷ xs) with ih ← partition-is-foldr xs | does (P? x)
      ... | true =  cong (Product.map₁ (x ∷_)) ih
      ... | false = cong (Product.map₂ (x ∷_)) ih

    ------------------------------------------------------------------------
    -- _ʳ++_

    ʳ++-defn : ∀ (xs : List A) {ys} → xs ʳ++ ys ≡ reverse xs ++ ys
    ʳ++-defn [] = refl
    ʳ++-defn (x ∷ xs) {ys} = begin
      (x ∷ xs)             ʳ++ ys   ≡⟨⟩
      xs         ʳ++   x     ∷ ys   ≡⟨⟩
      xs         ʳ++ [ x ]  ++ ys   ≡⟨ ʳ++-defn xs  ⟩
      reverse xs  ++ [ x ]  ++ ys   ≡⟨ sym (++-assoc (reverse xs) _ _) ⟩
      (reverse xs ++ [ x ]) ++ ys   ≡⟨ cong (_++ ys) (sym (ʳ++-defn xs)) ⟩
      (xs ʳ++ [ x ])        ++ ys   ≡⟨⟩
      reverse (x ∷ xs)      ++ ys   ∎

    -- Reverse-append of append is reverse-append after reverse-append.

    ++-ʳ++ : ∀ (xs {ys zs} : List A) → (xs ++ ys) ʳ++ zs ≡ ys ʳ++ xs ʳ++ zs
    ++-ʳ++ [] = refl
    ++-ʳ++ (x ∷ xs) {ys} {zs} = begin
      (x ∷ xs ++ ys) ʳ++ zs   ≡⟨⟩
      (xs ++ ys) ʳ++ x ∷ zs   ≡⟨ ++-ʳ++ xs ⟩
      ys ʳ++ xs ʳ++ x ∷ zs    ≡⟨⟩
      ys ʳ++ (x ∷ xs) ʳ++ zs  ∎

    -- Reverse-append of reverse-append is commuted reverse-append after append.

    ʳ++-ʳ++ : ∀ (xs {ys zs} : List A) → (xs ʳ++ ys) ʳ++ zs ≡ ys ʳ++ xs ++ zs
    ʳ++-ʳ++ [] = refl
    ʳ++-ʳ++ (x ∷ xs) {ys} {zs} = begin
      ((x ∷ xs) ʳ++ ys) ʳ++ zs   ≡⟨⟩
      (xs ʳ++ x ∷ ys) ʳ++ zs     ≡⟨ ʳ++-ʳ++ xs ⟩
      (x ∷ ys) ʳ++ xs ++ zs      ≡⟨⟩
      ys ʳ++ (x ∷ xs) ++ zs      ∎

    -- Length of reverse-append

    length-ʳ++ : ∀ (xs {ys} : List A) →
                 length (xs ʳ++ ys) ≡ length xs + length ys
    length-ʳ++ [] = refl
    length-ʳ++ (x ∷ xs) {ys} = begin
      length ((x ∷ xs) ʳ++ ys)      ≡⟨⟩
      length (xs ʳ++ x ∷ ys)        ≡⟨ length-ʳ++ xs ⟩
      length xs + length (x ∷ ys)   ≡⟨ +-suc _ _ ⟩
      length (x ∷ xs) + length ys   ∎

    -- map distributes over reverse-append.

    map-ʳ++ : (f : A → B) (xs {ys} : List A) →
              map f (xs ʳ++ ys) ≡ map f xs ʳ++ map f ys
    map-ʳ++ f []            = refl
    map-ʳ++ f (x ∷ xs) {ys} = begin
      map f ((x ∷ xs) ʳ++ ys)         ≡⟨⟩
      map f (xs ʳ++ x ∷ ys)           ≡⟨ map-ʳ++ f xs ⟩
      map f xs ʳ++ map f (x ∷ ys)     ≡⟨⟩
      map f xs ʳ++ f x ∷ map f ys     ≡⟨⟩
      (f x ∷ map f xs) ʳ++ map f ys   ≡⟨⟩
      map f (x ∷ xs)   ʳ++ map f ys   ∎

    -- A foldr after a reverse is a foldl.

    foldr-ʳ++ : ∀ (f : A → B → B) b xs {ys} →
                foldr f b (xs ʳ++ ys) ≡ foldl (flip f) (foldr f b ys) xs
    foldr-ʳ++ f b []       {_}  = refl
    foldr-ʳ++ f b (x ∷ xs) {ys} = begin
      foldr f b ((x ∷ xs) ʳ++ ys)              ≡⟨⟩
      foldr f b (xs ʳ++ x ∷ ys)                ≡⟨ foldr-ʳ++ f b xs ⟩
      foldl (flip f) (foldr f b (x ∷ ys)) xs   ≡⟨⟩
      foldl (flip f) (f x (foldr f b ys)) xs   ≡⟨⟩
      foldl (flip f) (foldr f b ys) (x ∷ xs)   ∎

    -- A foldl after a reverse is a foldr.

    foldl-ʳ++ : ∀ (f : B → A → B) b xs {ys} →
                foldl f b (xs ʳ++ ys) ≡ foldl f (foldr (flip f) b xs) ys
    foldl-ʳ++ f b []       {_}  = refl
    foldl-ʳ++ f b (x ∷ xs) {ys} = begin
      foldl f b ((x ∷ xs) ʳ++ ys)              ≡⟨⟩
      foldl f b (xs ʳ++ x ∷ ys)                ≡⟨ foldl-ʳ++ f b xs ⟩
      foldl f (foldr (flip f) b xs) (x ∷ ys)   ≡⟨⟩
      foldl f (f (foldr (flip f) b xs) x) ys   ≡⟨⟩
      foldl f (foldr (flip f) b (x ∷ xs)) ys   ∎

    ------------------------------------------------------------------------
    -- reverse

    -- reverse of cons is snoc of reverse.

    unfold-reverse : ∀ (x : A) xs → reverse (x ∷ xs) ≡ reverse xs ∷ʳ x
    unfold-reverse x xs = ʳ++-defn xs

    -- reverse is an anti-homomorphism with respect to append.

    reverse-++ : (xs ys : List A) →
                         reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
    reverse-++ xs ys = begin
      reverse (xs ++ ys)         ≡⟨⟩
      (xs ++ ys) ʳ++ []          ≡⟨ ++-ʳ++ xs ⟩
      ys ʳ++ xs ʳ++ []           ≡⟨⟩
      ys ʳ++ reverse xs          ≡⟨ ʳ++-defn ys ⟩
      reverse ys ++ reverse xs   ∎

    -- reverse is self-inverse.

    reverse-selfInverse : SelfInverse {A = List A} _≡_ reverse
    reverse-selfInverse {x = xs} {y = ys} xs⁻¹≈ys = begin
      reverse ys         ≡⟨⟩
      ys ʳ++ []          ≡⟨ cong (_ʳ++ []) xs⁻¹≈ys ⟨
      reverse xs ʳ++ []  ≡⟨⟩
      (xs ʳ++ []) ʳ++ [] ≡⟨ ʳ++-ʳ++ xs ⟩
      [] ʳ++ xs ++ []    ≡⟨⟩
      xs ++ []           ≡⟨ ++-identityʳ xs ⟩
      xs                 ∎

    -- reverse is involutive.

    reverse-involutive : Involutive {A = List A} _≡_ reverse
    reverse-involutive = selfInverse⇒involutive reverse-selfInverse

    -- reverse is injective.

    reverse-injective : Injective {A = List A} _≡_ _≡_ reverse
    reverse-injective = selfInverse⇒injective reverse-selfInverse

    -- reverse preserves length.

    length-reverse : ∀ (xs : List A) → length (reverse xs) ≡ length xs
    length-reverse xs = begin
      length (reverse xs)   ≡⟨⟩
      length (xs ʳ++ [])    ≡⟨ length-ʳ++ xs ⟩
      length xs + 0         ≡⟨ +-identityʳ _ ⟩
      length xs             ∎

    reverse-map : (f : A → B) → map f ∘ reverse ≗ reverse ∘ map f
    reverse-map f xs = begin
      map f (reverse xs) ≡⟨⟩
      map f (xs ʳ++ [])  ≡⟨ map-ʳ++ f xs ⟩
      map f xs ʳ++ []    ≡⟨⟩
      reverse (map f xs) ∎

    reverse-foldr : ∀ (f : A → B → B) b →
                    foldr f b ∘ reverse ≗ foldl (flip f) b
    reverse-foldr f b xs = foldr-ʳ++ f b xs

    reverse-foldl : ∀ (f : B → A → B) b xs →
                    foldl f b (reverse xs) ≡ foldr (flip f) b xs
    reverse-foldl f b xs = foldl-ʳ++ f b xs

    ------------------------------------------------------------------------
    -- reverse, applyUpTo, and applyDownFrom

    reverse-applyUpTo : ∀ (f : ℕ → A) n → reverse (applyUpTo f n) ≡ applyDownFrom f n
    reverse-applyUpTo f zero = refl
    reverse-applyUpTo f (suc n) = begin
      reverse (f 0 ∷ applyUpTo (f ∘ suc) n)  ≡⟨ reverse-++ [ f 0 ] (applyUpTo (f ∘ suc) n) ⟩
      reverse (applyUpTo (f ∘ suc) n) ∷ʳ f 0 ≡⟨ cong (_∷ʳ f 0) (reverse-applyUpTo (f ∘ suc) n) ⟩
      applyDownFrom (f ∘ suc) n ∷ʳ f 0       ≡⟨ applyDownFrom-∷ʳ f n ⟩
      applyDownFrom f (suc n)                ∎

    reverse-upTo : ∀ n → reverse (upTo n) ≡ downFrom n
    reverse-upTo = reverse-applyUpTo id

    reverse-applyDownFrom : ∀ (f : ℕ → A) n → reverse (applyDownFrom f n) ≡ applyUpTo f n
    reverse-applyDownFrom f zero = refl
    reverse-applyDownFrom f (suc n) = begin
      reverse (f n ∷ applyDownFrom f n)  ≡⟨ reverse-++ [ f n ] (applyDownFrom f n) ⟩
      reverse (applyDownFrom f n) ∷ʳ f n ≡⟨ cong (_∷ʳ f n) (reverse-applyDownFrom f n) ⟩
      applyUpTo f n ∷ʳ f n               ≡⟨ applyUpTo-∷ʳ f n ⟩
      applyUpTo f (suc n)                ∎

    reverse-downFrom : ∀ n → reverse (downFrom n) ≡ upTo n
    reverse-downFrom = reverse-applyDownFrom id

    ------------------------------------------------------------------------
    -- _∷ʳ_

    ∷ʳ-injective : ∀ xs ys → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y
    ∷ʳ-injective []          []          refl = refl , refl
    ∷ʳ-injective (x ∷ xs)    (y  ∷ ys)   eq   with refl , eq′  ← ∷-injective eq
      = Product.map (cong (x ∷_)) id (∷ʳ-injective xs ys eq′)
    ∷ʳ-injective []          (_ ∷ _ ∷ _) ()
    ∷ʳ-injective (_ ∷ _ ∷ _) []          ()

    ∷ʳ-injectiveˡ : ∀ xs ys → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys
    ∷ʳ-injectiveˡ xs ys eq = proj₁ (∷ʳ-injective xs ys eq)

    ∷ʳ-injectiveʳ : ∀ xs ys → xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y
    ∷ʳ-injectiveʳ xs ys eq = proj₂ (∷ʳ-injective xs ys eq)

    ∷ʳ-++ : ∀ xs (a : A) ys → xs ∷ʳ a ++ ys ≡ xs ++ a ∷ ys
    ∷ʳ-++ xs a ys = ++-assoc xs [ a ] ys

    ------------------------------------------------------------------------
    -- uncons

    module _ (f : A → B) where

      -- 'commute' List.uncons and List.map to obtain a Maybe.map and List.uncons.
      uncons-map : uncons ∘ map f ≗ Maybe.map (Product.map f (map f)) ∘ uncons
      uncons-map []       = refl
      uncons-map (x ∷ xs) = refl

    ------------------------------------------------------------------------
    -- head

    module _ {f : A → B} where

      -- 'commute' List.head and List.map to obtain a Maybe.map and List.head.
      head-map : head ∘ map f ≗ Maybe.map f ∘ head
      head-map []      = refl
      head-map (_ ∷ _) = refl

    ------------------------------------------------------------------------
    -- last

    module _ (f : A → B) where

      -- 'commute' List.last and List.map to obtain a Maybe.map and List.last.
      last-map : last ∘ map f ≗ Maybe.map f ∘ last
      last-map []               = refl
      last-map (x ∷ [])         = refl
      last-map (x ∷ xs@(_ ∷ _)) = last-map xs

    ------------------------------------------------------------------------
    -- tail

    module _ (f : A → B) where

      -- 'commute' List.tail and List.map to obtain a Maybe.map and List.tail.
      tail-map : tail ∘ map f ≗ Maybe.map (map f) ∘ tail
      tail-map []       = refl
      tail-map (x ∷ xs) = refl

    ------------------------------------------------------------------------
    -- DEPRECATED NAMES
    ------------------------------------------------------------------------
    -- Please use the new names as continuing support for the old names is
    -- not guaranteed.

    -- Version 2.0

    map-id₂ = map-id-local
    {-# WARNING_ON_USAGE map-id₂
    "Warning: map-id₂ was deprecated in v2.0.
    Please use map-id-local instead."
    #-}

    map-cong₂ = map-cong-local
    {-# WARNING_ON_USAGE map-id₂
    "Warning: map-cong₂ was deprecated in v2.0.
    Please use map-cong-local instead."
    #-}

    map-compose = map-∘
    {-# WARNING_ON_USAGE map-compose
    "Warning: map-compose was deprecated in v2.0.
    Please use map-∘ instead."
    #-}

    map-++-commute = map-++
    {-# WARNING_ON_USAGE map-++-commute
    "Warning: map-++-commute was deprecated in v2.0.
    Please use map-++ instead."
    #-}

    reverse-map-commute = reverse-map
    {-# WARNING_ON_USAGE reverse-map-commute
    "Warning: reverse-map-commute was deprecated in v2.0.
    Please use reverse-map instead."
    #-}

    reverse-++-commute = reverse-++
    {-# WARNING_ON_USAGE reverse-++-commute
    "Warning: reverse-++-commute was deprecated in v2.0.
    Please use reverse-++ instead."
    #-}

    zipWith-identityˡ = zipWith-zeroˡ
    {-# WARNING_ON_USAGE zipWith-identityˡ
    "Warning: zipWith-identityˡ was deprecated in v2.0.
    Please use zipWith-zeroˡ instead."
    #-}

    zipWith-identityʳ = zipWith-zeroʳ
    {-# WARNING_ON_USAGE zipWith-identityʳ
    "Warning: zipWith-identityʳ was deprecated in v2.0.
    Please use zipWith-zeroʳ instead."
    #-}

    ʳ++-++ = ++-ʳ++
    {-# WARNING_ON_USAGE ʳ++-++
    "Warning: ʳ++-++ was deprecated in v2.0.
    Please use ++-ʳ++ instead."
    #-}

    take++drop = take++drop≡id
    {-# WARNING_ON_USAGE take++drop
    "Warning: take++drop was deprecated in v2.0.
    Please use take++drop≡id instead."
    #-}

    length-─ = length-removeAt
    {-# WARNING_ON_USAGE length-─
    "Warning: length-─ was deprecated in v2.0.
    Please use length-removeAt instead."
    #-}

    map-─ = map-removeAt
    {-# WARNING_ON_USAGE map-─
    "Warning: map-─ was deprecated in v2.0.
    Please use map-removeAt instead."
    #-}

    -- Version 2.1

    scanr-defn : ∀ (f : A → B → B) (e : B) →
                 scanr f e ≗ map (foldr f e) ∘ tails
    scanr-defn f e []             = refl
    scanr-defn f e (x ∷ [])       = refl
    scanr-defn f e (x ∷ xs@(_ ∷ _))
      with eq ← scanr-defn f e xs
      with ys@(_ ∷ _) ← scanr f e xs
      = cong₂ (λ z → f x z ∷_) (∷-injectiveˡ eq) eq
    {-# WARNING_ON_USAGE scanr-defn
    "Warning: scanr-defn was deprecated in v2.1.
    Please use Data.List.Scans.Properties.scanr-defn instead."
    #-}

    scanl-defn : ∀ (f : A → B → A) (e : A) →
                 scanl f e ≗ map (foldl f e) ∘ inits
    scanl-defn f e []       = refl
    scanl-defn f e (x ∷ xs) = cong (e ∷_) (begin
       scanl f (f e x) xs
     ≡⟨ scanl-defn f (f e x) xs ⟩
       map (foldl f (f e x)) (inits xs)
     ≡⟨ refl ⟩
       map (foldl f e ∘ (x ∷_)) (inits xs)
     ≡⟨ map-∘ (inits xs) ⟩
       map (foldl f e) (map (x ∷_) (inits xs))
     ∎)
    {-# WARNING_ON_USAGE scanl-defn
    "Warning: scanl-defn was deprecated in v2.1.
    Please use Data.List.Scans.Properties.scanl-defn instead."
    #-}

    -- Version 2.2

    concat-[-] = concat-map-[_]
    {-# WARNING_ON_USAGE concat-[-]
    "Warning: concat-[-] was deprecated in v2.2.
    Please use concat-map-[_] instead."
    #-}

    -- Version 2.3

    sum-++ : ∀ xs ys → sum (xs ++ ys) ≡ sum xs + sum ys
    sum-++ []       ys = refl
    sum-++ (x ∷ xs) ys = begin
      x + sum (xs ++ ys)     ≡⟨ cong (x +_) (sum-++ xs ys) ⟩
      x + (sum xs + sum ys)  ≡⟨ +-assoc x _ _ ⟨
      (x + sum xs) + sum ys  ∎
    {-# WARNING_ON_USAGE sum-++
    "Warning: sum-++ was deprecated in v2.3.
    Please use Data.Nat.ListAction.Properties.sum-++ instead."
    #-}
    sum-++-commute = sum-++
    {-# WARNING_ON_USAGE sum-++-commute
    "Warning: sum-++-commute was deprecated in v2.0.
    Please use Data.Nat.ListAction.Properties.sum-++ instead."
    #-}

    open import Data.List.Membership.Propositional using (_∈_)
    open import Data.Nat.Divisibility using (_∣_; m∣m*n; ∣n⇒∣m*n)

    ∈⇒∣product : ∀ {n ns} → n ∈ ns → n ∣ product ns
    ∈⇒∣product {ns = n ∷ ns} (here  refl) = m∣m*n (product ns)
    ∈⇒∣product {ns = m ∷ ns} (there n∈ns) = ∣n⇒∣m*n m (∈⇒∣product n∈ns)
    {-# WARNING_ON_USAGE ∈⇒∣product
    "Warning: ∈⇒∣product was deprecated in v2.3.
    Please use Data.Nat.ListAction.Properties.∈⇒∣product instead."
    #-}

    product≢0 : ∀ {ns} → All NonZero ns → NonZero (product ns)
    product≢0 [] = _
    product≢0 {n ∷ ns} (n≢0 ∷ ns≢0) = m*n≢0 n (product ns) {{n≢0}} {{product≢0 ns≢0}}
    {-# WARNING_ON_USAGE product≢0
    "Warning: product≢0 was deprecated in v2.3.
    Please use Data.Nat.ListAction.Properties.product≢0 instead."
    #-}

    ∈⇒≤product : ∀ {n ns} → All NonZero ns → n ∈ ns → n ≤ product ns
    ∈⇒≤product {ns = n ∷ ns} (_ ∷ ns≢0) (here refl) =
      m≤m*n n (product ns) {{product≢0 ns≢0}}
    ∈⇒≤product {ns = n ∷ _} (n≢0 ∷ ns≢0) (there n∈ns) =
      m≤n⇒m≤o*n n {{n≢0}} (∈⇒≤product ns≢0 n∈ns)
    {-# WARNING_ON_USAGE ∈⇒≤product
    "Warning: ∈⇒≤product was deprecated in v2.3.
    Please use Data.Nat.ListAction.Properties.∈⇒≤product instead."
    #-}