module Cubical.Relation.Binary.Order.Toset.Instances.Nat where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Sum
open import Cubical.HITs.PropositionalTruncation

open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order renaming (_≤_ to _≤ℕ_)

open import Cubical.Relation.Binary.Order.Toset

open TosetStr

ℕ≤Toset : Toset ℓ-zero ℓ-zero
fst ℕ≤Toset = ℕ
_≤_ (snd ℕ≤Toset) = _≤ℕ_
isToset (snd ℕ≤Toset) = isTosetℕ≤
  where
    open IsToset
    abstract
      isTosetℕ≤ : IsToset _≤ℕ_
      isTosetℕ≤ .is-set         = isSetℕ
      isTosetℕ≤ .is-prop-valued = λ _ _ → isProp≤
      isTosetℕ≤ .is-refl        = λ _ → ≤-refl
      isTosetℕ≤ .is-trans       = λ _ _ _ → ≤-trans
      isTosetℕ≤ .is-antisym     = λ _ _ → ≤-antisym
      isTosetℕ≤ .is-total a b with splitℕ-≤ a b
      ... | inl a≤b = ∣ inl a≤b ∣₁
      ... | inr b<a = ∣ inr (<-weaken b<a) ∣₁