open import agda20200123 renaming (_+_ to _⊔_) -- \lub

-- open import Agda.Builtin.Nat

data ℕ : Type where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

{-# BUILTIN NATURAL ℕ #-}

one : ℕ
one = 1

_+_ : ℕ → ℕ → ℕ
0 + m = m
(suc n) + m = suc (n + m)

_*_ : ℕ → ℕ → ℕ
0 * m = 0
(suc n) * m = m + (n * m)

data Bool : Type where
  true : Bool
  false : Bool

if_then_else_ : ∀ {A : Type} → Bool → A → A → A
if true then x else y = x
if false then x else y = y

data List (A : Type) : Type where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A

filter : ∀ {A : Type} → (A → Bool) → List A → List A
filter p [] = []
filter p (x ∷ xs) with p x
... | true = x ∷ filter p xs
... | false = filter p xs

map : ∀ {A B : Type} → (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

data _<_ (n : ℕ) : ℕ → Type where
  ltS : n < suc n
  ltSR : ∀ {m : ℕ} → n < m → n < suc m

data _<'_ : ℕ → ℕ → Type where
  lt'O : ∀ {n : ℕ} → zero <' suc n
  lt'S : ∀ {n m : ℕ} → n <' m → suc n <' suc m

<-trans : ∀ {n m o : ℕ} → n < m → m < o → n < o
<-trans n<m ltS = ltSR n<m
<-trans n<m (ltSR m<o) = ltSR (<-trans n<m m<o)

{- this will be explained next week -}
data _≡_ (n : ℕ) : ℕ → Type where
  refl : n ≡ n

{- we will go back to this later -}
ℕ-dec : ∀ (n m : ℕ) → (n ≡ m) ⊔ (¬ (n ≡ m))
ℕ-dec 0 0 = inl refl
ℕ-dec 0 (suc m) = magic
ℕ-dec (suc n) 0 = magic
ℕ-dec (suc n) (suc m) = magic

{-
ℕ-trichotomy : ∀ (m n : ℕ) → (m ≡ n) ⊔ ((m < n) ⊔ (n < m))
ℕ-trichotomy = magic
-}