    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties related to All
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.List.Relation.Unary.All.Properties where

    open import Axiom.Extensionality.Propositional using (Extensionality)
    open import Data.Bool.Base using (Bool; T; true; false)
    open import Data.Bool.ListAction using (all)
    open import Data.Bool.Properties using (T-∧)
    open import Data.Fin.Base using (Fin; zero; suc)
    open import Data.List.Base as List hiding (lookup; updateAt; and; or; all; any)
    open import Data.List.Membership.Propositional using (_∈_; _≢∈_)
    open import Data.List.Membership.Propositional.Properties
      using (there-injective-≢∈; ∈-filter⁻)
    import Data.List.Membership.Setoid as SetoidMembership
    import Data.List.Properties as List
    import Data.List.Relation.Binary.Equality.Setoid as ≋
    open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
    import Data.List.Relation.Binary.Subset.Propositional as Subset
    open import Data.List.Relation.Unary.All as All using
      ( All; []; _∷_; lookup; updateAt
      ; _[_]=_; here; there
      ; Null
      )
    open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
    open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
    open import Data.Maybe.Relation.Unary.All as Maybe using (just; nothing; fromAny)
    open import Data.Maybe.Relation.Unary.Any as Maybe using (just)
    open import Data.Nat.Base using (zero; suc; s≤s; _<_; z<s; s<s)
    open import Data.Nat.Properties using (≤-refl; m≤n⇒m≤1+n)
    open import Data.Product.Base as Product using (_×_; _,_; uncurry; uncurry′)
    open import Function.Base using (_∘_; _$_; id; case_of_; flip)
    open import Function.Bundles using (_↠_; mk↠ₛ; _⇔_; mk⇔; _↔_; mk↔ₛ′; Equivalence)
    open import Level using (Level)
    open import Relation.Binary.Core using (REL)
    open import Relation.Binary.Bundles using (Setoid)
    import Relation.Binary.Definitions as B
    open import Relation.Binary.PropositionalEquality.Core
      using (_≡_; refl; sym; cong; cong₂; _≗_)
    open import Relation.Nullary.Reflects using (invert)
    open import Relation.Nullary.Negation.Core using (¬_; contradiction)
    open import Relation.Nullary.Decidable
      using (Dec; does; yes; no; _because_; ¬?; decidable-stable; dec-true)
    open import Relation.Unary
      using (Decidable; Pred; ∁; _⟨×⟩_) renaming (_⊆_ to _⋐_)
    open import Relation.Unary.Properties using (∁?)

    private
      variable
        a b c p q r ℓ ℓ₁ ℓ₂ : Level
        A : Set a
        B : Set b
        C : Set c
        P : Pred A p
        Q : Pred B q
        R : Pred C r
        x y : A
        xs ys : List A

    ------------------------------------------------------------------------
    -- Re-export Core Properties

    open import Data.List.Relation.Unary.All.Properties.Core public

    ------------------------------------------------------------------------
    -- Properties regarding Null

    Null⇒null : Null xs → T (null xs)
    Null⇒null [] = _

    null⇒Null : T (null xs) → Null xs
    null⇒Null {xs = []   } _ = []
    null⇒Null {xs = _ ∷ _} ()

    ------------------------------------------------------------------------
    -- Properties of the "points-to" relation _[_]=_

    -- Relation _[_]=_ is deterministic: each index points to a single value.

    []=-injective : ∀ {px qx : P x} {pxs : All P xs} {i : x ∈ xs} →
                    pxs [ i ]= px →
                    pxs [ i ]= qx →
                    px ≡ qx
    []=-injective here          here          = refl
    []=-injective (there x↦px) (there x↦qx) = []=-injective x↦px x↦qx

    -- See also Data.List.Relation.Unary.All.Properties.WithK.[]=-irrelevant.

    ------------------------------------------------------------------------
    -- Defining properties of lookup and _[_]=_
    --
    -- pxs [ i ]= px  if and only if  lookup pxs i = px.

    -- `i` points to `lookup pxs i` in `pxs`.

    []=lookup : (pxs : All P xs) (i : x ∈ xs) →
                pxs [ i ]= lookup pxs i
    []=lookup (px ∷ pxs) (here refl) = here
    []=lookup (px ∷ pxs) (there i)   = there ([]=lookup pxs i)

    -- If `i` points to `px` in `pxs`, then `lookup pxs i ≡ px`.

    []=⇒lookup : ∀ {px : P x} {pxs : All P xs} {i : x ∈ xs} →
                 pxs [ i ]= px →
                 lookup pxs i ≡ px
    []=⇒lookup x↦px = []=-injective ([]=lookup _ _) x↦px

    -- If `lookup pxs i ≡ px`, then `i` points to `px` in `pxs`.

    lookup⇒[]= : ∀ {px : P x} (pxs : All P xs) (i : x ∈ xs) →
                 lookup pxs i ≡ px →
                 pxs [ i ]= px
    lookup⇒[]= pxs i refl = []=lookup pxs i

    ------------------------------------------------------------------------
    -- Properties of operations over `All`
    ------------------------------------------------------------------------
    -- map

    map-cong : ∀ {f : P ⋐ Q} {g : P ⋐ Q} (pxs : All P xs) →
               (∀ {x} → f {x} ≗ g) → All.map f pxs ≡ All.map g pxs
    map-cong []         _   = refl
    map-cong (px ∷ pxs) feq = cong₂ _∷_ (feq px) (map-cong pxs feq)

    map-id : ∀ (pxs : All P xs) → All.map id pxs ≡ pxs
    map-id []         = refl
    map-id (px ∷ pxs) = cong (px ∷_)  (map-id pxs)

    map-∘ : ∀ {f : P ⋐ Q} {g : Q ⋐ R} (pxs : All P xs) →
            All.map g (All.map f pxs) ≡ All.map (g ∘ f) pxs
    map-∘ []         = refl
    map-∘ (px ∷ pxs) = cong (_ ∷_) (map-∘ pxs)

    lookup-map : ∀ {f : P ⋐ Q} (pxs : All P xs) (i : x ∈ xs) →
                 lookup (All.map f pxs) i ≡ f (lookup pxs i)
    lookup-map (px ∷ pxs) (here refl) = refl
    lookup-map (px ∷ pxs) (there i)   = lookup-map pxs i

    ------------------------------------------------------------------------
    -- _[_]%=_ / updateAt

      -- Defining properties of updateAt:

    -- (+) updateAt actually updates the element at the given index.

    updateAt-updates : ∀ (i : x ∈ xs) {f : P x → P x} {px : P x} (pxs : All P xs) →
                       pxs              [ i ]= px →
                       updateAt i f pxs [ i ]= f px
    updateAt-updates (here  refl) (px ∷ pxs) here         = here
    updateAt-updates (there i)    (px ∷ pxs) (there x↦px) =
      there (updateAt-updates i pxs x↦px)

    -- (-) updateAt i does not touch the elements at other indices.

    updateAt-minimal : ∀ (i : x ∈ xs) (j : y ∈ xs) →
                       ∀ {f : P y → P y} {px : P x} (pxs : All P xs) →
                       i ≢∈ j →
                       pxs              [ i ]= px →
                       updateAt j f pxs [ i ]= px
    updateAt-minimal (here .refl) (here refl) (px ∷ pxs) i≢j here        =
      contradiction refl (i≢j refl)
    updateAt-minimal (here .refl) (there j)   (px ∷ pxs) i≢j here        = here
    updateAt-minimal (there i)    (here refl) (px ∷ pxs) i≢j (there val) = there val
    updateAt-minimal (there i)    (there j)   (px ∷ pxs) i≢j (there val) =
      there (updateAt-minimal i j pxs (there-injective-≢∈ i≢j) val)

    -- lookup after updateAt reduces.

    -- For same index this is an easy consequence of updateAt-updates
    -- using []=↔lookup.

    lookup∘updateAt : ∀ (pxs : All P xs) (i : x ∈ xs) {f : P x → P x} →
                      lookup (updateAt i f pxs) i ≡ f (lookup pxs i)
    lookup∘updateAt pxs i =
      []=⇒lookup (updateAt-updates i pxs (lookup⇒[]= pxs i refl))

    -- For different indices it easily follows from updateAt-minimal.

    lookup∘updateAt′ : ∀ (i : x ∈ xs) (j : y ∈ xs) →
                       ∀ {f : P y → P y} {px : P x} (pxs : All P xs) →
                       i ≢∈ j →
                       lookup (updateAt j f pxs) i ≡ lookup pxs i
    lookup∘updateAt′ i j pxs i≢j =
      []=⇒lookup (updateAt-minimal i j pxs i≢j (lookup⇒[]= pxs i refl))

    -- The other properties are consequences of (+) and (-).
    -- We spell the most natural properties out.
    -- Direct inductive proofs are in most cases easier than just using
    -- the defining properties.

    -- In the explanations, we make use of shorthand  f = g ↾ x
    -- meaning that f and g agree locally at point x, i.e.  f x ≡ g x.

    -- updateAt (i : x ∈ xs)  is a morphism
    -- from the monoid of endofunctions  P x → P x
    -- to the monoid of endofunctions  All P xs → All P xs.

    -- 1a. local identity:  f = id ↾ (lookup pxs i)
    --             implies  updateAt i f = id ↾ pxs

    updateAt-id-local : ∀ (i : x ∈ xs) {f : P x → P x} (pxs : All P xs) →
                        f (lookup pxs i) ≡ lookup pxs i →
                        updateAt i f pxs ≡ pxs
    updateAt-id-local (here refl)(px ∷ pxs) eq = cong (_∷ pxs) eq
    updateAt-id-local (there i)  (px ∷ pxs) eq = cong (px ∷_) (updateAt-id-local i pxs eq)

    -- 1b. identity:  updateAt i id ≗ id

    updateAt-id : ∀ (i : x ∈ xs) (pxs : All P xs) → updateAt i id pxs ≡ pxs
    updateAt-id i pxs = updateAt-id-local i pxs refl

    -- 2a. relative composition:  f ∘ g = h ↾ (lookup i pxs)
    --                   implies  updateAt i f ∘ updateAt i g = updateAt i h ↾ pxs

    updateAt-∘-local : ∀ (i : x ∈ xs) {f g h : P x → P x} (pxs : All P xs) →
                       f (g (lookup pxs i)) ≡ h (lookup pxs i) →
                       updateAt i f (updateAt i g pxs) ≡ updateAt i h pxs
    updateAt-∘-local (here refl) (px ∷ pxs) fg=h = cong (_∷ pxs) fg=h
    updateAt-∘-local (there i)   (px ∷ pxs) fg=h = cong (px ∷_) (updateAt-∘-local i pxs fg=h)

    -- 2b. composition:  updateAt i f ∘ updateAt i g ≗ updateAt i (f ∘ g)

    updateAt-∘ : ∀ (i : x ∈ xs) {f g : P x → P x} →
                 updateAt {P = P} i f ∘ updateAt i g ≗ updateAt i (f ∘ g)
    updateAt-∘ i pxs = updateAt-∘-local i pxs refl

    -- 3. congruence:  updateAt i  is a congruence wrt. extensional equality.

    -- 3a.  If    f = g ↾ (lookup pxs i)
    --      then  updateAt i f = updateAt i g ↾ pxs

    updateAt-cong-local : ∀ (i : x ∈ xs) {f g : P x → P x} (pxs : All P xs) →
                          f (lookup pxs i) ≡ g (lookup pxs i) →
                          updateAt i f pxs ≡ updateAt i g pxs
    updateAt-cong-local (here refl) (px ∷ pxs) f=g = cong (_∷ pxs) f=g
    updateAt-cong-local (there i)   (px ∷ pxs) f=g = cong (px ∷_) (updateAt-cong-local i pxs f=g)

    -- 3b. congruence:  f ≗ g → updateAt i f ≗ updateAt i g

    updateAt-cong : ∀ (i : x ∈ xs) {f g : P x → P x} →
                    f ≗ g → updateAt {P = P} i f ≗ updateAt i g
    updateAt-cong i f≗g pxs = updateAt-cong-local i pxs (f≗g (lookup pxs i))

    -- The order of updates at different indices i ≢ j does not matter.

    -- This a consequence of updateAt-updates and updateAt-minimal
    -- but easier to prove inductively.

    updateAt-commutes : ∀ (i : x ∈ xs) (j : y ∈ xs) →
                        ∀ {f : P x → P x} {g : P y → P y} →
                        i ≢∈ j →
                        updateAt {P = P} i f ∘ updateAt j g ≗ updateAt j g ∘ updateAt i f
    updateAt-commutes (here refl) (here refl) i≢j (px ∷ pxs) =
      contradiction refl (i≢j refl)
    updateAt-commutes (here refl) (there j)   i≢j (px ∷ pxs) = refl
    updateAt-commutes (there i)   (here refl) i≢j (px ∷ pxs) = refl
    updateAt-commutes (there i)   (there j)   i≢j (px ∷ pxs) =
      cong (px ∷_) (updateAt-commutes i j (there-injective-≢∈ i≢j) pxs)

    map-updateAt : ∀ {f : P ⋐ Q} {g : P x → P x} {h : Q x → Q x}
                   (pxs : All P xs) (i : x ∈ xs) →
                   f (g (lookup pxs i)) ≡ h (f (lookup pxs i)) →
                   All.map f (pxs All.[ i ]%= g) ≡ (All.map f pxs) All.[ i ]%= h
    map-updateAt (px ∷ pxs) (here refl) = cong (_∷ _)
    map-updateAt (px ∷ pxs) (there i) feq = cong (_ ∷_) (map-updateAt pxs i feq)

    ------------------------------------------------------------------------
    -- Introduction (⁺) and elimination (⁻) rules for list operations
    ------------------------------------------------------------------------
    -- singleton

    singleton⁻ : All P [ x ] → P x
    singleton⁻ (px ∷ []) = px

    -- head

    head⁺ : All P xs → Maybe.All P (head xs)
    head⁺ []       = nothing
    head⁺ (px ∷ _) = just px

    -- tail

    tail⁺ : All P xs → Maybe.All (All P) (tail xs)
    tail⁺ []        = nothing
    tail⁺ (_ ∷ pxs) = just pxs

    -- last

    last⁺ : All P xs → Maybe.All P (last xs)
    last⁺ []                 = nothing
    last⁺ (px ∷ [])          = just px
    last⁺ (px ∷ pxs@(_ ∷ _)) = last⁺ pxs

    -- uncons

    uncons⁺ : All P xs → Maybe.All (P ⟨×⟩ All P) (uncons xs)
    uncons⁺ []         = nothing
    uncons⁺ (px ∷ pxs) = just (px , pxs)

    uncons⁻ : Maybe.All (P ⟨×⟩ All P) (uncons xs) → All P xs
    uncons⁻ {xs = []}     nothing           = []
    uncons⁻ {xs = x ∷ xs} (just (px , pxs)) = px ∷ pxs

    -- map

    map⁺ : ∀ {f : A → B} → All (P ∘ f) xs → All P (map f xs)
    map⁺ []       = []
    map⁺ (p ∷ ps) = p ∷ map⁺ ps

    map⁻ : ∀ {f : A → B} → All P (map f xs) → All (P ∘ f) xs
    map⁻ {xs = []}    []       = []
    map⁻ {xs = _ ∷ _} (p ∷ ps) = p ∷ map⁻ ps

    -- A variant of All.map.

    gmap⁺ : ∀ {f : A → B} → P ⋐ Q ∘ f → All P ⋐ All Q ∘ map f
    gmap⁺ g = map⁺ ∘ All.map g

    gmap⁻ : ∀ {f : A → B} → Q ∘ f ⋐ P → All Q ∘ map f ⋐ All P
    gmap⁻ g = All.map g ∘ map⁻

    ------------------------------------------------------------------------
    -- mapMaybe

    mapMaybe⁺ : ∀ {f : A → Maybe B} →
                All (Maybe.All P) (map f xs) → All P (mapMaybe f xs)
    mapMaybe⁺ {xs = []}     {f = f} []         = []
    mapMaybe⁺ {xs = x ∷ xs} {f = f} (px ∷ pxs) with f x
    ... | nothing = mapMaybe⁺ pxs
    ... | just v with just pv ← px = pv ∷ mapMaybe⁺ pxs

    ------------------------------------------------------------------------
    -- catMaybes

    All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs)
    All-catMaybes⁺ [] = []
    All-catMaybes⁺ (just px ∷ pxs) = px ∷ All-catMaybes⁺ pxs
    All-catMaybes⁺ (nothing ∷ pxs) = All-catMaybes⁺ pxs

    Any-catMaybes⁺ : All (Maybe.Any P) xs → All P (catMaybes xs)
    Any-catMaybes⁺ = All-catMaybes⁺ ∘ All.map fromAny

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

    ++⁺ : All P xs → All P ys → All P (xs ++ ys)
    ++⁺ []         pys = pys
    ++⁺ (px ∷ pxs) pys = px ∷ ++⁺ pxs pys

    ++⁻ˡ : ∀ xs {ys} → All P (xs ++ ys) → All P xs
    ++⁻ˡ []       p          = []
    ++⁻ˡ (x ∷ xs) (px ∷ pxs) = px ∷ (++⁻ˡ _ pxs)

    ++⁻ʳ : ∀ xs {ys} → All P (xs ++ ys) → All P ys
    ++⁻ʳ []       p          = p
    ++⁻ʳ (x ∷ xs) (px ∷ pxs) = ++⁻ʳ xs pxs

    ++⁻ : ∀ xs {ys} → All P (xs ++ ys) → All P xs × All P ys
    ++⁻ []       p          = [] , p
    ++⁻ (x ∷ xs) (px ∷ pxs) = Product.map (px ∷_) id (++⁻ _ pxs)

    ++↔ : (All P xs × All P ys) ↔ All P (xs ++ ys)
    ++↔ {xs = zs} = mk↔ₛ′ (uncurry ++⁺) (++⁻ zs) (++⁺∘++⁻ zs) ++⁻∘++⁺
      where
      ++⁺∘++⁻ : ∀ xs (p : All P (xs ++ ys)) → uncurry′ ++⁺ (++⁻ xs p) ≡ p
      ++⁺∘++⁻ []       p          = refl
      ++⁺∘++⁻ (x ∷ xs) (px ∷ pxs) = cong (_∷_ px) $ ++⁺∘++⁻ xs pxs

      ++⁻∘++⁺ : ∀ (p : All P xs × All P ys) → ++⁻ xs (uncurry ++⁺ p) ≡ p
      ++⁻∘++⁺ ([]       , pys) = refl
      ++⁻∘++⁺ (px ∷ pxs , pys) rewrite ++⁻∘++⁺ (pxs , pys) = refl

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

    concat⁺ : ∀ {xss} → All (All P) xss → All P (concat xss)
    concat⁺ []           = []
    concat⁺ (pxs ∷ pxss) = ++⁺ pxs (concat⁺ pxss)

    concat⁻ : ∀ {xss} → All P (concat xss) → All (All P) xss
    concat⁻ {xss = []}       []  = []
    concat⁻ {xss = xs ∷ xss} pxs = ++⁻ˡ xs pxs ∷ concat⁻ (++⁻ʳ xs pxs)

    ------------------------------------------------------------------------
    -- snoc

    ∷ʳ⁺ : All P xs → P x → All P (xs ∷ʳ x)
    ∷ʳ⁺ pxs px = ++⁺ pxs (px ∷ [])

    ∷ʳ⁻ : All P (xs ∷ʳ x) → All P xs × P x
    ∷ʳ⁻ pxs = Product.map₂ singleton⁻ $ ++⁻ _ pxs

    -- unsnoc

    unsnoc⁺ : All P xs → Maybe.All (All P ⟨×⟩ P) (unsnoc xs)
    unsnoc⁺ {xs = xs} pxs with initLast xs
    unsnoc⁺ {xs = .[]}        pxs | []       = nothing
    unsnoc⁺ {xs = .(xs ∷ʳ x)} pxs | xs ∷ʳ′ x = just (∷ʳ⁻ pxs)

    unsnoc⁻ : Maybe.All (All P ⟨×⟩ P) (unsnoc xs) → All P xs
    unsnoc⁻ {xs = xs} pxs with initLast xs
    unsnoc⁻ {xs = .[]}        nothing           | []       = []
    unsnoc⁻ {xs = .(xs ∷ʳ x)} (just (pxs , px)) | xs ∷ʳ′ x = ∷ʳ⁺ pxs px

    ------------------------------------------------------------------------
    -- cartesianProductWith and cartesianProduct

    module _ (S₁ : Setoid a ℓ₁) (S₂ : Setoid b ℓ₂) where
      open SetoidMembership S₁ using () renaming (_∈_ to _∈₁_)
      open SetoidMembership S₂ using () renaming (_∈_ to _∈₂_)

      cartesianProductWith⁺ : ∀ f xs ys →
                              (∀ {x y} → x ∈₁ xs → y ∈₂ ys → P (f x y)) →
                              All P (cartesianProductWith f xs ys)
      cartesianProductWith⁺ f []       ys pres = []
      cartesianProductWith⁺ f (x ∷ xs) ys pres = ++⁺
        (map⁺ (All.tabulateₛ S₂ (pres (here (Setoid.refl S₁)))))
        (cartesianProductWith⁺ f xs ys (pres ∘ there))

      cartesianProduct⁺ : ∀ xs ys →
                          (∀ {x y} → x ∈₁ xs → y ∈₂ ys → P (x , y)) →
                          All P (cartesianProduct xs ys)
      cartesianProduct⁺ = cartesianProductWith⁺ _,_

    ------------------------------------------------------------------------
    -- take and drop

    drop⁺ : ∀ n → All P xs → All P (drop n xs)
    drop⁺ zero    pxs        = pxs
    drop⁺ (suc n) []         = []
    drop⁺ (suc n) (px ∷ pxs) = drop⁺ n pxs

    dropWhile⁺ : (Q? : Decidable Q) → All P xs → All P (dropWhile Q? xs)
    dropWhile⁺               Q? []         = []
    dropWhile⁺ {xs = x ∷ xs} Q? px∷pxs@(_ ∷ pxs) with does (Q? x)
    ... | true  = dropWhile⁺ Q? pxs
    ... | false = px∷pxs

    dropWhile⁻ : (P? : Decidable P) → dropWhile P? xs ≡ [] → All P xs
    dropWhile⁻ {xs = []}     P? eq = []
    dropWhile⁻ {xs = x ∷ xs} P? eq with P? x
    ... | yes px = px ∷ (dropWhile⁻ P? eq)
    ... | no ¬px = case eq of λ ()

    all-head-dropWhile : (P? : Decidable P) →
                         ∀ xs → Maybe.All (∁ P) (head (dropWhile P? xs))
    all-head-dropWhile P? []       = nothing
    all-head-dropWhile P? (x ∷ xs) with P? x
    ... | yes px = all-head-dropWhile P? xs
    ... | no ¬px = just ¬px

    all⇒dropWhile≡[] : (P? : Decidable P) → All P xs → dropWhile P? xs ≡ []
    all⇒dropWhile≡[] P? [] = refl
    all⇒dropWhile≡[] P? (px ∷ pxs) rewrite dec-true (P? _) px
      = all⇒dropWhile≡[] P? pxs

    take⁺ : ∀ n → All P xs → All P (take n xs)
    take⁺ zero    pxs        = []
    take⁺ (suc n) []         = []
    take⁺ (suc n) (px ∷ pxs) = px ∷ take⁺ n pxs

    takeWhile⁺ : (Q? : Decidable Q) → All P xs → All P (takeWhile Q? xs)
    takeWhile⁺               Q? []         = []
    takeWhile⁺ {xs = x ∷ xs} Q? (px ∷ pxs) with does (Q? x)
    ... | true  = px ∷ takeWhile⁺ Q? pxs
    ... | false = []

    all-takeWhile : (P? : Decidable P) → ∀ xs → All P (takeWhile P? xs)
    all-takeWhile P? []       = []
    all-takeWhile P? (x ∷ xs) with P? x
    ... | yes px = px ∷ all-takeWhile P? xs
    ... | no ¬px = []

    all⇒takeWhile≗id : (P? : Decidable P) → All P xs → takeWhile P? xs ≡ xs
    all⇒takeWhile≗id P? [] = refl
    all⇒takeWhile≗id P? (px ∷ pxs) rewrite dec-true (P? _) px
      = cong (_ ∷_) (all⇒takeWhile≗id P? pxs)

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

    applyUpTo⁺₁ : ∀ f n → (∀ {i} → i < n → P (f i)) → All P (applyUpTo f n)
    applyUpTo⁺₁ f zero    Pf = []
    applyUpTo⁺₁ f (suc n) Pf = Pf z<s ∷ applyUpTo⁺₁ (f ∘ suc) n (Pf ∘ s<s)

    applyUpTo⁺₂ : ∀ f n → (∀ i → P (f i)) → All P (applyUpTo f n)
    applyUpTo⁺₂ f n Pf = applyUpTo⁺₁ f n (λ _ → Pf _)

    applyUpTo⁻ : ∀ f n → All P (applyUpTo f n) → ∀ {i} → i < n → P (f i)
    applyUpTo⁻ f (suc n) (px ∷ _)   z<s       = px
    applyUpTo⁻ f (suc n) (_  ∷ pxs) (s<s i<n@(s≤s _)) =
      applyUpTo⁻ (f ∘ suc) n pxs i<n

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

    all-upTo : ∀ n → All (_< n) (upTo n)
    all-upTo n = applyUpTo⁺₁ id n id

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

    applyDownFrom⁺₁ : ∀ f n → (∀ {i} → i < n → P (f i)) → All P (applyDownFrom f n)
    applyDownFrom⁺₁ f zero    Pf = []
    applyDownFrom⁺₁ f (suc n) Pf = Pf ≤-refl ∷ applyDownFrom⁺₁ f n (Pf ∘ m≤n⇒m≤1+n)

    applyDownFrom⁺₂ : ∀ f n → (∀ i → P (f i)) → All P (applyDownFrom f n)
    applyDownFrom⁺₂ f n Pf = applyDownFrom⁺₁ f n (λ _ → Pf _)

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

    tabulate⁺ : ∀ {n} {f : Fin n → A} →
                (∀ i → P (f i)) → All P (tabulate f)
    tabulate⁺ {n = zero}  Pf = []
    tabulate⁺ {n = suc _} Pf = Pf zero ∷ tabulate⁺ (Pf ∘ suc)

    tabulate⁻ : ∀ {n} {f : Fin n → A} →
                All P (tabulate f) → (∀ i → P (f i))
    tabulate⁻ (px ∷ _) zero    = px
    tabulate⁻ (_ ∷ pf) (suc i) = tabulate⁻ pf i

    ------------------------------------------------------------------------
    -- remove

    ─⁺ : ∀ (p : Any P xs) → All Q xs → All Q (xs Any.─ p)
    ─⁺ (here px) (_ ∷ qs) = qs
    ─⁺ (there p) (q ∷ qs) = q ∷ ─⁺ p qs

    ─⁻ : ∀ (p : Any P xs) → Q (Any.lookup p) → All Q (xs Any.─ p) → All Q xs
    ─⁻ (here px) q qs        = q ∷ qs
    ─⁻ (there p) q (q′ ∷ qs) = q′ ∷ ─⁻ p q qs

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

    module _ (P? : Decidable P) where

      all-filter : ∀ xs → All P (filter P? xs)
      all-filter []       = []
      all-filter (x ∷ xs) with P? x
      ... | true  because [Px] = invert [Px] ∷ all-filter xs
      ... | false because  _   = all-filter xs

      filter⁺ : All Q xs → All Q (filter P? xs)
      filter⁺ {xs = _}     [] = []
      filter⁺ {xs = x ∷ _} (Qx ∷ Qxs) with does (P? x)
      ... | false = filter⁺ Qxs
      ... | true  = Qx ∷ filter⁺ Qxs

      filter⁻ : All Q (filter P? xs) → All Q (filter (¬? ∘ P?) xs) → All Q xs
      filter⁻ {xs = []}          []          []                         = []
      filter⁻ {xs = x ∷ _}       all⁺        all⁻ with P? x  | ¬? (P? x)
      filter⁻ {xs = x ∷ _}       all⁺        all⁻  | yes  Px | yes  ¬Px = contradiction Px ¬Px
      filter⁻ {xs = x ∷ _} (qx ∷ all⁺)       all⁻  | yes  Px | no  ¬¬Px = qx ∷ filter⁻ all⁺ all⁻
      filter⁻ {xs = x ∷ _}       all⁺  (qx ∷ all⁻) | no    _ | yes  ¬Px = qx ∷ filter⁻ all⁺ all⁻
      filter⁻ {xs = x ∷ _}       all⁺        all⁻  | no  ¬Px | no  ¬¬Px = contradiction ¬Px ¬¬Px

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

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

      partition-All : ∀ xs → (let ys , zs = partition P? xs) →
                      All P ys × All (∁ P) zs
      partition-All xs rewrite List.partition-defn P? xs =
        all-filter P? xs , all-filter (∁? P?) xs

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

    module _ {R : A → A → Set q} (R? : B.Decidable R) where

      derun⁺ : All P xs → All P (derun R? xs)
      derun⁺ {xs = []}         []                 = []
      derun⁺ {xs = x ∷ []}     (px ∷ [])          = px ∷ []
      derun⁺ {xs = x ∷ y ∷ xs} (px ∷ all[P,y∷xs]) with does (R? x y)
      ... | false = px ∷ derun⁺ all[P,y∷xs]
      ... | true  = derun⁺ all[P,y∷xs]

      deduplicate⁺ : All P xs → All P (deduplicate R? xs)
      deduplicate⁺ []         = []
      deduplicate⁺ (px ∷ pxs) = px ∷ filter⁺ (¬? ∘ R? _) (deduplicate⁺ pxs)

      derun⁻ : P B.Respects (flip R) → ∀ xs → All P (derun R? xs) → All P xs
      derun⁻ {P = P} P-resp-R []       []          = []
      derun⁻ {P = P} P-resp-R (x ∷ xs) all[P,x∷xs] = aux x xs all[P,x∷xs]
        where
        aux : ∀ x xs → All P (derun R? (x ∷ xs)) → All P (x ∷ xs)
        aux x []       (px ∷ []) = px ∷ []
        aux x (y ∷ xs) all[P,x∷y∷xs] with R? x y
        aux x (y ∷ xs) all[P,y∷xs]        | yes Rxy
          with r@(py ∷ _) ← aux y xs all[P,y∷xs] = P-resp-R Rxy py ∷ r
        aux x (y ∷ xs) (px ∷ all[P,y∷xs]) | no _ = px ∷ aux y xs all[P,y∷xs]

      deduplicate⁻ : P B.Respects R → ∀ xs → All P (deduplicate R? xs) → All P xs
      deduplicate⁻ {P = P} resp []       [] = []
      deduplicate⁻ {P = P} resp (x ∷ xs) (px ∷ pxs!) =
        px ∷ deduplicate⁻ resp xs (filter⁻ (¬? ∘ R? x) pxs! (All.tabulate aux))
        where
        aux : ∀ {z} → z ∈ filter (¬? ∘ ¬? ∘ R? x) (deduplicate R? xs) → P z
        aux {z = z} z∈filter = resp (decidable-stable (R? x z)
          (Product.proj₂ (∈-filter⁻ (¬? ∘ ¬? ∘ R? x) {z} {deduplicate R? xs} z∈filter))) px

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

    zipWith⁺ : ∀ (f : A → B → C) → Pointwise (λ x y → P (f x y)) xs ys →
               All P (zipWith f xs ys)
    zipWith⁺ f []              = []
    zipWith⁺ f (Pfxy ∷ Pfxsys) = Pfxy ∷ zipWith⁺ f Pfxsys

    ------------------------------------------------------------------------
    -- Operations for constructing lists
    ------------------------------------------------------------------------
    -- fromMaybe

    fromMaybe⁺ : ∀ {mx} → Maybe.All P mx → All P (fromMaybe mx)
    fromMaybe⁺ (just px) = px ∷ []
    fromMaybe⁺ nothing   = []

    fromMaybe⁻ : ∀ mx → All P (fromMaybe mx) → Maybe.All P mx
    fromMaybe⁻ (just x) (px ∷ []) = just px
    fromMaybe⁻ nothing  p         = nothing

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

    replicate⁺ : ∀ n → P x → All P (replicate n x)
    replicate⁺ zero    px = []
    replicate⁺ (suc n) px = px ∷ replicate⁺ n px

    replicate⁻ : ∀ {n} → All P (replicate (suc n) x) → P x
    replicate⁻ (px ∷ _) = px

    ------------------------------------------------------------------------
    -- inits

    inits⁺ : All P xs → All (All P) (inits xs)
    inits⁺ []         = [] ∷ []
    inits⁺ (px ∷ pxs) = [] ∷ gmap⁺ (px ∷_) (inits⁺ pxs)

    inits⁻ : ∀ xs → All (All P) (inits xs) → All P xs
    inits⁻ []               pxs                   = []
    inits⁻ (x ∷ [])         ([] ∷ p[x] ∷ [])      = p[x]
    inits⁻ (x ∷ xs@(_ ∷ _)) ([] ∷ pxs@(p[x] ∷ _)) =
      singleton⁻ p[x] ∷ inits⁻ xs (All.map (drop⁺ 1) (map⁻ pxs))

    ------------------------------------------------------------------------
    -- tails

    tails⁺ : All P xs → All (All P) (tails xs)
    tails⁺ []             = [] ∷ []
    tails⁺ pxxs@(_ ∷ pxs) = pxxs ∷ tails⁺ pxs

    tails⁻ : ∀ xs → All (All P) (tails xs) → All P xs
    tails⁻ []       pxs        = []
    tails⁻ (x ∷ xs) (pxxs ∷ _) = pxxs

    ------------------------------------------------------------------------
    -- all

    module _ (p : A → Bool) where

      all⁺ : ∀ xs → T (all p xs) → All (T ∘ p) xs
      all⁺ []       _      = []
      all⁺ (x ∷ xs) px∷pxs =
        let px , pxs = Equivalence.to (T-∧ {p x}) px∷pxs
        in px ∷ all⁺ xs pxs

      all⁻ : All (T ∘ p) xs → T (all p xs)
      all⁻ []         = _
      all⁻ (px ∷ pxs) = Equivalence.from T-∧ (px , all⁻ pxs)

    ------------------------------------------------------------------------
    -- All is anti-monotone.

    anti-mono : xs Subset.⊆ ys → All P ys → All P xs
    anti-mono xs⊆ys pys = All.tabulate (lookup pys ∘ xs⊆ys)

    all-anti-mono : ∀ (p : A → Bool) → xs Subset.⊆ ys → T (all p ys) → T (all p xs)
    all-anti-mono p xs⊆ys = all⁻ p ∘ anti-mono xs⊆ys ∘ all⁺ p _

    ------------------------------------------------------------------------
    -- Interactions with pointwise equality
    ------------------------------------------------------------------------

    module _ (S : Setoid c ℓ) where

      open Setoid S
      open ≋ S

      respects : P B.Respects _≈_ → (All P) B.Respects _≋_
      respects p≈ []            []         = []
      respects p≈ (x≈y ∷ xs≈ys) (px ∷ pxs) = p≈ x≈y px ∷ respects p≈ xs≈ys pxs

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

    -- Version 1.3

    Any¬→¬All = Any¬⇒¬All
    {-# WARNING_ON_USAGE Any¬→¬All
    "Warning: Any¬→¬All was deprecated in v1.3.
    Please use Any¬⇒¬All instead."
    #-}

    -- Version 2.0

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

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

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

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

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

    -- Version 2.1

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

    -- Version 2.2

    takeWhile⁻ : (P? : Decidable P) → takeWhile P? xs ≡ xs → All P xs
    takeWhile⁻ {xs = xs} P? eq rewrite sym eq = all-takeWhile P? xs
    {-# WARNING_ON_USAGE takeWhile⁻
    "Warning: takeWhile⁻ was deprecated in v2.2.
    Please use all-takeWhile instead."
    #-}