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

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

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

    open import Axiom.Extensionality.Propositional using (Extensionality)
    open import Data.Bool.Base using (true; false)
    open import Data.List.Base using (List; []; _∷_)
    open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
    open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
    open import Data.Product.Base as Product using (_,_)
    open import Function.Base using (_∘_; _$_)
    open import Function.Bundles using (_↠_; mk↠ₛ; _⇔_; mk⇔)
    open import Level using (Level)
    open import Relation.Binary.Core using (REL)
    open import Relation.Binary.PropositionalEquality.Core
      using (_≡_; refl; cong; cong₂)
    open import Relation.Nullary.Reflects using (invert)
    open import Relation.Nullary.Negation.Core using (¬_; contradiction)
    open import Relation.Nullary.Decidable.Core using (_because_)
    open import Relation.Unary using (Decidable; Pred; Universal)

    private
      variable
        a b p ℓ : Level
        A : Set a
        B : Set b
        P : Pred A p
        x y : A
        xs ys : List A

    ------------------------------------------------------------------------
    -- Lemmas relating Any, All and negation.

    ¬Any⇒All¬ : ∀ xs → ¬ Any P xs → All (¬_ ∘ P) xs
    ¬Any⇒All¬ []       ¬p = []
    ¬Any⇒All¬ (x ∷ xs) ¬p = ¬p ∘ here ∷ ¬Any⇒All¬ xs (¬p ∘ there)

    All¬⇒¬Any : ∀ {xs} → All (¬_ ∘ P) xs → ¬ Any P xs
    All¬⇒¬Any (¬p ∷ _)  (here  p) = ¬p p
    All¬⇒¬Any (_  ∷ ¬p) (there p) = All¬⇒¬Any ¬p p

    ¬All⇒Any¬ : Decidable P → ∀ xs → ¬ All P xs → Any (¬_ ∘ P) xs
    ¬All⇒Any¬ dec []       ¬∀ = contradiction [] ¬∀
    ¬All⇒Any¬ dec (x ∷ xs) ¬∀ with dec x
    ... |  true because  [p] = there (¬All⇒Any¬ dec xs (¬∀ ∘ _∷_ (invert [p])))
    ... | false because [¬p] = here (invert [¬p])

    Any¬⇒¬All : ∀ {xs} → Any (¬_ ∘ P) xs → ¬ All P xs
    Any¬⇒¬All (here  ¬p) = ¬p           ∘ All.head
    Any¬⇒¬All (there ¬p) = Any¬⇒¬All ¬p ∘ All.tail

    ¬Any↠All¬ : ∀ {xs} → (¬ Any P xs) ↠ All (¬_ ∘ P) xs
    ¬Any↠All¬ = mk↠ₛ {to = ¬Any⇒All¬ _} (λ y → All¬⇒¬Any y , to∘from y)
      where
      to∘from : ∀ {xs} (¬p : All (¬_ ∘ P) xs) → ¬Any⇒All¬ xs (All¬⇒¬Any ¬p) ≡ ¬p
      to∘from []         = refl
      to∘from (¬p ∷ ¬ps) = cong₂ _∷_ refl (to∘from ¬ps)

      -- If equality of functions were extensional, then the surjection
      -- could be strengthened to a bijection.

      from∘to : Extensionality _ _ →
                ∀ xs → (¬p : ¬ Any P xs) → All¬⇒¬Any (¬Any⇒All¬ xs ¬p) ≡ ¬p
      from∘to ext []       ¬p = ext λ ()
      from∘to ext (x ∷ xs) ¬p = ext λ
        { (here p)  → refl
        ; (there p) → cong (λ f → f p) $ from∘to ext xs (¬p ∘ there)
        }

    Any¬⇔¬All : ∀ {xs} → Decidable P → Any (¬_ ∘ P) xs ⇔ (¬ All P xs)
    Any¬⇔¬All dec = mk⇔ Any¬⇒¬All (¬All⇒Any¬ dec _)

    private
      -- If equality of functions were extensional, then the logical
      -- equivalence could be strengthened to a surjection.
      to∘from : Extensionality _ _ → (dec : Decidable P) →
                (¬∀ : ¬ All P xs) → Any¬⇒¬All (¬All⇒Any¬ dec xs ¬∀) ≡ ¬∀
      to∘from ext P ¬∀ = ext λ ∀P → contradiction ∀P ¬∀

    module _ {_~_ : REL A B ℓ} where

      All-swap : ∀ {xs ys} →
                 All (λ x → All (x ~_) ys) xs →
                 All (λ y → All (_~ y) xs) ys
      All-swap {ys = []}     _   = []
      All-swap {ys = y ∷ ys} []  = All.universal (λ _ → []) (y ∷ ys)
      All-swap {ys = y ∷ ys} ((x~y ∷ x~ys) ∷ pxs) =
        (x~y ∷ (All.map All.head pxs)) ∷
        All-swap (x~ys ∷ (All.map All.tail pxs))