# Pastebin uvJibPhV
open import Agda.Builtin.Size

record ⊤ : Set where constructor tt


record Stream {i : Size} {ℓ} (A : Set ℓ) : Set ℓ where
  constructor _,_
  coinductive
  field
    head : A
    tail : {j : Size< i} → Stream {j} A
open Stream public

repeat : ∀ {i ℓ} {A : Set ℓ} → A → Stream {i} A
head (repeat x) = x
tail (repeat x) = repeat x


record All {i : Size} {ℓ} (Â : Stream (Set ℓ)) : Set ℓ where
  constructor _,_
  coinductive
  field
    head : head Â
    tail : {j : Size< i} → All (tail Â)
open All public

ex : All (repeat ⊤)
head ex = tt
tail ex = ex


-- musical coinduction to make things easier...

open import Agda.Builtin.Coinduction

data Any {i ℓ} (Â : Stream (Set ℓ)) : Set ℓ where
  inl : head  → Any Â
  inr : {j : Size< i} → ∞ (Any {j} (tail Â)) → Any Â

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

fromNat : Nat → Any (repeat ⊤)
fromNat zero = inl tt
fromNat (suc n) = inr (♯ fromNat n)

toNat : ∀ {i} → Any {i} (repeat ⊤) → Nat
toNat (inl tt) = zero
toNat (inr n) = suc (toNat (♭ n))

toFromNat : (n : Nat) → toNat (fromNat n) ≡ n
toFromNat zero = refl
toFromNat (suc n) rewrite toFromNat n = refl

fromToNat : ∀ {i} (x : Any {i} (repeat ⊤)) → fromNat (toNat x) ≡ x
fromToNat (inl tt) = refl
fromToNat (inr x) = {!!} -- ???