CoNat.agda

open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Product
open import Data.Empty
open import Function


data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

add-suc≡ : ∀ {n m} → n ≡ m → (suc n) ≡ (suc m)
add-suc≡ refl = refl


mutual
  record coℕ : Set where
    coinductive
    field
      force : coℕ'

  data coℕ' : Set where
    cozero' : coℕ'
    cosuc'  : coℕ → coℕ'
open coℕ

cozero : coℕ
force cozero = cozero'

cosuc : coℕ → coℕ
force (cosuc n) = cosuc' n

omega : coℕ
force omega = cosuc' omega


force≡ : ∀ {n m} → n ≡ m → (force n) ≡ (force m)
force≡ {n} {.n} refl = refl

cozero'-not-cosuc' : ∀ {n} → cozero' ≢ cosuc' n
cozero'-not-cosuc' {n} ()

cozero-not-cosuc : ∀ {n} → cozero ≢ cosuc n
cozero-not-cosuc {n} coz≡cos = cozero'-not-cosuc' (force≡ coz≡cos)

drop-cosuc'≡ : ∀ {n m} → cosuc' n ≡ cosuc' m → n ≡ m
drop-cosuc'≡ refl = refl

drop-cosuc≡ : ∀ {n m} → cosuc n ≡ cosuc m → n ≡ m
drop-cosuc≡ cn≡cm = drop-cosuc'≡ (force≡ cn≡cm)


ℕ-to-coℕ : ℕ → coℕ
ℕ-to-coℕ zero    = cozero
ℕ-to-coℕ (suc n) = cosuc (ℕ-to-coℕ n)

injective : {A B : Set} → (A → B) → Set
injective f = ∀ a b → f a ≡ f b → a ≡ b

inj-ℕ-to-coℕ : injective ℕ-to-coℕ
inj-ℕ-to-coℕ zero zero fa≡fb       = refl
inj-ℕ-to-coℕ zero (suc b) fa≡fb    = ⊥-elim (cozero-not-cosuc fa≡fb)
inj-ℕ-to-coℕ (suc a) zero fa≡fb    = ⊥-elim (cozero-not-cosuc (sym fa≡fb))
inj-ℕ-to-coℕ (suc a) (suc b) fa≡fb = add-suc≡ (inj-ℕ-to-coℕ a b (drop-cosuc≡ fa≡fb))

coℕ-to-ℕ? : coℕ → ℕ
coℕ-to-ℕ? n with (force n)
coℕ-to-ℕ? n | cozero' = zero
coℕ-to-ℕ? n | cosuc' n' with (force n')
coℕ-to-ℕ? n | cosuc' n' | cozero' = suc zero
coℕ-to-ℕ? n | cosuc' n' | (cosuc' x) = suc (suc zero)

cant-inject : ¬ (Σ[ f ∈ (coℕ → ℕ) ] (injective f))
cant-inject (f , inj) with (f omega) | inspect f omega
cant-inject (f , inj) | fω | [ eq ] = {!!}

no-inject-means-not-same : {A B : Set} → ¬ (Σ[ f ∈ (A → B) ] (injective f)) → A ≢ B
no-inject-means-not-same no-inj refl = no-inj (id , λ x y z → z)