{-# OPTIONS --sized-types #-}
module Delay-monad.Sized.Always where
open import Prelude
open import Prelude.Size
open import Delay-monad.Sized
open import Delay-monad.Sized.Monad
mutual
data □ {a p} {A : Size → Type a} (i : Size) (P : A ∞ → Type p) :
Delay A ∞ → Type (a ⊔ p) where
now : ∀ {x} → P x → □ i P (now x)
later : ∀ {x} → □′ i P (force x) → □ i P (later x)
record □′ {a p} {A : Size → Type a} (i : Size) (P : A ∞ → Type p)
(x : Delay A ∞) : Type (a ⊔ p) where
coinductive
field
force : {j : Size< i} → □ j P x
open □′ public
□->>= :
∀ {i a b p q}
{A : Size → Type a} {B : Size → Type b}
{P : A ∞ → Type p} {Q : B ∞ → Type q}
{x : Delay A ∞} {f : ∀ {i} → A i → Delay B i} →
□ i P x → (∀ {x} → P x → □ i Q (f x)) → □ i Q (x >>= f)
□->>= (now P-x) □-f = □-f P-x
□->>= (later □-x) □-f = later λ { .force → □->>= (force □-x) □-f }