{-# 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
open import Relation.Unary
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))