```------------------------------------------------------------------------
-- Colists
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Colist where

open import Conat using (Conat; zero; suc; force; infinity)
open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude

open import Function-universe equality-with-J hiding (id; _∘_)

------------------------------------------------------------------------
-- The type

-- Colists.

mutual

infixr 5 _∷_

data Colist {a} (A : Set a) (i : Size) : Set a where
[]  : Colist A i
_∷_ : A → Colist′ A i → Colist A i

record Colist′ {a} (A : Set a) (i : Size) : Set a where
coinductive
field
force : {j : Size< i} → Colist A j

open Colist′ public

------------------------------------------------------------------------
-- Some operations

-- A variant of cons.

infixr 5 _∷′_

_∷′_ : ∀ {i a} {A : Set a} → A → Colist A i → Colist A i
x ∷′ xs = x ∷ λ { .force → xs }

-- The colist's tail, if any.

tail : ∀ {a} {A : Set a} {i} → Colist A i → Colist′ A i
tail xs@[]    = λ { .force → xs }
tail (x ∷ xs) = xs

-- A map function.

map : ∀ {a b i} {A : Set a} {B : Set b} →
(A → B) → Colist A i → Colist B i
map f []       = []
map f (x ∷ xs) = f x ∷ λ { .force → map f (force xs) }

-- The colist replicate n x contains exactly n copies of x (and
-- nothing else).

replicate : ∀ {a i} {A : Set a} → Conat i → A → Colist A i
replicate zero    x = []
replicate (suc n) x = x ∷ λ { .force → replicate (force n) x }

-- Repeats the given element indefinitely.

repeat : ∀ {a i} {A : Set a} → A → Colist A i
repeat = replicate infinity

-- Appends one colist to another.

infixr 5 _++_

_++_ : ∀ {a i} {A : Set a} → Colist A i → Colist A i → Colist A i
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ λ { .force → force xs ++ ys }

------------------------------------------------------------------------
-- Bisimilarity

-- [ ∞ ] xs ∼ ys means that xs and ys are "equal".

mutual

infix 4 [_]_∼_ [_]_∼′_

data [_]_∼_ {a} {A : Set a} (i : Size) :
Colist A ∞ → Colist A ∞ → Set a where
[]  : [ i ] [] ∼ []
_∷_ : ∀ {x y xs ys} →
x ≡ y → [ i ] force xs ∼′ force ys → [ i ] x ∷ xs ∼ y ∷ ys

record [_]_∼′_ {a} {A : Set a} (i : Size)
(xs ys : Colist A ∞) : Set a where
coinductive
field
force : {j : Size< i} → [ j ] xs ∼ ys

open [_]_∼′_ public

-- Bisimilarity is an equivalence relation.

reflexive-∼ : ∀ {i a} {A : Set a}
(xs : Colist A ∞) → [ i ] xs ∼ xs
reflexive-∼ []       = []
reflexive-∼ (x ∷ xs) = refl ∷ λ { .force → reflexive-∼ (force xs) }

symmetric-∼ : ∀ {i a} {A : Set a} {xs ys : Colist A ∞} →
[ i ] xs ∼ ys → [ i ] ys ∼ xs
symmetric-∼ []        = []
symmetric-∼ (p₁ ∷ p₂) = sym p₁ ∷ λ { .force → symmetric-∼ (force p₂) }

transitive-∼ : ∀ {i a} {A : Set a} {xs ys zs : Colist A ∞} →
[ i ] xs ∼ ys → [ i ] ys ∼ zs → [ i ] xs ∼ zs
transitive-∼ []        []        = []
transitive-∼ (p₁ ∷ p₂) (q₁ ∷ q₂) =
trans p₁ q₁ ∷ λ { .force → transitive-∼ (force p₂) (force q₂) }

-- A property relating Colist._∷_ and _∷′_.

∷∼∷′ : ∀ {i a} {A : Set a} {x : A} {xs} →
[ i ] x ∷ xs ∼ x ∷′ force xs
∷∼∷′ = refl ∷ λ { .force → reflexive-∼ _ }

------------------------------------------------------------------------
-- The ◇ predicate

-- ◇ ∞ P xs means that P holds for some element in xs.

data ◇ {a p} {A : Set a} (i : Size)
(P : A → Set p) : Colist A ∞ → Set (a ⊔ p) where
here  : ∀ {x xs} → P x → ◇ i P (x ∷ xs)
there : ∀ {x xs} {j : Size< i} → ◇ j P (force xs) → ◇ i P (x ∷ xs)

-- ◇ respects bisimilarity.

◇-∼ :
∀ {a p i} {A : Set a} {P : A → Set p} {xs ys} →
[ ∞ ] xs ∼ ys → ◇ i P xs → ◇ i P ys
◇-∼ (refl ∷ _) (here p)  = here p
◇-∼ (_    ∷ b) (there p) = there (◇-∼ (force b) p)

-- A map function for ◇.

◇-map : ∀ {a p q i} {A : Set a} {P : A → Set p} {Q : A → Set q} →
(∀ {x} → P x → Q x) →
(∀ {xs} → ◇ i P xs → ◇ i Q xs)
◇-map f (here p)  = here (f p)
◇-map f (there p) = there (◇-map f p)

-- A variant of ◇-map.

◇-map′ : ∀ {a b p q i}
{A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q}
{f : A → B} →
(∀ {x} → P x → Q (f x)) →
(∀ {xs} → ◇ i P xs → ◇ i Q (map f xs))
◇-map′ g (here p)  = here (g p)
◇-map′ g (there p) = there (◇-map′ g p)

-- If a predicate holds for some element in a colist, then it holds
-- for some value.

◇-witness : ∀ {a p i} {A : Set a} {P : A → Set p} {xs} →
◇ i P xs → ∃ P
◇-witness (here p)  = _ , p
◇-witness (there p) = ◇-witness p

-- If const P holds for some element, then P holds.

◇-const : ∀ {a p i} {A : Set a} {P : Set p} {xs : Colist A ∞} →
◇ i (const P) xs → P
◇-const = proj₂ ∘ ◇-witness

-- Colist membership.

infix 4 [_]_∈_

[_]_∈_ : ∀ {a} {A : Set a} → Size → A → Colist A ∞ → Set a
[ i ] x ∈ xs = ◇ i (x ≡_) xs

-- A generalisation of "◇ ∞ P xs holds iff P holds for some element in
-- xs".

◇⇔∈× : ∀ {a p i} {A : Set a} {P : A → Set p} {xs} →
◇ i P xs ⇔ ∃ λ x → [ i ] x ∈ xs × P x
◇⇔∈× {P = P} = record { to = to; from = from }
where
to : ∀ {i xs} → ◇ i P xs → ∃ λ x → [ i ] x ∈ xs × P x
to (here p)  = _ , here refl , p
to (there p) = Σ-map id (Σ-map there id) (to p)

from : ∀ {i xs} → (∃ λ x → [ i ] x ∈ xs × P x) → ◇ i P xs
from (x , here refl  , p) = here p
from (x , there x∈xs , p) = there (from (x , x∈xs , p))

------------------------------------------------------------------------
-- The □ predicate

-- □ ∞ P xs means that P holds for every element in xs.

mutual

data □ {a p} {A : Set a} (i : Size)
(P : A → Set p) : Colist A ∞ → Set (a ⊔ p) where
[]  : □ i P []
_∷_ : ∀ {x xs} → P x → □′ i P (force xs) → □ i P (x ∷ xs)

record □′ {a p} {A : Set a} (i : Size)
(P : A → Set p) (xs : Colist A ∞) : Set (a ⊔ p) where
coinductive
field
force : {j : Size< i} → □ j P xs

open □′ public

-- Some projections.

□-head : ∀ {a p i} {A : Set a} {P : A → Set p} {x xs} →
□ i P (x ∷ xs) → P x
□-head (p ∷ _) = p

□-tail : ∀ {a p i} {j : Size< i} {A : Set a} {P : A → Set p} {x xs} →
□ i P (x ∷ xs) → □ j P (force xs)
□-tail (_ ∷ ps) = force ps

-- □ respects bisimilarity.

□-∼ :
∀ {i a p} {A : Set a} {P : A → Set p} {xs ys} →
[ i ] xs ∼ ys → □ i P xs → □ i P ys
□-∼ []         _        = []
□-∼ (refl ∷ b) (p ∷ ps) = p ∷ λ { .force → □-∼ (force b) (force ps) }

-- A generalisation of "□ ∞ P xs holds iff P is true for every element
-- in xs".

□⇔∈→ : ∀ {a p i} {A : Set a} {P : A → Set p} {xs} →
□ i P xs ⇔ (∀ x → [ i ] x ∈ xs → P x)
□⇔∈→ {P = P} = record { to = to; from = from _ }
where
to : ∀ {i xs} → □ i P xs → (∀ x → [ i ] x ∈ xs → P x)
to (p ∷ ps) x (here refl)  = p
to (p ∷ ps) x (there x∈xs) = to (force ps) x x∈xs

from : ∀ {i} xs → (∀ x → [ i ] x ∈ xs → P x) → □ i P xs
from []       f = []
from (x ∷ xs) f =
f x (here refl) ∷ λ { .force → from (force xs) (λ x → f x ∘ there) }

-- If P is universally true, then □ i P is also universally true.

□-replicate : ∀ {a p i} {A : Set a} {P : A → Set p} →
(∀ x → P x) →
(∀ xs → □ i P xs)
□-replicate f _ = _⇔_.from □⇔∈→ (λ x _ → f x)

-- Something resembling applicative functor application for □.

infixl 4 _□-⊛_

_□-⊛_ : ∀ {i a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} {xs} →
□ i (λ x → P x → Q x) xs → □ i P xs → □ i Q xs
[]       □-⊛ _        = []
(f ∷ fs) □-⊛ (p ∷ ps) = f p ∷ λ { .force → force fs □-⊛ force ps }

-- A map function for □.

□-map : ∀ {a p q i} {A : Set a} {P : A → Set p} {Q : A → Set q} →
(∀ {x} → P x → Q x) →
(∀ {xs} → □ i P xs → □ i Q xs)
□-map f ps = □-replicate (λ _ → f) _ □-⊛ ps

-- A variant of □-map.

□-map′ : ∀ {a b p q i}
{A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q}
{f : A → B} →
(∀ {x} → P x → Q (f x)) →
(∀ {xs} → □ i P xs → □ i Q (map f xs))
□-map′ g []       = []
□-map′ g (p ∷ ps) = g p ∷ λ { .force → □-map′ g (force ps) }

-- Something resembling applicative functor application for □ and ◇.

infixl 4 _□◇-⊛_

_□◇-⊛_ : ∀ {a p q i} {A : Set a} {P : A → Set p} {Q : A → Set q} {xs} →
□ i (λ x → P x → Q x) xs → ◇ i P xs → ◇ i Q xs
(f ∷ _)  □◇-⊛ (here p)  = here (f p)
(_ ∷ fs) □◇-⊛ (there p) = there (force fs □◇-⊛ p)

-- A combination of some of the combinators above.

□◇-witness :
∀ {a p q i} {A : Set a} {P : A → Set p} {Q : A → Set q} {xs} →
□ i P xs → ◇ i Q xs → ∃ λ x → P x × Q x
□◇-witness p q = ◇-witness (□-map _,_ p □◇-⊛ q)

------------------------------------------------------------------------
-- A variant of ◇ with a sized predicate

-- ◇ˢ ∞ P xs means that (some instance of) P holds for some element in
-- xs.

data ◇ˢ {a p} {A : Set a} (i : Size)
(P : Size → A → Set p) : Colist A ∞ → Set (a ⊔ p) where
here  : ∀ {x xs} → P i x → ◇ˢ i P (x ∷ xs)
there : ∀ {x xs} {j : Size< i} → ◇ˢ j P (force xs) → ◇ˢ i P (x ∷ xs)

-- ◇ˢ respects bisimilarity.

◇ˢ-∼ :
∀ {a p i} {A : Set a} {P : Size → A → Set p} {xs ys} →
[ ∞ ] xs ∼ ys → ◇ˢ i P xs → ◇ˢ i P ys
◇ˢ-∼ (refl ∷ _) (here p)  = here p
◇ˢ-∼ (_    ∷ b) (there p) = there (◇ˢ-∼ (force b) p)

-- If P is upwards closed, then flip ◇ˢ P is upwards closed.

◇ˢ-upwards-closed :
∀ {a p} {A : Set a} {P : Size → A → Set p} →
(∀ {i} {j : Size< i} {x} → P j x → P i x) →
(∀ {i} {j : Size< i} {xs} → ◇ˢ j P xs → ◇ˢ i P xs)
◇ˢ-upwards-closed P-closed (here p)  = here (P-closed p)
◇ˢ-upwards-closed P-closed (there p) =
there (◇ˢ-upwards-closed P-closed p)

-- A variant of the previous lemma.

◇ˢ-upwards-closed-∞ :
∀ {a p} {A : Set a} {P : Size → A → Set p} →
(∀ {i x} → P i x → P ∞ x) →
(∀ {i xs} → ◇ˢ i P xs → ◇ˢ ∞ P xs)
◇ˢ-upwards-closed-∞ P-closed-∞ (here p)  = here (P-closed-∞ p)
◇ˢ-upwards-closed-∞ P-closed-∞ (there p) =
there (◇ˢ-upwards-closed-∞ P-closed-∞ p)

-- A map function for ◇ˢ.

◇ˢ-map : ∀ {a p q i}
{A : Set a} {P : Size → A → Set p} {Q : Size → A → Set q} →
(∀ {i x} → P i x → Q i x) →
(∀ {xs} → ◇ˢ i P xs → ◇ˢ i Q xs)
◇ˢ-map f (here p)  = here (f p)
◇ˢ-map f (there p) = there (◇ˢ-map f p)

-- A variant of ◇ˢ-map.

◇ˢ-map′ : ∀ {a b p q i} {A : Set a} {B : Set b}
{P : Size → A → Set p} {Q : Size → B → Set q} {f : A → B} →
(∀ {i x} → P i x → Q i (f x)) →
(∀ {xs} → ◇ˢ i P xs → ◇ˢ i Q (map f xs))
◇ˢ-map′ g (here p)  = here (g p)
◇ˢ-map′ g (there p) = there (◇ˢ-map′ g p)

-- If a predicate holds for some element in a colist, then it holds
-- for some value (assuming that P is upwards closed).

◇ˢ-witness : ∀ {a p i} {A : Set a} {P : Size → A → Set p} {xs} →
(∀ {i} {j : Size< i} {x} → P j x → P i x) →
◇ˢ i P xs → ∃ (P i)
◇ˢ-witness closed (here p)  = _ , p
◇ˢ-witness closed (there p) = Σ-map id closed (◇ˢ-witness closed p)

-- If P ∞ holds for some element in xs, then ◇ˢ ∞ P xs holds.

∈×∞→◇ˢ : ∀ {a p} {A : Set a} {P : Size → A → Set p} {x xs} →
[ ∞ ] x ∈ xs → P ∞ x → ◇ˢ ∞ P xs
∈×∞→◇ˢ (here refl)  p = here p
∈×∞→◇ˢ (there x∈xs) p = there (∈×∞→◇ˢ x∈xs p)

-- If P i x implies P ∞ x for any i and x, then ◇ˢ ∞ P xs holds iff
-- P ∞ holds for some element in xs.

◇ˢ⇔∈× : ∀ {a p} {A : Set a} {P : Size → A → Set p} {xs} →
(∀ {i x} → P i x → P ∞ x) →
◇ˢ ∞ P xs ⇔ (∃ λ x → [ ∞ ] x ∈ xs × P ∞ x)
◇ˢ⇔∈× {P = P} →∞ = record
{ to   = to
; from = λ { (_ , x∈xs , p) → ∈×∞→◇ˢ x∈xs p }
}
where
to : ∀ {i xs} → ◇ˢ i P xs → ∃ λ x → [ ∞ ] x ∈ xs × P ∞ x
to (here p)  = _ , here refl , →∞ p
to (there p) = Σ-map id (Σ-map there id) (to p)

-- Sized variants of the previous lemma.

◇ˢ→∈× : ∀ {a p} {A : Set a} {P : Size → A → Set p} →
(∀ {i} {j : Size< i} {x} → P j x → P i x) →
∀ {i xs} → ◇ˢ i P xs → ∃ λ x → [ i ] x ∈ xs × P i x
◇ˢ→∈× closed (here p)  = _ , here refl , p
◇ˢ→∈× closed (there p) = Σ-map id (Σ-map there closed) (◇ˢ→∈× closed p)

∈×→◇ˢ : ∀ {a p} {A : Set a} {P : Size → A → Set p} →
(∀ {i} {j : Size< i} {x} → P i x → P j x) →
∀ {i x xs} → [ i ] x ∈ xs → P i x → ◇ˢ i P xs
∈×→◇ˢ closed (here refl)  p = here p
∈×→◇ˢ closed (there x∈xs) p = there (∈×→◇ˢ closed x∈xs (closed p))

-- ◇ ∞ (P ∞) is "contained in" ◇ˢ ∞ P.

◇∞→◇ˢ∞ : ∀ {a p} {A : Set a} {P : Size → A → Set p} {xs} →
◇ ∞ (P ∞) xs → ◇ˢ ∞ P xs
◇∞→◇ˢ∞ {P = P} {xs} =
◇ ∞ (P ∞) xs                    ↝⟨ _⇔_.to ◇⇔∈× ⟩
(∃ λ x → [ ∞ ] x ∈ xs × P ∞ x)  ↝⟨ (λ { (_ , x∈xs , p) → ∈×∞→◇ˢ x∈xs p }) ⟩□
◇ˢ ∞ P xs                       □

-- If P i x implies P ∞ x for any i and x, then ◇ˢ ∞ P is pointwise
-- logically equivalent to ◇ ∞ (P ∞).

◇ˢ∞⇔◇∞ : ∀ {a p} {A : Set a} {P : Size → A → Set p} {xs} →
(∀ {i x} → P i x → P ∞ x) →
◇ˢ ∞ P xs ⇔ ◇ ∞ (P ∞) xs
◇ˢ∞⇔◇∞ {P = P} {xs} →∞ =
◇ˢ ∞ P xs                       ↝⟨ ◇ˢ⇔∈× →∞ ⟩
(∃ λ x → [ ∞ ] x ∈ xs × P ∞ x)  ↝⟨ inverse ◇⇔∈× ⟩□
◇ ∞ (P ∞) xs                    □

-- ◇ˢ i (const P) is pointwise logically equivalent to ◇ i P.

◇ˢ⇔◇ : ∀ {a p i} {A : Set a} {P : A → Set p} {xs} →
◇ˢ i (const P) xs ⇔ ◇ i P xs
◇ˢ⇔◇ {P = P} {xs} = record { to = to; from = from }
where
to : ∀ {i xs} → ◇ˢ i (const P) xs → ◇ i P xs
to (here p)  = here p
to (there p) = there (to p)

from : ∀ {i xs} → ◇ i P xs → ◇ˢ i (const P) xs
from (here p)  = here p
from (there p) = there (from p)

------------------------------------------------------------------------
-- A variant of □ with a sized predicate

-- □ˢ ∞ P xs means that (some instance of) P holds for every element
-- in xs.

mutual

data □ˢ {a p} {A : Set a} (i : Size)
(P : Size → A → Set p) : Colist A ∞ → Set (a ⊔ p) where
[]  : □ˢ i P []
_∷_ : ∀ {x xs} → P i x → □ˢ′ i P (force xs) → □ˢ i P (x ∷ xs)

record □ˢ′ {a p} {A : Set a} (i : Size)
(P : Size → A → Set p) (xs : Colist A ∞) : Set (a ⊔ p) where
coinductive
field
force : {j : Size< i} → □ˢ j P xs

open □ˢ′ public

-- Some projections.

□ˢ-head : ∀ {a p i} {A : Set a} {P : Size → A → Set p} {x xs} →
□ˢ i P (x ∷ xs) → P i x
□ˢ-head (p ∷ _) = p

□ˢ-tail : ∀ {a p i} {j : Size< i}
{A : Set a} {P : Size → A → Set p} {x xs} →
□ˢ i P (x ∷ xs) → □ˢ j P (force xs)
□ˢ-tail (_ ∷ ps) = force ps

-- □ˢ respects bisimilarity.

□ˢ-∼ :
∀ {i a p} {A : Set a} {P : Size → A → Set p} {xs ys} →
[ i ] xs ∼ ys → □ˢ i P xs → □ˢ i P ys
□ˢ-∼ []         _        = []
□ˢ-∼ (refl ∷ b) (p ∷ ps) = p ∷ λ { .force → □ˢ-∼ (force b) (force ps) }

-- If P is downwards closed, then flip □ˢ P is downwards closed.

□ˢ-downwards-closed :
∀ {a p} {A : Set a} {P : Size → A → Set p} →
(∀ {i} {j : Size< i} {x} → P i x → P j x) →
(∀ {i} {j : Size< i} {xs} → □ˢ i P xs → □ˢ j P xs)
□ˢ-downwards-closed P-closed []       = []
□ˢ-downwards-closed P-closed (p ∷ ps) =
P-closed p ∷ λ { .force → □ˢ-downwards-closed P-closed (force ps) }

-- A variant of the previous lemma.

□ˢ-downwards-closed-∞ :
∀ {a p} {A : Set a} {P : Size → A → Set p} →
(∀ {i x} → P ∞ x → P i x) →
(∀ {i xs} → □ˢ ∞ P xs → □ˢ i P xs)
□ˢ-downwards-closed-∞ P-closed-∞ []       = []
□ˢ-downwards-closed-∞ P-closed-∞ (p ∷ ps) =
P-closed-∞ p ∷ λ { .force →
□ˢ-downwards-closed-∞ P-closed-∞ (force ps) }

-- If □ˢ ∞ P xs holds, then P ∞ holds for every element in xs.

□ˢ∞∈→ : ∀ {a p} {A : Set a} {P : Size → A → Set p} {xs x} →
□ˢ ∞ P xs → [ ∞ ] x ∈ xs → P ∞ x
□ˢ∞∈→ (p ∷ ps) (here refl)  = p
□ˢ∞∈→ (p ∷ ps) (there x∈xs) = □ˢ∞∈→ (force ps) x∈xs

-- If P ∞ x implies P i x for any i and x, then □ˢ ∞ P xs holds iff P ∞
-- holds for every element in xs.

□ˢ⇔∈→ : ∀ {a p} {A : Set a} {P : Size → A → Set p} {xs} →
(∀ {i x} → P ∞ x → P i x) →
□ˢ ∞ P xs ⇔ (∀ x → [ ∞ ] x ∈ xs → P ∞ x)
□ˢ⇔∈→ {P = P} ∞→ = record { to = λ p _ → □ˢ∞∈→ p; from = from _ }
where
from : ∀ {i} xs → (∀ x → [ ∞ ] x ∈ xs → P ∞ x) → □ˢ i P xs
from []       f = []
from (x ∷ xs) f =
∞→ (f x (here refl)) ∷ λ { .force →
from (force xs) (λ x → f x ∘ there) }

-- Sized variants of the previous lemma.

□ˢ∈→ : ∀ {a p} {A : Set a} {P : Size → A → Set p} →
(∀ {i} {j : Size< i} {x} → P j x → P i x) →
∀ {i x xs} → □ˢ i P xs → [ i ] x ∈ xs → P i x
□ˢ∈→ closed (p ∷ ps) (here refl)  = p
□ˢ∈→ closed (p ∷ ps) (there x∈xs) = closed (□ˢ∈→ closed (force ps) x∈xs)

∈→→□ˢ : ∀ {a p} {A : Set a} {P : Size → A → Set p} →
(∀ {i} {j : Size< i} {x} → P i x → P j x) →
∀ {i} xs → (∀ x → [ i ] x ∈ xs → P i x) → □ˢ i P xs
∈→→□ˢ closed []       f = []
∈→→□ˢ closed (x ∷ xs) f =
f x (here refl) ∷ λ { .force →
∈→→□ˢ closed (force xs) (λ x → closed ∘ f x ∘ there) }

-- □ˢ ∞ P is "contained in" □ ∞ (P ∞).

□ˢ∞→□∞ : ∀ {a p} {A : Set a} {P : Size → A → Set p} {xs} →
□ˢ ∞ P xs → □ ∞ (P ∞) xs
□ˢ∞→□∞ {P = P} {xs} =
□ˢ ∞ P xs                     ↝⟨ (λ p _ → □ˢ∞∈→ p) ⟩
(∀ x → [ ∞ ] x ∈ xs → P ∞ x)  ↝⟨ _⇔_.from □⇔∈→ ⟩□
□ ∞ (P ∞) xs                  □

-- If P ∞ x implies P i x for any i and x, then □ˢ ∞ P is pointwise
-- logically equivalent to □ ∞ (P ∞).

□ˢ∞⇔□∞ : ∀ {a p} {A : Set a} {P : Size → A → Set p} {xs} →
(∀ {i x} → P ∞ x → P i x) →
□ˢ ∞ P xs ⇔ □ ∞ (P ∞) xs
□ˢ∞⇔□∞ {P = P} {xs} ∞→ =
□ˢ ∞ P xs                     ↝⟨ □ˢ⇔∈→ ∞→ ⟩
(∀ x → [ ∞ ] x ∈ xs → P ∞ x)  ↝⟨ inverse □⇔∈→ ⟩□
□ ∞ (P ∞) xs                  □

-- □ˢ i (const P) is pointwise logically equivalent to □ i P.

□ˢ⇔□ : ∀ {a p i} {A : Set a} {P : A → Set p} {xs} →
□ˢ i (const P) xs ⇔ □ i P xs
□ˢ⇔□ {P = P} {xs} = record { to = to; from = from }
where
to : ∀ {i xs} → □ˢ i (const P) xs → □ i P xs
to []       = []
to (p ∷ ps) = p ∷ λ { .force → to (force ps) }

from : ∀ {i xs} → □ i P xs → □ˢ i (const P) xs
from []       = []
from (p ∷ ps) = p ∷ λ { .force → from (force ps) }

-- If P is universally true, then □ˢ i P is also universally true.

□ˢ-replicate : ∀ {a p i} {A : Set a} {P : Size → A → Set p} →
(∀ {i} x → P i x) →
(∀ xs → □ˢ i P xs)
□ˢ-replicate f []       = []
□ˢ-replicate f (x ∷ xs) = f x ∷ λ { .force → □ˢ-replicate f (force xs) }

-- Something resembling applicative functor application for □ˢ.

infixl 4 _□ˢ-⊛_

_□ˢ-⊛_ : ∀ {i a p q} {A : Set a}
{P : Size → A → Set p} {Q : Size → A → Set q} {xs} →
□ˢ i (λ j x → P j x → Q j x) xs → □ˢ i P xs → □ˢ i Q xs
[]       □ˢ-⊛ _        = []
(f ∷ fs) □ˢ-⊛ (p ∷ ps) = f p ∷ λ { .force → force fs □ˢ-⊛ force ps }

-- A map function for □ˢ.

□ˢ-map : ∀ {a p q i}
{A : Set a} {P : Size → A → Set p} {Q : Size → A → Set q} →
(∀ {i x} → P i x → Q i x) →
(∀ {xs} → □ˢ i P xs → □ˢ i Q xs)
□ˢ-map f ps = □ˢ-replicate (λ _ → f) _ □ˢ-⊛ ps

-- A variant of □ˢ-map.

□ˢ-map′ : ∀ {a b p q i} {A : Set a} {B : Set b}
{P : Size → A → Set p} {Q : Size → B → Set q} {f : A → B} →
(∀ {i x} → P i x → Q i (f x)) →
(∀ {xs} → □ˢ i P xs → □ˢ i Q (map f xs))
□ˢ-map′ g []       = []
□ˢ-map′ g (p ∷ ps) = g p ∷ λ { .force → □ˢ-map′ g (force ps) }

-- Something resembling applicative functor application for □ˢ and ◇ˢ.

infixl 4 _□ˢ◇ˢ-⊛_

_□ˢ◇ˢ-⊛_ : ∀ {a p q i} {A : Set a}
{P : Size → A → Set p} {Q : Size → A → Set q} {xs} →
□ˢ i (λ j x → P j x → Q j x) xs → ◇ˢ i P xs → ◇ˢ i Q xs
(f ∷ _)  □ˢ◇ˢ-⊛ (here p)  = here (f p)
(_ ∷ fs) □ˢ◇ˢ-⊛ (there p) = there (force fs □ˢ◇ˢ-⊛ p)

-- A combination of some of the combinators above.

□ˢ◇ˢ-witness :
∀ {a p q i}
{A : Set a} {P : Size → A → Set p} {Q : Size → A → Set q} {xs} →
(∀ {i} {j : Size< i} {x} → P j x → P i x) →
(∀ {i} {j : Size< i} {x} → Q j x → Q i x) →
□ˢ i P xs → ◇ˢ i Q xs → ∃ λ x → P i x × Q i x
□ˢ◇ˢ-witness P-closed Q-closed p q =
◇ˢ-witness (λ { {_} {_} → Σ-map P-closed Q-closed })
(□ˢ-map _,_ p □ˢ◇ˢ-⊛ q)
```