infnat.agda

data ω : Type₀ where
  zero : ω
  suc : ω → ω
  inf : ω
  suc-inf : suc inf ≡ inf

ω′ : Type₀
ω′ = Maybe ℕ

zero′ : ω′
zero′ = just zero

suc′ : ω′ → ω′
suc′ nothing = nothing
suc′ (just x) = just (suc x)

inf′ : ω′
inf′ = nothing

ω→ω′ : ω → ω′
ω→ω′ zero = zero′
ω→ω′ (suc n) = suc′ (ω→ω′ n)
ω→ω′ inf = inf′
ω→ω′ (suc-inf i) = inf′

ℕ→ω : ℕ → ω
ℕ→ω zero = zero
ℕ→ω (suc n) = suc (ℕ→ω n)

ω′→ω : ω′ → ω
ω′→ω nothing = inf
ω′→ω (just n) = ℕ→ω n

ℕ→ω→ω′ : ∀ n → ω→ω′ (ℕ→ω n) ≡ just n
ℕ→ω→ω′ zero = refl
ℕ→ω→ω′ (suc n) = cong suc′ (ℕ→ω→ω′ n)

ω′→ω→ω′ : ∀ n → ω→ω′ (ω′→ω n) ≡ n
ω′→ω→ω′ nothing = refl
ω′→ω→ω′ (just n) = ℕ→ω→ω′ n

suc-hom : ∀ n → ω′→ω (suc′ n) ≡ suc (ω′→ω n)
suc-hom nothing = sym suc-inf
suc-hom (just x) = refl

ω→ω′→ω : ∀ n → ω′→ω (ω→ω′ n) ≡ n
ω→ω′→ω zero = refl
ω→ω′→ω inf = refl
ω→ω′→ω (suc n) = suc-hom (ω→ω′ n) ∙ cong suc (ω→ω′→ω n)
ω→ω′→ω (suc-inf i) = {!!}

open Iso

ω⇔ω′ : Iso ω ω′
ω⇔ω′ .fun = ω→ω′
ω⇔ω′ .inv = ω′→ω
ω⇔ω′ .leftInv = ω→ω′→ω
ω⇔ω′ .rightInv = ω′→ω→ω′