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

open import Cubical.Foundations.Prelude

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

open import Cubical.Data.Int
open import Cubical.Data.Int.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        = λ _  isRefl≤
      isTosetℤ≤ .is-trans       = λ _ _ _  isTrans≤
      isTosetℤ≤ .is-antisym     = λ _ _  isAntisym≤
      isTosetℤ≤ .is-total a b with a  b
      ... | lt a<b =  inl (<-weaken a<b) ∣₁
      ... | eq a≡b =  inl (subst (a ≤ℤ_) a≡b isRefl≤) ∣₁
      ... | gt b<a =  inr (<-weaken b<a) ∣₁