{-# OPTIONS --without-K --rewriting #-}

open import Agda.Builtin.Nat
  using ()
  renaming (_+_ to _+6_)
open import lib.Base
open import lib.Function
open import lib.NType
open import lib.PathGroupoid
open import lib.Relation
open import lib.types.Coproduct
open import lib.types.Empty

module lib.types.Nat where

_+_ = _+6_
infixl 80 _+_
abstract
  +-unit-r : (m : )  m + 0 == m
  +-unit-r 0     = idp
  +-unit-r (S m) = ap S (+-unit-r m)

  +-βr : (m n : )  m + (S n) == S (m + n)
  +-βr 0     n = idp
  +-βr (S m) n = ap S (+-βr m n)

  +-comm : (m n : )  m + n == n + m
  +-comm m 0     = +-unit-r m
  +-comm m (S n) = +-βr m n  ap S (+-comm m n)

  +-assoc : (k m n : )  (k + m) + n == k + (m + n)
  +-assoc 0     m n = idp
  +-assoc (S k) m n = ap S (+-assoc k m n)

-- the [+] is like [ℕ-S^]
ℕ-S^' :     
ℕ-S^' O n = n
ℕ-S^' (S m) n = ℕ-S^' m (S n)

ℕ-pred :   
ℕ-pred 0 = 0
ℕ-pred (S n) = n

abstract
  ℕ-S-is-inj : is-inj (S :> (  ))
  ℕ-S-is-inj n m p = ap ℕ-pred p

  ℕ-S-≠ :  {n m : } (p : n  m)  S n  S m :> 
  ℕ-S-≠ {n} {m} p = p  ℕ-S-is-inj n m

  private
    ℕ-S≠O-type :   Type₀
    ℕ-S≠O-type O = Empty
    ℕ-S≠O-type (S n) = Unit

  ℕ-S≠O : (n : )  S n  O
  ℕ-S≠O n p = transport ℕ-S≠O-type p unit

  ℕ-O≠S : (n : )  (O  S n)
  ℕ-O≠S n p = ℕ-S≠O n (! p)

  ℕ-has-dec-eq : has-dec-eq 
  ℕ-has-dec-eq O O = inl idp
  ℕ-has-dec-eq O (S n) = inr (ℕ-O≠S n)
  ℕ-has-dec-eq (S n) O = inr (ℕ-S≠O n)
  ℕ-has-dec-eq (S n) (S m) with ℕ-has-dec-eq n m
  ℕ-has-dec-eq (S n) (S m) | inl p = inl (ap S p)
  ℕ-has-dec-eq (S n) (S m) | inr ¬p = inr (ℕ-S-≠ ¬p)

ℕ-is-set : is-set 
ℕ-is-set = dec-eq-is-set ℕ-has-dec-eq

instance
  ℕ-level : {n : ℕ₋₂}  has-level (S (S n)) 
  ℕ-level {⟨-2⟩} = ℕ-is-set
  ℕ-level {n = S n} = raise-level (S (S n)) ℕ-level

{- Inequalities -}
infix 40 _<_ _≤_

data _<_ :     Type₀ where
  ltS : {m : }  m < (S m)
  ltSR : {m n : }  m < n  m < (S n)

_≤_ :     Type₀
m  n = Coprod (m == n) (m < n)

-- experimental: [lteE] [lteS] [lteSR]
lteE : {m : }  m  m
lteE = inl idp

lteS : {m : }  m  S m
lteS = inr ltS

lteSR : {m n : }  m  n  m  (S n)
lteSR (inl idp) = lteS
lteSR (inr lt) = inr (ltSR lt)

-- properties of [<]

O<S : (m : )  O < S m
O<S O = ltS
O<S (S m) = ltSR (O<S m)

O≤ : (m : )  O  m
O≤ O = inl idp
O≤ (S m) = inr (O<S m)

≮O :  n  ¬ (n < O)
≮O _ ()

S≰O :  n  ¬ (S n  O)
S≰O _ (inl ())
S≰O _ (inr ())

<-trans : {m n k : }  m < n  n < k  m < k
<-trans lt₁ ltS = ltSR lt₁
<-trans lt₁ (ltSR lt₂) = ltSR (<-trans lt₁ lt₂)

≤-refl : {m : }  m  m
≤-refl = lteE

≤-trans : {m n k : }  m  n  n  k  m  k
≤-trans (inl idp) lte₂ = lte₂
≤-trans lte₁ (inl idp) = lte₁
≤-trans (inr lt₁) (inr lt₂) = inr (<-trans lt₁ lt₂)

private
  test₀ : {m n : } (m≤n : m  n)  lteSR m≤n == ≤-trans m≤n lteS
  test₀ (inl idp) = idp
  test₀ (inr lt) = idp

<-ap-S : {m n : }  m < n  S m < S n
<-ap-S ltS = ltS
<-ap-S (ltSR lt) = ltSR (<-ap-S lt)

≤-ap-S : {m n : }  m  n  S m  S n
≤-ap-S (inl p) = inl (ap S p)
≤-ap-S (inr lt) = inr (<-ap-S lt)

<-cancel-S : {m n : }  S m < S n  m < n
<-cancel-S ltS = ltS
<-cancel-S (ltSR lt) = <-trans ltS lt

≤-cancel-S : {m n : }  S m  S n  m  n
≤-cancel-S (inl p) = inl (ap ℕ-pred p)
≤-cancel-S (inr lt) = inr (<-cancel-S lt)

<-dec : Decidable _<_
<-dec _ O = inr (≮O _)
<-dec O (S m) = inl (O<S m)
<-dec (S n) (S m) with <-dec n m
<-dec (S n) (S m) | inl p = inl (<-ap-S p)
<-dec (S n) (S m) | inr ¬p = inr (¬p  <-cancel-S)

≤-dec : Decidable _≤_
≤-dec O m = inl (O≤ m) -- important for the current cohomology development
≤-dec (S n) O = inr (S≰O n)
≤-dec (S n) (S m) with -dec n m
-dec (S n) (S m) | inl p = inl (≤-ap-S p)
≤-dec (S n) (S m) | inr ¬p = inr (¬p  ≤-cancel-S)

abstract
  <-to-≠ : {m n : }  m < n  m  n
  <-to-≠ {m = O} ltS = ℕ-O≠S _
  <-to-≠ {m = O} (ltSR lt) = ℕ-O≠S _
  <-to-≠ {m = S m} {n = O} ()
  <-to-≠ {m = S m} {n = S n} lt = ℕ-S-≠ (<-to-≠ (<-cancel-S lt))

  <-to-≱ : {m n : }  m < n  ¬ (n  m)
  <-to-≱ m<n (inl idp) = <-to-≠ m<n idp
  <-to-≱ m<n (inr n<m) = <-to-≠ (<-trans m<n n<m) idp

  <-has-all-paths : {m n : }  has-all-paths (m < n)
  <-has-all-paths = <-has-all-paths' idp where
    <-has-all-paths' : {m n₁ n₂ : } (eqn : n₁ == n₂) (lt₁ : m < n₁) (lt₂ : m < n₂)
       PathOver  n  m < n) eqn lt₁ lt₂
    <-has-all-paths' eqn ltS ltS = transport  eqn₁  PathOver (_<_ _) eqn₁ ltS ltS)
      (prop-has-all-paths idp eqn) idp
    <-has-all-paths' idp ltS (ltSR lt₂) = ⊥-rec (<-to-≠ lt₂ idp)
    <-has-all-paths' idp (ltSR lt₁) ltS = ⊥-rec (<-to-≠ lt₁ idp)
    <-has-all-paths' idp (ltSR lt₁) (ltSR lt₂) = ap ltSR (<-has-all-paths' idp lt₁ lt₂)

  instance
    <-is-prop : {m n : }  is-prop (m < n)
    <-is-prop = all-paths-is-prop <-has-all-paths

  ≤-has-all-paths : {m n : }  has-all-paths (m  n)
  ≤-has-all-paths = λ{
    (inl eq₁) (inl eq₂)  ap inl (prop-has-all-paths eq₁ eq₂);
    (inl eq)  (inr lt)   ⊥-rec (<-to-≠ lt eq);
    (inr lt)  (inl eq)   ⊥-rec (<-to-≠ lt eq);
    (inr lt₁) (inr lt₂)  ap inr (<-has-all-paths lt₁ lt₂)}

  instance
    ≤-is-prop : {m n : }  is-prop (m  n)
    ≤-is-prop = all-paths-is-prop ≤-has-all-paths

<-+-l : {m n : } (k : )  m < n  (k + m) < (k + n)
<-+-l O lt = lt
<-+-l (S k) lt = <-ap-S (<-+-l k lt)

≤-+-l : {m n : } (k : )  m  n  (k + m)  (k + n)
≤-+-l k (inl p) = inl (ap  t  k + t) p)
≤-+-l k (inr lt) = inr (<-+-l k lt)

<-+-r : {m n : } (k : )  m < n  (m + k) < (n + k)
<-+-r k ltS = ltS
<-+-r k (ltSR lt) = ltSR (<-+-r k lt)

≤-+-r : {m n : } (k : )  m  n  (m + k)  (n + k)
≤-+-r k (inl p) = inl (ap  t  t + k) p)
≤-+-r k (inr lt) = inr (<-+-r k lt)

<-witness : {m n : }  (m < n)  Σ   k  S k + m == n)
<-witness ltS = (O , idp)
<-witness (ltSR lt) = let w' = <-witness lt in (S (fst w') , ap S (snd w'))

≤-witness : {m n : }  (m  n)  Σ   k  k + m == n)
≤-witness (inl p) = (O , p)
≤-witness (inr lt) = let w' = <-witness lt in (S (fst w') , snd w')

-- Double

infix 120 _*2
_*2 :   
O *2 = O
(S n) *2 = S (S (n *2))

*2-increasing : (m : )  (m  m *2)
*2-increasing O = inl idp
*2-increasing (S m) = ≤-trans (≤-ap-S (*2-increasing m)) (inr ltS)

*2-monotone-< : {m n : }  m < n  m *2 < n *2
*2-monotone-< ltS = ltSR ltS
*2-monotone-< (ltSR lt) = ltSR (ltSR (*2-monotone-< lt))

*2-monotone-≤ : {m n : }  m  n  m *2  n *2
*2-monotone-≤ (inl p) = inl (ap _*2 p)
*2-monotone-≤ (inr lt) = inr (*2-monotone-< lt)

-- Trichotomy

ℕ-trichotomy : (m n : )  (m == n)  ((m < n)  (n < m))
ℕ-trichotomy O O = inl idp
ℕ-trichotomy O (S n) = inr (inl (O<S n))
ℕ-trichotomy (S m) O = inr (inr (O<S m))
ℕ-trichotomy (S m) (S n) with ℕ-trichotomy m n
ℕ-trichotomy (S m) (S n) | inl m=n = inl (ap S m=n)
ℕ-trichotomy (S m) (S n) | inr (inl m<n) = inr (inl (<-ap-S m<n))
ℕ-trichotomy (S m) (S n) | inr (inr m>n) = inr (inr (<-ap-S m>n))