Skip to content

Instantly share code, notes, and snippets.

@oisdk oisdk/infnat.agda
Created Oct 29, 2019

Embed
What would you like to do?
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 = ω′→ω→ω′
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.