What could this strange type be isomorphic to?

WeirdIso.agda

module WeirdIso where

open import Coinduction
open import Data.Nat
open import Data.Stream
open import Relation.Binary.PropositionalEquality

data Weird : Set where
  A : (x :   Weird) → Weird
  B : (x : ∞ Weird) → Weird

data _≈W_ : Weird → Weird → Set where
  eqA : ∀ {x y} (p :      x ≈W   y) → A x ≈W A y
  eqB : ∀ {x y} (p : ∞ (♭ x ≈W ♭ y)) → B x ≈W B y

to : Weird → Stream ℕ
to (A x) with to x
to (A x) | y ∷ ys = suc y ∷ ys
to (B x) = zero ∷ ♯ to (♭ x)

from : Stream ℕ → Weird
from (zero ∷ xs) = B (♯ from (♭ xs))
from (suc x ∷ xs) = A (from (x ∷ xs))

to∘from≈id : ∀ x → to (from x) ≈ x
to∘from≈id (zero  ∷ xs) = refl ∷ ♯ to∘from≈id (♭ xs)
to∘from≈id (suc x ∷ xs) with to (from (x ∷ xs)) | to∘from≈id (x ∷ xs)
to∘from≈id (suc x ∷ xs) | ._ | p ∷ ps = cong suc p ∷ ps

from∘to≈id : ∀ x → from (to x) ≈W x
from∘to≈id (A x) with to x | from∘to≈id x
from∘to≈id (A x) | y ∷ ys | q = eqA q
from∘to≈id (B x) = eqB (♯ from∘to≈id (♭ x))

@Blaisorblade that's right, it's Stream ℕ! There are a lot of fun things one can do with mixed data/codata. See also my gist on infinite prime numbers that uses a fancier type to express that there's an infinite stream of primes with finite non-primes between them.