    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Universal lifting of predicates over Vectors
    ------------------------------------------------------------------------

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

    module Data.Vec.Functional.Relation.Unary.All where

    open import Data.Fin.Properties using (all?)
    open import Data.Product.Base using (_,_)
    open import Data.Vec.Functional as VF hiding (map)
    open import Level using (Level)
    open import Relation.Unary using (Pred; _⊆_; Decidable; Universal; Satisfiable)

    private
      variable
        a p q ℓ : Level
        A : Set a

    ------------------------------------------------------------------------
    -- Definition

    All : Pred A ℓ → ∀ {n} → Vector A n → Set ℓ
    All P xs = ∀ i → P (xs i)

    ------------------------------------------------------------------------
    -- Operations

    module _ {P : Pred A p} {Q : Pred A q} where

      map : P ⊆ Q → ∀ {n} → All P {n = n} ⊆ All Q
      map p⊆q ps i = p⊆q (ps i)

    ------------------------------------------------------------------------
    -- Properties of predicates preserved by All

    module _ {P : Pred A p} where

      all : Decidable P → ∀ {n} → Decidable (All P {n = n})
      all p? xs = all? λ i → p? (xs i)

      universal : Universal P → ∀ {n} → Universal (All P {n = n})
      universal uni xs i = uni (xs i)

      satisfiable : Satisfiable P → ∀ {n} → Satisfiable (All P {n = n})
      satisfiable (x , px) = (λ _ → x) , (λ _ → px)