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) ∣₁