module Universe where
open import Coinduction
open import Data.Product
open import Data.Stream
infixr 5 _∷_
infixr 4 _,_
data U : Set₁ where
lift : Set → U
stream : U → U
product : U → U → U
El : U → Set
El (lift A) = A
El (stream a) = Stream (El a)
El (product a b) = El a × El b
data ElP : U → Set₁ where
interleave : ∀ {a} → ElP (stream a) → ElP (stream a) → ElP (stream a)
fst : ∀ {a b} → ElP (product a b) → ElP a
snd : ∀ {a b} → ElP (product a b) → ElP b
data ElW : U → Set₁ where
_∷_ : ∀ {a} → ElW a → ElP (stream a) → ElW (stream a)
_,_ : ∀ {a b} → ElW a → ElW b → ElW (product a b)
⌈_⌉ : ∀ {A} → A → ElW (lift A)
interleaveW : ∀ {a} → ElW (stream a) → ElP (stream a) → ElW (stream a)
interleaveW (x ∷ xs) ys = x ∷ interleave ys xs
fstW : ∀ {a b} → ElW (product a b) → ElW a
fstW (x , y) = x
sndW : ∀ {a b} → ElW (product a b) → ElW b
sndW (x , y) = y
whnf : ∀ {a} → ElP a → ElW a
whnf (interleave xs ys) = interleaveW (whnf xs) ys
whnf (fst p) = fstW (whnf p)
whnf (snd p) = sndW (whnf p)
mutual
⟦_⟧W : ∀ {a} → ElW a → El a
⟦ x ∷ xs ⟧W = ⟦ x ⟧W ∷ ♯ ⟦ xs ⟧P
⟦ x , y ⟧W = (⟦ x ⟧W , ⟦ y ⟧W)
⟦ ⌈ x ⌉ ⟧W = x
⟦_⟧P : ∀ {a} → ElP a → El a
⟦ p ⟧P = ⟦ whnf p ⟧W