Nat.agda

open import 1Lab.Prelude
open import Data.Nat

module wip.Nat where

module _
  (N : Type)
  (N-set : is-set N)
  (z : N)
  (s : N → N)
  (ind-prop : ∀ (P : N → Type) → (∀ n → is-prop (P n)) → P z → (∀ n → P n → P (s n)) → ∀ n → P n)
  (z≠s : ∀ n → ¬ (z ≡ s n))
  (s-inj : ∀ n m → s n ≡ s m → n ≡ m)
  where

  to : Nat → N
  to zero = z
  to (suc n) = s (to n)

  Nat≃N : Nat ≃ N
  Nat≃N .fst = to
  Nat≃N .snd .is-eqv = ind-prop _ (λ _ → hlevel 1)
    (contr (0 , refl) λ where
      (zero , p) → Σ-prop-path (λ _ → N-set _ _) refl
      (suc n , p) → absurd (z≠s _ (sym p)))
    λ n (contr (m , p) q) → contr (suc m , ap s p) λ where
      (zero , y) → absurd (z≠s _ y)
      (suc x , y) → Σ-prop-path (λ _ → N-set _ _) (ap (suc ∘ fst) (q (x , s-inj _ _ y)))