module Setoid.NatType where

open import Prelude

open import Setoid.Definition
open import Setoid.Display
open import Setoid.Universes
open import Setoid.Lift

----------------------------------------------------------------------
-- Natural number type
----------------------------------------------------------------------
nrec :
  (l : ℕ)
  (X : ℕ → U l)
  (x₀ : El l (X 0))
  (x₊ :
    (n : ℕ)
    (x : El l (X n))
    → --------------
    El l (X (1+ n)) )
  (_ :
    (n : ℕ)
    (x x' : El l (X n))
    (_ : ℰ𝓁 l ∋ X n , x ≈ X n , x')
    → -------------------------------------------
    ℰ𝓁 l ∋ X (1+ n) , x₊ n x ≈ X (1+ n) , x₊ n x')
  (n : ℕ)
  → ----------------------------------------------
  El l (X n)

nrec l X x₀ x₊ e 0      = x₀
nrec l X x₀ x₊ e (1+ n) = x₊ n (nrec l X x₀ x₊ e n)

nrecCong :
  {l : ℕ}
  {X X' : ℕ → U l}
  {x₀ : El l (X 0)}
  {x₀' : El l (X' 0)}
  {x₊ :
    (n : ℕ)
    (x : El l (X n))
    → --------------
    El l (X (1+ n))  }
  {x₊' :
    (n : ℕ)
    (x : El l (X' n))
    → --------------
    El l (X' (1+ n))  }
  {c :
    (n : ℕ)
    (x x' : El l (X n))
    (_ : ℰ𝓁 l ∋ X n , x ≈ X n , x')
    → -------------------------------------------
    ℰ𝓁 l ∋ X (1+ n) , x₊ n x ≈ X (1+ n) , x₊ n x'}
  {c' :
    (n : ℕ)
    (x x' : El l (X' n))
    (_ : ℰ𝓁 l ∋ X' n , x ≈ X' n , x')
    → -----------------------------------------------
    ℰ𝓁 l ∋ X' (1+ n) , x₊' n x ≈ X' (1+ n) , x₊' n x'}
  (n n' : ℕ)
  (_ :
    (n : ℕ)
    → --------------
    𝒰 l ∋ X n ~ X' n)
  (_ : ℰ𝓁 l ∋ X 0 , x₀ ≈ X' 0 , x₀')
  (_ :
    (n : ℕ)
    (x : El l (X n))
    (x' : El l (X' n))
    (_ : ℰ𝓁 l ∋ X n , x ≈ X' n , x')
    → ---------------------------------------------
    ℰ𝓁 l ∋ X (1+ n) , x₊ n x ≈ X' (1+ n) , x₊' n x')
  (_ : n ≡ n')
  → ------------------------------------------------
  ℰ𝓁 l ∋ X  n , nrec l X  x₀  x₊  c  n  ≈
         X' n' , nrec l X' x₀' x₊' c' n'

nrecCong 0 _ _ e _ refl = e
nrecCong{l}{X}{X'}{x₀}{x₀'}{x₊}{x₊'}{c}{c'} (1+ n) _ f e g refl = g n
  (nrec l X x₀ x₊ c n)
  (nrec l X' x₀' x₊' c' n)
  (nrecCong{l}{X}{X'}{x₀}{x₀'}{x₊}{x₊'}{c}{c'} n _ f e g refl)

natbeta₀ :
  (l : ℕ)
  (X : ℕ → U l)
  (x₀ : El l (X 0))
  (x₊ :
    (n : ℕ)
    (x : El l (X n))
    → --------------
    El l (X (1+ n))  )
  (c :
    (n : ℕ)
    (x x' : El l (X n))
    (_ : ℰ𝓁 l ∋ X n , x ≈ X n , x')
    → -------------------------------------------
    ℰ𝓁 l ∋ X (1+ n) , x₊ n x ≈ X (1+ n) , x₊ n x')
  → ----------------------------------------------
  ℰ𝓁 l ∋ X 0 , nrec l X x₀ x₊ c 0 ≈ X 0 , x₀

natbeta₀ l X x₀ _ _ = hrfl (ℰ𝓁 l) (X 0) x₀

natbeta₊ :
  (l : ℕ)
  (X : ℕ → U l)
  (x₀ : El l (X 0))
  (x₊ :
    (n : ℕ)
    (x : El l (X n))
    → --------------
    El l (X (1+ n))  )
  (c :
    (n : ℕ)
    (x x' : El l (X n))
    (_ : ℰ𝓁 l ∋ X n , x ≈ X n , x')
    → -------------------------------------------
    ℰ𝓁 l ∋ X (1+ n) , x₊ n x ≈ X (1+ n) , x₊ n x')
  (n : ℕ)
  → ----------------------------------------------
  ℰ𝓁 l ∋ X (1+ n) , nrec l X x₀ x₊ c (1+ n) ≈
         X (1+ n) , x₊ n (nrec l X x₀ x₊ c n)

natbeta₊ l X x₀ x₊ c n =
  hrfl (ℰ𝓁 l) (X (1+ n)) (x₊ n (nrec l X x₀ x₊ c n))