{-# OPTIONS --safe #-}
module Cubical.Data.Rationals.Order where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence
open import Cubical.Functions.Logic using (_⊔′_)
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Int.Base as ℤ using (ℤ)
open import Cubical.Data.Int.Properties as ℤ using ()
open import Cubical.Data.Int.Order as ℤ using ()
open import Cubical.Data.Rationals.Base as ℚ
open import Cubical.Data.Rationals.Properties as ℚ
open import Cubical.Data.Nat as ℕ
open import Cubical.Data.NatPlusOne
open import Cubical.Data.Sigma
open import Cubical.Data.Sum as ⊎ using (_⊎_; inl; inr; isProp⊎)
open import Cubical.HITs.PropositionalTruncation as ∥₁ using (isPropPropTrunc; ∣_∣₁)
open import Cubical.HITs.SetQuotients
open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary.Base
infix 4 _≤_ _<_ _≥_ _>_
private
·CommR : (a b c : ℤ) → a ℤ.· b ℤ.· c ≡ a ℤ.· c ℤ.· b
·CommR a b c = sym (ℤ.·Assoc a b c) ∙ cong (a ℤ.·_) (ℤ.·Comm b c) ∙ ℤ.·Assoc a c b
_≤'_ : ℚ → ℚ → hProp ℓ-zero
_≤'_ = fun
where
lemma≤ : ((a , b) (c , d) (e , f) : (ℤ × ℕ₊₁))
→ (c ℤ.· ℕ₊₁→ℤ f ) ≡ (e ℤ.· ℕ₊₁→ℤ d)
→ ((a ℤ.· ℕ₊₁→ℤ d) ℤ.≤ (c ℤ.· ℕ₊₁→ℤ b))
≡ ((a ℤ.· ℕ₊₁→ℤ f) ℤ.≤ (e ℤ.· ℕ₊₁→ℤ b))
lemma≤ (a , b) (c , d) (e , f) cf≡ed = (ua (propBiimpl→Equiv ℤ.isProp≤ ℤ.isProp≤
(ℤ.≤-·o-cancel {k = -1+ d} ∘
subst2 ℤ._≤_ (·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))
(·CommR c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f) ∙
cong (ℤ._· ℕ₊₁→ℤ b) cf≡ed ∙
·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∘
ℤ.≤-·o {k = ℕ₊₁→ℕ f})
(ℤ.≤-·o-cancel {k = -1+ f} ∘
subst2 ℤ._≤_ (·CommR a (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d))
(·CommR e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) ∙
cong (ℤ._· ℕ₊₁→ℤ b) (sym cf≡ed) ∙
·CommR c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b)) ∘
ℤ.≤-·o {k = ℕ₊₁→ℕ d})))
fun₀ : ℤ × ℕ₊₁ → ℚ → hProp ℓ-zero
fst (fun₀ (a , b) [ c , d ]) = a ℤ.· ℕ₊₁→ℤ d ℤ.≤ c ℤ.· ℕ₊₁→ℤ b
snd (fun₀ _ [ _ ]) = ℤ.isProp≤
fun₀ a/b (eq/ c/d e/f cf≡ed i) = record
{ fst = lemma≤ a/b c/d e/f cf≡ed i
; snd = isProp→PathP (λ i → isPropIsProp {A = lemma≤ a/b c/d e/f cf≡ed i}) ℤ.isProp≤ ℤ.isProp≤ i
}
fun₀ a/b (squash/ x y p q i j) = isSet→SquareP (λ _ _ → isSetHProp)
(λ _ → fun₀ a/b x)
(λ _ → fun₀ a/b y)
(λ i → fun₀ a/b (p i))
(λ i → fun₀ a/b (q i)) j i
toPath : ∀ a/b c/d (x : a/b ∼ c/d) (y : ℚ) → fun₀ a/b y ≡ fun₀ c/d y
toPath (a , b) (c , d) ad≡cb = elimProp (λ _ → isSetHProp _ _) λ (e , f) →
Σ≡Prop (λ _ → isPropIsProp) (ua (propBiimpl→Equiv ℤ.isProp≤ ℤ.isProp≤
(ℤ.≤-·o-cancel {k = -1+ b} ∘
subst2 ℤ._≤_ (·CommR a (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d) ∙
cong (ℤ._· ℕ₊₁→ℤ f) ad≡cb ∙
·CommR c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f))
(·CommR e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d)) ∘
ℤ.≤-·o {k = ℕ₊₁→ℕ d})
(ℤ.≤-·o-cancel {k = -1+ d} ∘
subst2 ℤ._≤_ (·CommR c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b) ∙
cong (ℤ._· ℕ₊₁→ℤ f) (sym ad≡cb) ∙
·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))
(·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∘
ℤ.≤-·o {k = ℕ₊₁→ℕ b})))
fun : ℚ → ℚ → hProp ℓ-zero
fun [ a/b ] y = fun₀ a/b y
fun (eq/ a/b c/d ad≡cb i) y = toPath a/b c/d ad≡cb y i
fun (squash/ x y p q i j) z = isSet→SquareP (λ _ _ → isSetHProp)
(λ _ → fun x z) (λ _ → fun y z) (λ i → fun (p i) z) (λ i → fun (q i) z) j i
_<'_ : ℚ → ℚ → hProp ℓ-zero
_<'_ = fun
where
lemma< : ((a , b) (c , d) (e , f) : (ℤ × ℕ₊₁))
→ (c ℤ.· ℕ₊₁→ℤ f ) ≡ (e ℤ.· ℕ₊₁→ℤ d)
→ ((a ℤ.· ℕ₊₁→ℤ d) ℤ.< (c ℤ.· ℕ₊₁→ℤ b))
≡ ((a ℤ.· ℕ₊₁→ℤ f) ℤ.< (e ℤ.· ℕ₊₁→ℤ b))
lemma< (a , b) (c , d) (e , f) cf≡ed = (ua (propBiimpl→Equiv ℤ.isProp< ℤ.isProp<
(ℤ.<-·o-cancel {k = -1+ d} ∘
subst2 ℤ._<_ (·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))
(·CommR c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f) ∙
cong (ℤ._· ℕ₊₁→ℤ b) cf≡ed ∙
·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∘
ℤ.<-·o {k = -1+ f})
(ℤ.<-·o-cancel {k = -1+ f} ∘
subst2 ℤ._<_ (·CommR a (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d))
(·CommR e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) ∙
cong (ℤ._· ℕ₊₁→ℤ b) (sym cf≡ed) ∙
·CommR c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b)) ∘
ℤ.<-·o {k = -1+ d})))
fun₀ : ℤ × ℕ₊₁ → ℚ → hProp ℓ-zero
fst (fun₀ (a , b) [ c , d ]) = a ℤ.· ℕ₊₁→ℤ d ℤ.< c ℤ.· ℕ₊₁→ℤ b
snd (fun₀ _ [ _ ]) = ℤ.isProp<
fun₀ a/b (eq/ c/d e/f cf≡ed i) = record
{ fst = lemma< a/b c/d e/f cf≡ed i
; snd = isProp→PathP (λ i → isPropIsProp {A = lemma< a/b c/d e/f cf≡ed i}) ℤ.isProp< ℤ.isProp< i
}
fun₀ a/b (squash/ x y p q i j) = isSet→SquareP (λ _ _ → isSetHProp)
(λ _ → fun₀ a/b x)
(λ _ → fun₀ a/b y)
(λ i → fun₀ a/b (p i))
(λ i → fun₀ a/b (q i)) j i
toPath : ∀ a/b c/d (x : a/b ∼ c/d) (y : ℚ) → fun₀ a/b y ≡ fun₀ c/d y
toPath (a , b) (c , d) ad≡cb = elimProp (λ _ → isSetHProp _ _) λ (e , f) →
Σ≡Prop (λ _ → isPropIsProp) (ua (propBiimpl→Equiv ℤ.isProp< ℤ.isProp<
(ℤ.<-·o-cancel {k = -1+ b} ∘
subst2 ℤ._<_ (·CommR a (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d) ∙
cong (ℤ._· ℕ₊₁→ℤ f) ad≡cb ∙
·CommR c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f))
(·CommR e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d)) ∘
ℤ.<-·o {k = -1+ d})
(ℤ.<-·o-cancel {k = -1+ d} ∘
subst2 ℤ._<_ (·CommR c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b) ∙
cong (ℤ._· ℕ₊₁→ℤ f) (sym ad≡cb) ∙
·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))
(·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∘
ℤ.<-·o {k = -1+ b})))
fun : ℚ → ℚ → hProp ℓ-zero
fun [ a/b ] y = fun₀ a/b y
fun (eq/ a/b c/d ad≡cb i) y = toPath a/b c/d ad≡cb y i
fun (squash/ x y p q i j) z = isSet→SquareP (λ _ _ → isSetHProp)
(λ _ → fun x z) (λ _ → fun y z) (λ i → fun (p i) z) (λ i → fun (q i) z) j i
_≤_ : ℚ → ℚ → Type₀
m ≤ n = fst (m ≤' n)
_<_ : ℚ → ℚ → Type₀
m < n = fst (m <' n)
_≥_ : ℚ → ℚ → Type₀
m ≥ n = n ≤ m
_>_ : ℚ → ℚ → Type₀
m > n = n < m
_#_ : ℚ → ℚ → Type₀
m # n = (m < n) ⊎ (n < m)
data Trichotomy (m n : ℚ) : Type₀ where
lt : m < n → Trichotomy m n
eq : m ≡ n → Trichotomy m n
gt : m > n → Trichotomy m n
module _ where
open BinaryRelation
isProp≤ : isPropValued _≤_
isProp≤ m n = snd (m ≤' n)
isProp< : isPropValued _<_
isProp< m n = snd (m <' n)
isRefl≤ : isRefl _≤_
isRefl≤ = elimProp {P = λ x → x ≤ x} (λ x → isProp≤ x x) λ _ → ℤ.isRefl≤
isIrrefl< : isIrrefl _<_
isIrrefl< = elimProp {P = λ x → ¬ x < x} (λ _ → isProp¬ _) λ _ → ℤ.isIrrefl<
isAntisym≤ : isAntisym _≤_
isAntisym≤ =
elimProp2 {P = λ a b → a ≤ b → b ≤ a → a ≡ b}
(λ x y → isPropΠ2 λ _ _ → isSetℚ x y)
λ a b a≤b b≤a → eq/ a b (ℤ.isAntisym≤ a≤b b≤a)
isTrans≤ : isTrans _≤_
isTrans≤ =
elimProp3 {P = λ a b c → a ≤ b → b ≤ c → a ≤ c}
(λ x _ z → isPropΠ2 λ _ _ → isProp≤ x z)
λ { (a , b) (c , d) (e , f) ad≤cb cf≤ed →
ℤ.≤-·o-cancel {k = -1+ d}
(subst (ℤ._≤ e ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ d)
(·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))
(ℤ.isTrans≤ (ℤ.≤-·o {k = ℕ₊₁→ℕ f} ad≤cb)
(subst2 ℤ._≤_
(·CommR c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b))
(·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b))
(ℤ.≤-·o {k = ℕ₊₁→ℕ b} cf≤ed)))) }
isTrans< : isTrans _<_
isTrans< =
elimProp3 {P = λ a b c → a < b → b < c → a < c}
(λ x _ z → isPropΠ2 λ _ _ → isProp< x z)
λ { (a , b) (c , d) (e , f) ad<cb cf<ed →
ℤ.<-·o-cancel {k = -1+ d}
(subst (ℤ._< e ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ d)
(·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))
(ℤ.isTrans< (ℤ.<-·o {k = -1+ f} ad<cb)
(subst2 ℤ._<_
(·CommR c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b))
(·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b))
(ℤ.<-·o {k = -1+ b} cf<ed)))) }
isAsym< : isAsym _<_
isAsym< = isIrrefl×isTrans→isAsym _<_ (isIrrefl< , isTrans<)
isTotal≤ : isTotal _≤_
isTotal≤ =
elimProp2 {P = λ a b → (a ≤ b) ⊔′ (b ≤ a)}
(λ _ _ → isPropPropTrunc)
λ a b → ∣ lem a b ∣₁
where
lem : (a b : ℤ.ℤ × ℕ₊₁) → ([ a ] ≤ [ b ]) ⊎ ([ b ] ≤ [ a ])
lem (a , b) (c , d) with (a ℤ.· ℕ₊₁→ℤ d) ℤ.≟ (c ℤ.· ℕ₊₁→ℤ b)
... | ℤ.lt ad<cb = inl (ℤ.<-weaken ad<cb)
... | ℤ.eq ad≡cb = inl (0 , ad≡cb)
... | ℤ.gt cb<ad = inr (ℤ.<-weaken cb<ad)
isConnected< : isConnected _<_
isConnected< =
elimProp2 {P = λ a b → (¬ a < b) × (¬ b < a) → a ≡ b}
(λ a b → isProp→ (isSetℚ a b))
lem
where
lem : (a b : ℤ.ℤ × ℕ₊₁) → (¬ [ a ] < [ b ]) × (¬ [ b ] < [ a ]) → [ a ] ≡ [ b ]
lem (a , b) (c , d) (¬ad<cb , ¬cb<ad) with (a ℤ.· ℕ₊₁→ℤ d) ℤ.≟ (c ℤ.· ℕ₊₁→ℤ b)
... | ℤ.lt ad<cb = ⊥.rec (¬ad<cb ad<cb)
... | ℤ.eq ad≡cb = eq/ (a , b) (c , d) ad≡cb
... | ℤ.gt cb<ad = ⊥.rec (¬cb<ad cb<ad)
isProp# : isPropValued _#_
isProp# x y = isProp⊎ (isProp< x y) (isProp< y x) (isAsym< x y)
isIrrefl# : isIrrefl _#_
isIrrefl# x (inl x<x) = isIrrefl< x x<x
isIrrefl# x (inr x<x) = isIrrefl< x x<x
isSym# : isSym _#_
isSym# _ _ (inl x<y) = inr x<y
isSym# _ _ (inr y<x) = inl y<x
inequalityImplies# : inequalityImplies _#_
inequalityImplies#
= elimProp2 {P = λ a b → ¬ a ≡ b → a # b}
(λ a b → isProp→ (isProp# a b))
lem
where
lem : (a b : ℤ.ℤ × ℕ₊₁) → ¬ [_] {R = _∼_} a ≡ [ b ] → [ a ] # [ b ]
lem (a , b) (c , d) ¬a≡b with (a ℤ.· ℕ₊₁→ℤ d) ℤ.≟ (c ℤ.· ℕ₊₁→ℤ b)
... | ℤ.lt ad<cb = inl ad<cb
... | ℤ.eq ad≡cb = ⊥.rec (¬a≡b (eq/ (a , b) (c , d) ad≡cb))
... | ℤ.gt cb<ad = inr cb<ad
isWeaklyLinear< : isWeaklyLinear _<_
isWeaklyLinear< =
elimProp3 {P = λ a b c → a < b → (a < c) ⊔′ (c < b)}
(λ _ _ _ → isProp→ isPropPropTrunc)
lem
where
lem : (a b c : ℤ.ℤ × ℕ₊₁) → [ a ] < [ b ] → ([ a ] < [ c ]) ⊔′ ([ c ] < [ b ])
lem a b c a<b with discreteℚ [ a ] [ c ]
... | yes a≡c = ∣ inr (subst (_< [ b ]) a≡c a<b) ∣₁
... | no a≢c = ∣ ⊎.map (λ a<c → a<c)
(λ c<a → isTrans< [ c ] [ a ] [ b ] c<a a<b)
(inequalityImplies# [ a ] [ c ] a≢c) ∣₁
isCotrans# : isCotrans _#_
isCotrans#
= elimProp3 {P = λ a b c → a # b → (a # c) ⊔′ (b # c)}
(λ _ _ _ → isProp→ isPropPropTrunc)
lem
where
lem : (a b c : ℤ.ℤ × ℕ₊₁) → [ a ] # [ b ] → ([ a ] # [ c ]) ⊔′ ([ b ] # [ c ])
lem a b c a#b with discreteℚ [ b ] [ c ]
... | yes b≡c = ∣ inl (subst ([ a ] #_) b≡c a#b) ∣₁
... | no b≢c = ∣ inr (inequalityImplies# [ b ] [ c ] b≢c) ∣₁
≤-+o : ∀ m n o → m ≤ n → m ℚ.+ o ≤ n ℚ.+ o
≤-+o =
elimProp3 {P = λ a b c → a ≤ b → a ℚ.+ c ≤ b ℚ.+ c}
(λ x y z → isProp→ (isProp≤ (x ℚ.+ z) (y ℚ.+ z)))
λ { (a , b) (c , d) (e , f) ad≤cb →
subst2 ℤ._≤_
(cong₂ ℤ._+_
(cong (λ x → a ℤ.· ℕ₊₁→ℤ d ℤ.· x)
(ℤ.pos·pos (ℕ₊₁→ℕ f) (ℕ₊₁→ℕ f)) ∙
sym (ℤ.·Assoc a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f ℤ.· ℕ₊₁→ℤ f)) ∙
cong (a ℤ.·_) (ℤ.·Assoc (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ f) ∙
cong (ℤ._· ℕ₊₁→ℤ f) (ℤ.·Comm (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f)) ∙
sym (ℤ.·Assoc (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))) ∙
ℤ.·Assoc a (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d ℤ.· ℕ₊₁→ℤ f) ∙
cong (λ x → a ℤ.· ℕ₊₁→ℤ f ℤ.· x)
(sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f))))
(sym (ℤ.·Assoc (e ℤ.· ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f)) ∙
cong (λ x → e ℤ.· ℕ₊₁→ℤ b ℤ.· x)
(sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f)))) ∙
sym (ℤ.·DistL+ (a ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ b) (ℕ₊₁→ℤ (d ·₊₁ f))))
(cong₂ ℤ._+_
(cong (λ x → c ℤ.· ℕ₊₁→ℤ b ℤ.· x)
(ℤ.pos·pos (ℕ₊₁→ℕ f) (ℕ₊₁→ℕ f)) ∙
sym (ℤ.·Assoc c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f ℤ.· ℕ₊₁→ℤ f)) ∙
cong (c ℤ.·_) (ℤ.·Assoc (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ f) ∙
cong (ℤ._· ℕ₊₁→ℤ f) (ℤ.·Comm (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f)) ∙
sym (ℤ.·Assoc (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f))) ∙
ℤ.·Assoc c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ f) ∙
cong (λ x → c ℤ.· ℕ₊₁→ℤ f ℤ.· x)
(sym (ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f))))
(cong (ℤ._· ℕ₊₁→ℤ f)
(sym (ℤ.·Assoc e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d)) ∙
cong (e ℤ.·_) (ℤ.·Comm (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d)) ∙
ℤ.·Assoc e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∙
sym (ℤ.·Assoc (e ℤ.· ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f)) ∙
cong (λ x → e ℤ.· ℕ₊₁→ℤ d ℤ.· x)
(sym (ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f)))) ∙
sym (ℤ.·DistL+ (c ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ d) (ℕ₊₁→ℤ (b ·₊₁ f))))
(ℤ.≤-+o {o = e ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ d ℤ.· ℕ₊₁→ℤ f}
(ℤ.≤-·o {k = ℕ₊₁→ℕ (f ·₊₁ f)} ad≤cb)) }
≤-o+ : ∀ m n o → m ≤ n → o ℚ.+ m ≤ o ℚ.+ n
≤-o+ m n o = subst2 _≤_ (+Comm m o)
(+Comm n o) ∘
≤-+o m n o
≤Monotone+ : ∀ m n o s → m ≤ n → o ≤ s → m ℚ.+ o ≤ n ℚ.+ s
≤Monotone+ m n o s m≤n o≤s
= isTrans≤ (m ℚ.+ o)
(n ℚ.+ o)
(n ℚ.+ s)
(≤-+o m n o m≤n)
(≤-o+ o s n o≤s)
≤-o+-cancel : ∀ m n o → o ℚ.+ m ≤ o ℚ.+ n → m ≤ n
≤-o+-cancel m n o
= subst2 _≤_ (+Assoc (- o) o m ∙ cong (ℚ._+ m) (+InvL o) ∙ +IdL m)
(+Assoc (- o) o n ∙ cong (ℚ._+ n) (+InvL o) ∙ +IdL n) ∘
≤-o+ (o ℚ.+ m) (o ℚ.+ n) (- o)
≤-+o-cancel : ∀ m n o → m ℚ.+ o ≤ n ℚ.+ o → m ≤ n
≤-+o-cancel m n o
= subst2 _≤_ (sym (+Assoc m o (- o)) ∙ cong (λ x → m ℚ.+ x) (+InvR o) ∙ +IdR m)
(sym (+Assoc n o (- o)) ∙ cong (λ x → n ℚ.+ x) (+InvR o) ∙ +IdR n) ∘
≤-+o (m ℚ.+ o) (n ℚ.+ o) (- o)
<-+o : ∀ m n o → m < n → m ℚ.+ o < n ℚ.+ o
<-+o =
elimProp3 {P = λ a b c → a < b → a ℚ.+ c < b ℚ.+ c}
(λ x y z → isProp→ (isProp< (x ℚ.+ z) (y ℚ.+ z)))
λ { (a , b) (c , d) (e , f) ad<cb →
subst2 ℤ._<_
(cong₂ ℤ._+_
(cong (λ x → a ℤ.· ℕ₊₁→ℤ d ℤ.· x)
(ℤ.pos·pos (ℕ₊₁→ℕ f) (ℕ₊₁→ℕ f)) ∙
sym (ℤ.·Assoc a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f ℤ.· ℕ₊₁→ℤ f)) ∙
cong (a ℤ.·_) (ℤ.·Assoc (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ f) ∙
cong (ℤ._· ℕ₊₁→ℤ f) (ℤ.·Comm (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f)) ∙
sym (ℤ.·Assoc (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))) ∙
ℤ.·Assoc a (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d ℤ.· ℕ₊₁→ℤ f) ∙
cong (λ x → a ℤ.· ℕ₊₁→ℤ f ℤ.· x)
(sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f))))
(sym (ℤ.·Assoc (e ℤ.· ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f)) ∙
cong (λ x → e ℤ.· ℕ₊₁→ℤ b ℤ.· x)
(sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f)))) ∙
sym (ℤ.·DistL+ (a ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ b) (ℕ₊₁→ℤ (d ·₊₁ f))))
(cong₂ ℤ._+_
(cong (λ x → c ℤ.· ℕ₊₁→ℤ b ℤ.· x)
(ℤ.pos·pos (ℕ₊₁→ℕ f) (ℕ₊₁→ℕ f)) ∙
sym (ℤ.·Assoc c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f ℤ.· ℕ₊₁→ℤ f)) ∙
cong (c ℤ.·_) (ℤ.·Assoc (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ f) ∙
cong (ℤ._· ℕ₊₁→ℤ f) (ℤ.·Comm (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f)) ∙
sym (ℤ.·Assoc (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f))) ∙
ℤ.·Assoc c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ f) ∙
cong (λ x → c ℤ.· ℕ₊₁→ℤ f ℤ.· x)
(sym (ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f))))
(cong (ℤ._· ℕ₊₁→ℤ f)
(sym (ℤ.·Assoc e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d)) ∙
cong (e ℤ.·_) (ℤ.·Comm (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d)) ∙
ℤ.·Assoc e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∙
sym (ℤ.·Assoc (e ℤ.· ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f)) ∙
cong (λ x → e ℤ.· ℕ₊₁→ℤ d ℤ.· x)
(sym (ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f)))) ∙
sym (ℤ.·DistL+ (c ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ d) (ℕ₊₁→ℤ (b ·₊₁ f))))
(ℤ.<-+o {o = e ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ d ℤ.· ℕ₊₁→ℤ f}
(ℤ.<-·o {k = -1+ (f ·₊₁ f)} ad<cb)) }
<-o+ : ∀ m n o → m < n → o ℚ.+ m < o ℚ.+ n
<-o+ m n o = subst2 _<_ (+Comm m o) (+Comm n o) ∘ <-+o m n o
<Monotone+ : ∀ m n o s → m < n → o < s → m ℚ.+ o < n ℚ.+ s
<Monotone+ m n o s m<n o<s
= isTrans< (m ℚ.+ o) (n ℚ.+ o) (n ℚ.+ s) (<-+o m n o m<n) (<-o+ o s n o<s)
<-o+-cancel : ∀ m n o → o ℚ.+ m < o ℚ.+ n → m < n
<-o+-cancel m n o
= subst2 _<_ (+Assoc (- o) o m ∙ cong (ℚ._+ m) (+InvL o) ∙ +IdL m)
(+Assoc (- o) o n ∙ cong (ℚ._+ n) (+InvL o) ∙ +IdL n) ∘
<-o+ (o ℚ.+ m) (o ℚ.+ n) (- o)
<-+o-cancel : ∀ m n o → m ℚ.+ o < n ℚ.+ o → m < n
<-+o-cancel m n o
= subst2 _<_ (sym (+Assoc m o (- o)) ∙ cong (λ x → m ℚ.+ x) (+InvR o) ∙ +IdR m)
(sym (+Assoc n o (- o)) ∙ cong (λ x → n ℚ.+ x) (+InvR o) ∙ +IdR n) ∘
<-+o (m ℚ.+ o) (n ℚ.+ o) (- o)
<Weaken≤ : ∀ m n → m < n → m ≤ n
<Weaken≤ m n = elimProp2 {P = λ x y → x < y → x ≤ y}
(λ x y → isProp→ (isProp≤ x y))
(λ { (a , b) (c , d) → ℤ.<-weaken }) m n
isTrans<≤ : ∀ m n o → m < n → n ≤ o → m < o
isTrans<≤ =
elimProp3 {P = λ a b c → a < b → b ≤ c → a < c}
(λ x _ z → isPropΠ2 λ _ _ → isProp< x z)
λ { (a , b) (c , d) (e , f) ad<cb cf≤ed
→ ℤ.<-·o-cancel {k = -1+ d}
(ℤ.<≤-trans {m = c ℤ.· ℕ₊₁→ℤ f ℤ.· ℕ₊₁→ℤ b}
(subst2 ℤ._<_ (·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))
(·CommR c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f))
(ℤ.<-·o {k = -1+ f} ad<cb))
(subst (_ ℤ.≤_) (·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b))
(ℤ.≤-·o {k = ℕ₊₁→ℕ b} cf≤ed)) )}
isTrans≤< : ∀ m n o → m ≤ n → n < o → m < o
isTrans≤< =
elimProp3 {P = λ a b c → a ≤ b → b < c → a < c}
(λ x _ z → isPropΠ2 λ _ _ → isProp< x z)
λ { (a , b) (c , d) (e , f) ad≤cb cf<ed
→ ℤ.<-·o-cancel {k = -1+ d}
(ℤ.≤<-trans {m = c ℤ.· ℕ₊₁→ℤ f ℤ.· ℕ₊₁→ℤ b}
(subst2 ℤ._≤_ (·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))
(·CommR c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f))
(ℤ.≤-·o {k = ℕ₊₁→ℕ f} ad≤cb))
(subst (_ ℤ.<_) (·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b))
(ℤ.<-·o {k = -1+ b} cf<ed)) )}
≤-·o : ∀ m n o → 0 ≤ o → m ≤ n → m ℚ.· o ≤ n ℚ.· o
≤-·o =
elimProp3 {P = λ a b c → 0 ≤ c → a ≤ b → a ℚ.· c ≤ b ℚ.· c}
(λ x y z → isPropΠ2 λ _ _ → isProp≤ (x ℚ.· z) (y ℚ.· z))
λ { (a , b) (c , d) (e , f) 0≤e ad≤cb
→ subst2 ℤ._≤_ (cong (ℤ._· ℕ₊₁→ℤ f) (·CommR a (ℕ₊₁→ℤ d) e) ∙
sym (ℤ.·Assoc (a ℤ.· e) (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f)) ∙
cong (a ℤ.· e ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f))))
(cong (ℤ._· ℕ₊₁→ℤ f) (·CommR c (ℕ₊₁→ℤ b) e) ∙
sym (ℤ.·Assoc (c ℤ.· e) (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f)) ∙
cong (c ℤ.· e ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f))))
(ℤ.≤-·o {k = ℕ₊₁→ℕ f}
(ℤ.0≤o→≤-·o (subst (0 ℤ.≤_) (ℤ.·IdR e) 0≤e) ad≤cb)) }
≤-·o-cancel : ∀ m n o → 0 < o → m ℚ.· o ≤ n ℚ.· o → m ≤ n
≤-·o-cancel =
elimProp3 {P = λ a b c → 0 < c → a ℚ.· c ≤ b ℚ.· c → a ≤ b}
(λ x y _ → isPropΠ2 λ _ _ → isProp≤ x y)
λ { (a , b) (c , d) (e , f) 0<e aedf≤cebf
→ ℤ.0<o→≤-·o-cancel (subst (0 ℤ.<_) (ℤ.·IdR e) 0<e)
(subst2 ℤ._≤_ (·CommR a e (ℕ₊₁→ℤ d)) (·CommR c e (ℕ₊₁→ℤ b))
(ℤ.≤-·o-cancel {k = -1+ f}
(subst2 ℤ._≤_ (sym (ℤ.·Assoc a e (ℕ₊₁→ℤ (d ·₊₁ f))) ∙
cong (λ x → a ℤ.· (e ℤ.· x))
(ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f)) ∙
assoc {a} {e})
(sym (ℤ.·Assoc c e (ℕ₊₁→ℤ (b ·₊₁ f))) ∙
cong (λ x → c ℤ.· (e ℤ.· x))
(ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f)) ∙
assoc {c} {e})
aedf≤cebf))) }
where assoc : ∀{a b c d} → a ℤ.· (b ℤ.· (c ℤ.· d)) ≡ a ℤ.· b ℤ.· c ℤ.· d
assoc {a} {b} {c} {d} = cong (a ℤ.·_) (ℤ.·Assoc b c d) ∙
ℤ.·Assoc a (b ℤ.· c) d ∙
cong (ℤ._· d) (ℤ.·Assoc a b c)
<-·o : ∀ m n o → 0 < o → m < n → m ℚ.· o < n ℚ.· o
<-·o =
elimProp3 {P = λ a b c → 0 < c → a < b → a ℚ.· c < b ℚ.· c}
(λ x y z → isPropΠ2 λ _ _ → isProp< (x ℚ.· z) (y ℚ.· z))
λ { (a , b) (c , d) (e , f) 0<e ad<cb
→ subst2 ℤ._<_ (cong (ℤ._· ℕ₊₁→ℤ f) (·CommR a (ℕ₊₁→ℤ d) e) ∙
sym (ℤ.·Assoc (a ℤ.· e) (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f)) ∙
cong (a ℤ.· e ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f))))
(cong (ℤ._· ℕ₊₁→ℤ f) (·CommR c (ℕ₊₁→ℤ b) e) ∙
sym (ℤ.·Assoc (c ℤ.· e) (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f)) ∙
cong (c ℤ.· e ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f))))
(ℤ.<-·o {k = -1+ f}
(ℤ.0<o→<-·o (subst (0 ℤ.<_) (ℤ.·IdR e) 0<e) ad<cb)) }
<-·o-cancel : ∀ m n o → 0 < o → m ℚ.· o < n ℚ.· o → m < n
<-·o-cancel =
elimProp3 {P = λ a b c → 0 < c → a ℚ.· c < b ℚ.· c → a < b}
(λ x y _ → isPropΠ2 λ _ _ → isProp< x y)
λ { (a , b) (c , d) (e , f) 0<e aedf<cebf
→ ℤ.0<o→<-·o-cancel (subst (0 ℤ.<_) (ℤ.·IdR e) 0<e)
(subst2 ℤ._<_ (·CommR a e (ℕ₊₁→ℤ d)) (·CommR c e (ℕ₊₁→ℤ b))
(ℤ.<-·o-cancel {k = -1+ f}
(subst2 ℤ._<_ (sym (ℤ.·Assoc a e (ℕ₊₁→ℤ (d ·₊₁ f))) ∙
cong (λ x → a ℤ.· (e ℤ.· x))
(ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f)) ∙
assoc {a} {e})
(sym (ℤ.·Assoc c e (ℕ₊₁→ℤ (b ·₊₁ f))) ∙
cong (λ x → c ℤ.· (e ℤ.· x))
(ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f)) ∙
assoc {c} {e})
aedf<cebf))) }
where assoc : ∀{a b c d} → a ℤ.· (b ℤ.· (c ℤ.· d)) ≡ a ℤ.· b ℤ.· c ℤ.· d
assoc {a} {b} {c} {d} = cong (a ℤ.·_) (ℤ.·Assoc b c d) ∙
ℤ.·Assoc a (b ℤ.· c) d ∙
cong (ℤ._· d) (ℤ.·Assoc a b c)
min≤ : ∀ m n → ℚ.min m n ≤ m
min≤
= elimProp2 {P = λ a b → ℚ.min a b ≤ a}
(λ x y → isProp≤ (ℚ.min x y) x)
λ { (a , b) (c , d)
→ subst2 ℤ._≤_ (sym (ℤ.·DistPosLMin (a ℤ.· ℕ₊₁→ℤ d)
(c ℤ.· ℕ₊₁→ℤ b)
(ℕ₊₁→ℕ b)))
(sym (ℤ.·Assoc a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∙
cong (a ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ b)) ∙
cong ℕ₊₁→ℤ (·₊₁-comm d b)))
(ℤ.min≤ {a ℤ.· ℕ₊₁→ℤ d ℤ.· ℕ₊₁→ℤ b}
{c ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ b}) }
≤→min : ∀ m n → m ≤ n → ℚ.min m n ≡ m
≤→min
= elimProp2 {P = λ a b → a ≤ b → ℚ.min a b ≡ a}
(λ x y → isProp→ (isSetℚ (ℚ.min x y) x))
λ { (a , b) (c , d) ad≤cb
→ eq/ (ℤ.min (a ℤ.· ℕ₊₁→ℤ d)
(c ℤ.· ℕ₊₁→ℤ b)
, b ·₊₁ d)
(a , b)
(cong (ℤ._· ℕ₊₁→ℤ b) (ℤ.≤→min ad≤cb) ∙
sym (ℤ.·Assoc a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∙
cong (a ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ b)) ∙
cong ℕ₊₁→ℤ (·₊₁-comm d b))) }
≤max : ∀ m n → m ≤ ℚ.max m n
≤max
= elimProp2 {P = λ a b → a ≤ ℚ.max a b}
(λ x y → isProp≤ x (ℚ.max x y))
λ { (a , b) (c , d)
→ subst2 ℤ._≤_ (sym (ℤ.·Assoc a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∙
cong (a ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ b)) ∙
cong ℕ₊₁→ℤ (·₊₁-comm d b)))
(sym (ℤ.·DistPosLMax (a ℤ.· ℕ₊₁→ℤ d)
(c ℤ.· ℕ₊₁→ℤ b)
(ℕ₊₁→ℕ b)))
(ℤ.≤max {a ℤ.· ℕ₊₁→ℤ d ℤ.· ℕ₊₁→ℤ b}
{c ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ b}) }
≤→max : ∀ m n → m ≤ n → ℚ.max m n ≡ n
≤→max m n
= elimProp2 {P = λ a b → a ≤ b → ℚ.max a b ≡ b}
(λ x y → isProp→ (isSetℚ (ℚ.max x y) y))
(λ { (a , b) (c , d) ad≤cb
→ eq/ (ℤ.max (a ℤ.· ℕ₊₁→ℤ d)
(c ℤ.· ℕ₊₁→ℤ b)
, b ·₊₁ d)
(c , d)
(cong (ℤ._· ℕ₊₁→ℤ d) (ℤ.≤→max ad≤cb) ∙
sym (ℤ.·Assoc c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d)) ∙
cong (c ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ d)))) }) m n
≤Dec : ∀ m n → Dec (m ≤ n)
≤Dec = elimProp2 (λ x y → isPropDec (isProp≤ x y))
λ { (a , b) (c , d) → ℤ.≤Dec (a ℤ.· ℕ₊₁→ℤ d) (c ℤ.· ℕ₊₁→ℤ b) }
<Dec : ∀ m n → Dec (m < n)
<Dec = elimProp2 (λ x y → isPropDec (isProp< x y))
λ { (a , b) (c , d) → ℤ.<Dec (a ℤ.· ℕ₊₁→ℤ d) (c ℤ.· ℕ₊₁→ℤ b) }
_≟_ : (m n : ℚ) → Trichotomy m n
m ≟ n with discreteℚ m n
... | yes m≡n = eq m≡n
... | no m≢n with inequalityImplies# m n m≢n
... | inl m<n = lt m<n
... | inr n<m = gt n<m
≤MonotoneMin : ∀ m n o s → m ≤ n → o ≤ s → ℚ.min m o ≤ ℚ.min n s
≤MonotoneMin m n o s m≤n o≤s
= subst (_≤ ℚ.min n s)
(sym (ℚ.minAssoc n s (ℚ.min m o)) ∙
cong (ℚ.min n) (ℚ.minAssoc s m o ∙
cong (λ a → ℚ.min a o) (ℚ.minComm s m) ∙
sym (ℚ.minAssoc m s o)) ∙
ℚ.minAssoc n m (ℚ.min s o) ∙
cong₂ ℚ.min (ℚ.minComm n m ∙ ≤→min m n m≤n)
(ℚ.minComm s o ∙ ≤→min o s o≤s))
(min≤ (ℚ.min n s) (ℚ.min m o))
≤MonotoneMax : ∀ m n o s → m ≤ n → o ≤ s → ℚ.max m o ≤ ℚ.max n s
≤MonotoneMax m n o s m≤n o≤s
= subst (ℚ.max m o ≤_)
(sym (ℚ.maxAssoc m o (ℚ.max n s)) ∙
cong (ℚ.max m) (ℚ.maxAssoc o n s ∙
cong (λ a → ℚ.max a s) (ℚ.maxComm o n) ∙
sym (ℚ.maxAssoc n o s)) ∙
ℚ.maxAssoc m n (ℚ.max o s) ∙
cong₂ ℚ.max (≤→max m n m≤n) (≤→max o s o≤s))
(≤max (ℚ.max m o) (ℚ.max n s))
≡Weaken≤ : ∀ m n → m ≡ n → m ≤ n
≡Weaken≤ m n m≡n = subst (m ≤_) m≡n (isRefl≤ m)
≤→≯ : ∀ m n → m ≤ n → ¬ (m > n)
≤→≯ m n m≤n n<m = isIrrefl< n (subst (n <_) (isAntisym≤ m n m≤n (<Weaken≤ n m n<m)) n<m)
≮→≥ : ∀ m n → ¬ (m < n) → m ≥ n
≮→≥ m n m≮n with discreteℚ m n
... | yes m≡n = ≡Weaken≤ n m (sym m≡n)
... | no m≢n = ∥₁.elim (λ _ → isProp≤ n m)
(⊎.rec (⊥.rec ∘ m≮n) (<Weaken≤ n m))
∣ inequalityImplies# m n m≢n ∣₁
0<+ : ∀ m n → 0 < m ℚ.+ n → (0 < m) ⊎ (0 < n)
0<+ m n 0<m+n with <Dec 0 m | <Dec 0 n
... | no 0≮m | no 0≮n = ⊥.rec (≤→≯ (m ℚ.+ n) 0 (≤Monotone+ m 0 n 0 (≮→≥ 0 m 0≮m) (≮→≥ 0 n 0≮n)) 0<m+n)
... | no _ | yes 0<n = inr 0<n
... | yes 0<m | _ = inl 0<m