    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Streams where all elements satisfy a given property
    ------------------------------------------------------------------------

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

    module Codata.Guarded.Stream.Relation.Unary.All where

    open import Codata.Guarded.Stream using (Stream; head; tail)
    open import Data.Product.Base using (_,_; proj₁; proj₂)
    open import Level using (Level)
    open import Relation.Unary using (Pred; _∩_; _⊆_)

    private
      variable
        a p ℓ : Level
        A : Set a
        P Q R : Pred A p
        xs : Stream A

    infixr 5 _∷_

    record All (P : Pred A ℓ) (as : Stream A) : Set ℓ where
      coinductive
      constructor _∷_
      field
        head :     P (head as)
        tail : All P (tail as)

    open All public

    map : P ⊆ Q → All P ⊆ All Q
    head (map f xs) = f (head xs)
    tail (map f xs) = map f (tail xs)

    zipWith : P ∩ Q ⊆ R → All P ∩ All Q ⊆ All R
    head (zipWith f (ps , qs)) = f (head ps , head qs)
    tail (zipWith f (ps , qs)) = zipWith f (tail ps , tail qs)

    unzipWith : R ⊆ P ∩ Q → All R ⊆ All P ∩ All Q
    head (proj₁ (unzipWith f rs)) = proj₁ (f (head rs))
    tail (proj₁ (unzipWith f rs)) = proj₁ (unzipWith f (tail rs))
    head (proj₂ (unzipWith f rs)) = proj₂ (f (head rs))
    tail (proj₂ (unzipWith f rs)) = proj₂ (unzipWith f (tail rs))