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