module Cubical.Relation.Binary.Order.Loset.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.Loset
open LosetStr
ℕ<Loset : Loset ℓ-zero ℓ-zero
fst ℕ<Loset = ℕ
_<_ (snd ℕ<Loset) = _<ℕ_
isLoset (snd ℕ<Loset) = isLosetℕ<
where
open IsLoset
abstract
isLosetℕ< : IsLoset _<ℕ_
isLosetℕ< .is-set = isSetℕ
isLosetℕ< .is-prop-valued = λ _ _ → isProp≤
isLosetℕ< .is-irrefl = λ _ → ¬m<m
isLosetℕ< .is-trans = λ _ _ _ → <-trans
isLosetℕ< .is-asym = λ a b a<b b<a → ¬m<m (<-trans a<b b<a)
isLosetℕ< .is-weakly-linear a b c a<b with a ≟ c
... | lt a<c = ∣ inl a<c ∣₁
... | eq a≡c = ∣ inr (subst (_<ℕ b) a≡c a<b) ∣₁
... | gt c<a = ∣ inr (<-trans c<a a<b) ∣₁
isLosetℕ< .is-connected a b (¬a<b , ¬b<a) = ≤-antisym (<-asym' ¬b<a) (<-asym' ¬a<b)