    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties of the Any predicate on colists
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --guardedness #-}

    module Codata.Musical.Colist.Relation.Unary.Any.Properties where

    open import Codata.Musical.Colist.Base
    open import Codata.Musical.Colist.Bisimilarity
    open import Codata.Musical.Colist.Relation.Unary.Any
    open import Codata.Musical.Notation
    open import Data.Maybe using (Is-just)
    open import Data.Maybe.Relation.Unary.Any using (just)
    open import Data.Nat.Base using (suc; _≥′_; ≤′-refl; ≤′-step)
    open import Data.Nat.Properties using (s≤′s)
    open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′; [_,_])
    open import Function.Base using (_∋_; _∘_)
    open import Function.Bundles
    open import Level using (Level; _⊔_)
    open import Relation.Binary.Bundles using (Setoid)
    open import Relation.Binary.PropositionalEquality.Core
      using (_≡_; refl; cong)
    open import Relation.Unary using (Pred)

    private
      variable
        a b p q : Level
        A : Set a
        B : Set b
        P : Pred A p
        Q : Pred A q

    ------------------------------------------------------------------------
    -- Equality properties

    here-injective : ∀ {x xs p q} → (Any P (x ∷ xs) ∋ here p) ≡ here q → p ≡ q
    here-injective refl = refl

    there-injective : ∀ {x xs p q} → (Any P (x ∷ xs) ∋ there p) ≡ there q → p ≡ q
    there-injective refl = refl

    Any-resp : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q}
               {xs ys} → (∀ {x} → P x → Q x) → xs ≈ ys →
               Any P xs → Any Q ys
    Any-resp f (x ∷ xs≈) (here px) = here (f px)
    Any-resp f (x ∷ xs≈) (there p) = there (Any-resp f (♭ xs≈) p)

    -- Any maps pointwise isomorphic predicates and equal colists to
    -- isomorphic types.

    Any-cong : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q}
               {xs ys} → (∀ {i} → P i ↔ Q i) → xs ≈ ys → Any P xs ↔ Any Q ys
    Any-cong {A = A} {P} {Q} {xs} {ys} P↔Q xs≈ys =
      mk↔ₛ′ (to xs≈ys) (from xs≈ys) (to∘from _) (from∘to _)
      where
      open Setoid (setoid _) using (sym)

      to : ∀ {xs ys} → xs ≈ ys → Any P xs → Any Q ys
      to xs≈ys = Any-resp (Inverse.to P↔Q) xs≈ys

      from : ∀ {xs ys} → xs ≈ ys → Any Q ys → Any P xs
      from xs≈ys = Any-resp (Inverse.from P↔Q) (sym xs≈ys)

      to∘from : ∀ {xs ys} (xs≈ys : xs ≈ ys) (q : Any Q ys) →
                to xs≈ys (from xs≈ys q) ≡ q
      to∘from (x ∷ xs≈) (there q) = cong there (to∘from (♭ xs≈) q)
      to∘from (x ∷ xs≈) (here qx) =
        cong here (Inverse.strictlyInverseˡ P↔Q qx)

      from∘to : ∀ {xs ys} (xs≈ys : xs ≈ ys) (p : Any P xs) →
                from xs≈ys (to xs≈ys p) ≡ p
      from∘to (x ∷ xs≈) (there p) = cong there (from∘to (♭ xs≈) p)
      from∘to (x ∷ xs≈) (here px) =
        cong here (Inverse.strictlyInverseʳ P↔Q px)

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

    module _ {f : A → B} where

      map⁻ : ∀ {xs} → Any P (map f xs) → Any (P ∘ f) xs
      map⁻ {xs = x ∷ xs} (here px) = here px
      map⁻ {xs = x ∷ xs} (there p) = there (map⁻ p)

      map⁺ : ∀ {xs} → Any (P ∘ f) xs → Any P (map f xs)
      map⁺ (here px) = here px
      map⁺ (there p) = there (map⁺ p)

      Any-map : ∀ {xs} → Any P (map f xs) ↔ Any (P ∘ f) xs
      Any-map {xs = xs} = mk↔ₛ′ map⁻ map⁺ to∘from from∘to
        where
        from∘to : ∀ {xs} (p : Any P (map f xs)) → map⁺ (map⁻ p) ≡ p
        from∘to {xs = x ∷ xs} (here px) = refl
        from∘to {xs = x ∷ xs} (there p) = cong there (from∘to p)

        to∘from : ∀ {xs} (p : Any (P ∘ f) xs) → map⁻ {P = P} (map⁺ p) ≡ p
        to∘from (here px) = refl
        to∘from (there p) = cong there (to∘from p)

    ------------------------------------------------------------------------
    -- _⋎_

    ⋎⁻ : ∀ xs {ys} → Any P (xs ⋎ ys) → Any P xs ⊎ Any P ys
    ⋎⁻ []       p         = inj₂ p
    ⋎⁻ (x ∷ xs) (here px) = inj₁ (here px)
    ⋎⁻ (x ∷ xs) (there p) = [ inj₂ , inj₁ ∘ there ]′ (⋎⁻ _ p)

    mutual

      ⋎⁺₁ : ∀ {xs ys} → Any P xs → Any P (xs ⋎ ys)
      ⋎⁺₁           (here px) = here px
      ⋎⁺₁ {ys = ys} (there p) = there (⋎⁺₂ ys p)

      ⋎⁺₂ : ∀ xs {ys} → Any P ys → Any P (xs ⋎ ys)
      ⋎⁺₂ []       p = p
      ⋎⁺₂ (x ∷ xs) p = there (⋎⁺₁ p)

    ⋎⁺ : ∀ xs {ys} → Any P xs ⊎ Any P ys → Any P (xs ⋎ ys)
    ⋎⁺ xs = [ ⋎⁺₁ , ⋎⁺₂ xs ]

    Any-⋎ : ∀ {a p} {A : Set a} {P : A → Set p} xs {ys} →
            Any P (xs ⋎ ys) ↔ (Any P xs ⊎ Any P ys)
    Any-⋎ {P = P} xs = mk↔ₛ′ (⋎⁻ xs) (⋎⁺ xs) (to∘from xs) (from∘to xs)
      where

      from∘to : ∀ xs {ys} (p : Any P (xs ⋎ ys)) → ⋎⁺ xs (⋎⁻ xs p) ≡ p
      from∘to []                 p                          = refl
      from∘to (x ∷ xs)           (here px)                  = refl
      from∘to (x ∷ xs) {ys = ys} (there p)                  with ⋎⁻ ys p | from∘to ys p
      from∘to (x ∷ xs) {ys = ys} (there .(⋎⁺₁ q))     | inj₁ q | refl = refl
      from∘to (x ∷ xs) {ys = ys} (there .(⋎⁺₂ ys q)) | inj₂ q | refl = refl

      mutual

        to∘from₁ : ∀ {xs ys} (p : Any P xs) →
                       ⋎⁻ xs {ys = ys} (⋎⁺₁ p) ≡ inj₁ p
        to∘from₁           (here px) = refl
        to∘from₁ {ys = ys} (there p)
          rewrite to∘from₂ ys p = refl

        to∘from₂ : ∀ xs {ys} (p : Any P ys) →
                        ⋎⁻ xs (⋎⁺₂ xs p) ≡ inj₂ p
        to∘from₂ []                 p = refl
        to∘from₂ (x ∷ xs) {ys = ys} p
          rewrite to∘from₁ {xs = ys} {ys = ♭ xs} p = refl

      to∘from : ∀ xs {ys} (p : Any P xs ⊎ Any P ys) → ⋎⁻ xs (⋎⁺ xs p) ≡ p
      to∘from xs = [ to∘from₁ , to∘from₂ xs ]

    ------------------------------------------------------------------------
    -- index

    -- The position returned by index is guaranteed to be within bounds.

    lookup-index : ∀ {xs} (p : Any P xs) → Is-just (lookup xs (index p))
    lookup-index (here px) = just _
    lookup-index (there p) = lookup-index p

    -- Any-resp preserves the index.

    index-Any-resp : ∀ {f : ∀ {x} → P x → Q x} {xs ys}
                     (xs≈ys : xs ≈ ys) (p : Any P xs) →
                     index (Any-resp f xs≈ys p) ≡ index p
    index-Any-resp (x ∷ xs≈) (here px) = refl
    index-Any-resp (x ∷ xs≈) (there p) =
      cong suc (index-Any-resp (♭ xs≈) p)

    -- The left-to-right direction of Any-⋎ returns a proof whose size is
    -- no larger than that of the input proof.

    index-Any-⋎ : ∀ xs {ys} (p : Any P (xs ⋎ ys)) →
                  index p ≥′ [ index , index ]′ (Inverse.to (Any-⋎ xs) p)
    index-Any-⋎ []                 p         = ≤′-refl
    index-Any-⋎ (x ∷ xs)           (here px) = ≤′-refl
    index-Any-⋎ (x ∷ xs) {ys = ys} (there p)
      with Inverse.to (Any-⋎ ys) p | index-Any-⋎ ys p
    ... | inj₁ q | q≤p = ≤′-step q≤p
    ... | inj₂ q | q≤p = s≤′s    q≤p