From Topology via logic
{-# OPTIONS --safe --without-K --guardedness --no-exact-split #-} module ag-000D where open import MLTT.Spartan open import MLTT.List
Stream can be defined as a coinductive record.
record Stream (A : 𝓤 ̇ ) : 𝓤 ̇ where coinductive constructor _∷_ field head : A tail : Stream A open Stream
For example a stream of all zero.
zeros : Stream 𝟚 head zeros = ₀ tail zeros = zeros
s ⊨starts o defines a relation that a stream can be
realized by a finite observation.
_⊨starts_ : Stream 𝟚 → List 𝟚 → 𝓤₀ ̇ s ⊨starts [] = ₀ ＝ ₀ s ⊨starts (x ∷ xs) = (x ＝ head s) × (tail s ⊨starts xs)
For example, the first bit zeros produces is
₀.
first-bit : zeros ⊨starts [ ₀ ] first-bit = refl , refl
Every stream can be realized by “no” observation.
realize-by-no-observation : (s : Stream 𝟚) → s ⊨starts [] realize-by-no-observation s = refl
We can define order relation for these finite observations.
_⊇_ : List 𝟚 → List 𝟚 → 𝓤₀ ̇ _ ⊇ [] = ₀ ＝ ₀ [] ⊇ _ = 𝟘 (x ∷ l) ⊇ (x₁ ∷ l2) = (x ＝ x₁) × (l ⊇ l2)
This order has antisymmetric
eq-condition : (l1 l2 : List 𝟚) → l1 ⊇ l2 → l2 ⊇ l1 → l1 ＝ l2 eq-condition [] [] p q = refl eq-condition (x ∷ l1) (y ∷ l2) (ph , pt) (qh , qt) = x ∷ l1 ＝⟨ ap (_∷ l1) ph ⟩ y ∷ l1 ＝⟨ ap (y ∷_) (eq-condition l1 l2 pt qt) ⟩ y ∷ l2 ∎
, in fact total, which means a boring order. The order induces refinement of observations: if a observation is subsequence of another observation that realise the stream, then the stream also be realized by this subsequence.
refine-observation : {s : Stream 𝟚} → (l l2 : List 𝟚) → s ⊨starts l → l ⊇ l2 → s ⊨starts l2 refine-observation l2 [] _ _ = refl refine-observation (x ∷ l) (y ∷ l2) (x=head , tail) (x=y , rest) = (x=y ⁻¹ ∙ x=head) , refine-observation l l2 tail rest