Instantly share code, notes, and snippets.

# copumpkin/WeirdIso.agda Created Mar 10, 2014

What could this strange type be isomorphic to?
 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 commented Nov 23, 2016 • edited

 What's the TL;DR. answer to the title question? Weird seems neither data nor codata since it mixes recursion and corecursion... EDIT: Sorry thinko, the types of `to` and `from` have the answer...
Owner Author

### copumpkin commented May 26, 2017

 @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.