------------------------------------------------------------------------
-- The Agda standard library
--
-- Coinductive "natural" numbers
------------------------------------------------------------------------

module Data.Conat where

open import Coinduction
open import Data.Nat.Base using (; zero; suc)
open import Relation.Binary

------------------------------------------------------------------------
-- The type

data Coℕ : Set where
zero : Coℕ
suc  : (n :  Coℕ)  Coℕ

------------------------------------------------------------------------
-- Some operations

fromℕ :   Coℕ
fromℕ zero    = zero
fromℕ (suc n) = suc ( fromℕ n)

∞ℕ : Coℕ
∞ℕ = suc ( ∞ℕ)

infixl 6 _+_

_+_ : Coℕ  Coℕ  Coℕ
zero  + n = n
suc m + n = suc ( ( m + n))

------------------------------------------------------------------------
-- Equality

data _≈_ : Coℕ  Coℕ  Set where
zero :                                 zero   zero
suc  :  {m n} (m≈n :  ( m   n))  suc m  suc n

setoid : Setoid _ _
setoid = record
{ Carrier       = Coℕ
; _≈_           = _≈_
; isEquivalence = record
{ refl  = refl
; sym   = sym
; trans = trans
}
}
where
refl : Reflexive _≈_
refl {zero}  = zero
refl {suc n} = suc ( refl)

sym : Symmetric _≈_
sym zero      = zero
sym (suc m≈n) = suc ( sym ( m≈n))

trans : Transitive _≈_
trans zero      zero      = zero
trans (suc m≈n) (suc n≈k) = suc ( trans ( m≈n) ( n≈k))