Todd Waugh Ambridge, January 2024

# Orders

\begin{code}
{-# OPTIONS --without-K --safe #-}

open import MLTT.Spartan
open import UF.FunExt
open import UF.DiscreteAndSeparated
open import UF.Subsingletons
open import UF.PropTrunc
open import Quotient.Type
 using (is-prop-valued;is-equiv-relation;EqRel)
open import Notation.Order
open import Naturals.Order

module TWA.Thesis.Chapter4.ApproxOrder (fe : FunExt) where

open import TWA.Thesis.Chapter3.ClosenessSpaces fe
\end{code}

## Traditional orders

\begin{code}
is-preorder : {X : 𝓀 Μ‡ } β†’ (X β†’ X β†’ 𝓦 Μ‡ ) β†’ 𝓀 βŠ” 𝓦 Μ‡
is-preorder _≀_ = reflexive _≀_
                Γ— transitive _≀_
                Γ— is-prop-valued _≀_

is-partial-order : {X : 𝓀 Μ‡ } β†’ (X β†’ X β†’ 𝓦 Μ‡ ) β†’ 𝓀 βŠ” 𝓦 Μ‡
is-partial-order {_} {_} {X} _≀_
 = is-preorder _≀_ Γ— antisymmetric _≀_

linear :  {X : 𝓀 Μ‡ } β†’ (X β†’ X β†’ 𝓦 Μ‡ ) β†’ 𝓀 βŠ” 𝓦 Μ‡
linear {_} {_} {X} _≀_ = (x y : X) β†’ (x ≀ y) + (y ≀ x)

is-linear-preorder : {X : 𝓀 Μ‡ } β†’ (X β†’ X β†’ 𝓦 Μ‡ ) β†’ 𝓀 βŠ” 𝓦 Μ‡
is-linear-preorder {_} {_} {X} _≀_
 = is-preorder _≀_ Γ— linear _≀_

is-linear-order : {X : 𝓀 Μ‡ } β†’ (X β†’ X β†’ 𝓦 Μ‡ ) β†’ 𝓀 βŠ” 𝓦 Μ‡
is-linear-order {_} {_} {X} _≀_
 = is-partial-order _≀_ Γ— linear _≀_

discrete-reflexive-antisym-linear-order-is-decidable
 : {X : 𝓀 Μ‡ }
 β†’ is-discrete X
 β†’ (_≀_ : X β†’ X β†’ 𝓦 Μ‡ )
 β†’ reflexive _≀_
 β†’ antisymmetric _≀_
 β†’ linear _≀_
 β†’ (x y : X)
 β†’ is-decidable (x ≀ y)
discrete-reflexive-antisym-linear-order-is-decidable
 ds _≀_ r a l x y
 = Cases (ds x y) (Ξ» x=y β†’ inl (transport (x ≀_) x=y (r x)))
    (λ x≠y → Cases (l x y) inl
               (inr ∘ (Ξ» y≀x x≀y β†’ xβ‰ y (a x y x≀y y≀x))))

\end{code}

## Approximate orders

\begin{code}
is-approx-order : (X : ClosenessSpace 𝓀)
                β†’ (_≀ⁿ_ : ⟨ X ⟩ β†’ ⟨ X ⟩ β†’ β„• β†’ 𝓦' Μ‡ )
                β†’ 𝓀 βŠ” 𝓦' Μ‡
is-approx-order X _≀ⁿ_
 = ((Ο΅ : β„•) β†’ is-linear-preorder (Ξ» x y β†’ (x ≀ⁿ y) Ο΅))
 Γ— ((Ο΅ : β„•) (x y : ⟨ X ⟩) β†’ is-decidable ((x ≀ⁿ y) Ο΅))
 Γ— ((Ο΅ : β„•) (x y : ⟨ X ⟩) β†’   C X Ο΅ x y β†’ (x ≀ⁿ y) Ο΅)

≀-refl⟨_⟩
 : {X : 𝓀 Μ‡ } {_≀_ : X β†’ X β†’ 𝓦 Μ‡ }
 β†’ is-preorder _≀_
 β†’ reflexive _≀_
≀-refl⟨ r , t , p ⟩ = r

≀-trans⟨_⟩
 : {X : 𝓀 Μ‡ } {_≀_ : X β†’ X β†’ 𝓦 Μ‡ }
 β†’ is-preorder _≀_
 β†’ transitive _≀_
≀-trans⟨ r , t , p ⟩ = t

≀-prop⟨_⟩
 : {X : 𝓀 Μ‡ } {_≀_ : X β†’ X β†’ 𝓦 Μ‡ }
 β†’ is-preorder _≀_
 β†’ is-prop-valued _≀_
≀-prop⟨ r , t , p ⟩ = p

≀-pre⟨_⟩
 : {X : 𝓀 Μ‡ } {_≀_ : X β†’ X β†’ 𝓦 Μ‡ }
 β†’ is-linear-preorder _≀_
 β†’ is-preorder _≀_
≀-pre⟨ pre , l ⟩ = pre

≀-linear⟨_⟩
 : {X : 𝓀 Μ‡ } {_≀_ : X β†’ X β†’ 𝓦 Μ‡ }
 β†’ is-linear-preorder _≀_
 β†’ (x y : X) β†’ (x ≀ y) + (y ≀ x)
≀-linear⟨ pre , l ⟩ = l

≀ⁿ-all-linear
 : (X : ClosenessSpace 𝓀)
 β†’ {_≀ⁿ_ : ⟨ X ⟩ β†’ ⟨ X ⟩ β†’ β„• β†’ 𝓦' Μ‡ }
 β†’ is-approx-order X _≀ⁿ_
 β†’ (Ο΅ : β„•) β†’ is-linear-preorder (Ξ» x y β†’ (x ≀ⁿ y) Ο΅)
≀ⁿ-all-linear X (l , d , c) = l

≀ⁿ-refl
 : (X : ClosenessSpace 𝓀)
 β†’ {_≀ⁿ_ : ⟨ X ⟩ β†’ ⟨ X ⟩ β†’ β„• β†’ 𝓦' Μ‡ }
 β†’ is-approx-order X _≀ⁿ_
 β†’ (Ο΅ : β„•)
 β†’ (x : ⟨ X ⟩) β†’ (x ≀ⁿ x) Ο΅
≀ⁿ-refl X (l , d , c) Ο΅ = (pr₁ ∘ pr₁) (l Ο΅)

≀ⁿ-trans
 : (X : ClosenessSpace 𝓀)
 β†’ {_≀ⁿ_  : ⟨ X ⟩ β†’ ⟨ X ⟩ β†’ β„• β†’ 𝓦 Μ‡ }
 β†’ is-approx-order X _≀ⁿ_
 β†’ (Ο΅ : β„•) (x y z : ⟨ X ⟩)
 β†’ (x ≀ⁿ y) Ο΅ β†’ (y ≀ⁿ z) Ο΅ β†’ (x ≀ⁿ z) Ο΅
≀ⁿ-trans X (l , d , c) Ο΅ = (pr₁ ∘ prβ‚‚ ∘ pr₁) (l Ο΅)

≀ⁿ-prop
 : (X : ClosenessSpace 𝓀)
 β†’ {_≀ⁿ_ : ⟨ X ⟩ β†’ ⟨ X ⟩ β†’ β„• β†’ 𝓦' Μ‡ }
 β†’ is-approx-order X _≀ⁿ_
 β†’ (Ο΅ : β„•) (x y : ⟨ X ⟩)
 β†’ is-prop ((x ≀ⁿ y) Ο΅)
≀ⁿ-prop X (l , d , c) Ο΅ = (prβ‚‚ ∘ prβ‚‚ ∘ pr₁) (l Ο΅)

≀ⁿ-linear
 : (X : ClosenessSpace 𝓀)
 β†’ {_≀ⁿ_ : ⟨ X ⟩ β†’ ⟨ X ⟩ β†’ β„• β†’ 𝓦' Μ‡ }
 β†’ is-approx-order X _≀ⁿ_
 β†’ (Ο΅ : β„•) (x y : ⟨ X ⟩)
 β†’ (x ≀ⁿ y) Ο΅ + (y ≀ⁿ x) Ο΅
≀ⁿ-linear X (l , d , c) Ο΅ = prβ‚‚ (l Ο΅)

≀ⁿ-decidable
 : (X : ClosenessSpace 𝓀)
 β†’ {_≀ⁿ_ : ⟨ X ⟩ β†’ ⟨ X ⟩ β†’ β„• β†’ 𝓦' Μ‡ }
 β†’ is-approx-order X _≀ⁿ_
 β†’ (Ο΅ : β„•) (x y : ⟨ X ⟩)
 β†’ is-decidable ((x ≀ⁿ y) Ο΅)
≀ⁿ-decidable X (l , d , c) = d

≀ⁿ-close
 : (X : ClosenessSpace 𝓀)
 β†’ {_≀ⁿ_ : ⟨ X ⟩ β†’ ⟨ X ⟩ β†’ β„• β†’ 𝓦' Μ‡ }
 β†’ is-approx-order X _≀ⁿ_
 β†’ (Ο΅ : β„•) (x y : ⟨ X ⟩)
 β†’ C X Ο΅ x y β†’ (x ≀ⁿ y) Ο΅
≀ⁿ-close X (l , d , c) = c

module ApproxOrder-Relates (pt : propositional-truncations-exist) where

 open PropositionalTruncation pt

 _relates-toβ†’_ : {X : 𝓀 Μ‡ }
               β†’ (_≀ⁿ_ : X β†’ X β†’ β„• β†’ 𝓦' Μ‡ )
               β†’ (_≀_  : X β†’ X β†’ 𝓦 Μ‡ )
               β†’ 𝓀 βŠ” 𝓦 βŠ” 𝓦' Μ‡
 _≀ⁿx_ relates-toβ†’ _≀x_
  = βˆ€ x y β†’ ((n : β„•) β†’ (x ≀ⁿx y) n) β†’ x ≀x y

 _relates-to←_ : {X : 𝓀 Μ‡ }
               β†’ (_≀ⁿ_ : X β†’ X β†’ β„• β†’ 𝓦' Μ‡ )
               β†’ (_≀_  : X β†’ X β†’ 𝓦 Μ‡ )
               β†’ 𝓀 βŠ” 𝓦 βŠ” 𝓦' Μ‡
 _≀ⁿx_ relates-to← _≀x_
  = βˆ€ x y β†’ x ≀x y β†’ βˆƒ n κž‰ β„• , ((Ο΅ : β„•) β†’ n ≀ Ο΅ β†’ (x ≀ⁿx y) Ο΅)

 approx-order-relates : (X : ClosenessSpace 𝓀)
                      β†’ (_≀ⁿ_ : ⟨ X ⟩ β†’ ⟨ X ⟩ β†’ β„• β†’ 𝓦' Μ‡ )
                      β†’ is-approx-order X _≀ⁿ_
                      β†’ (_≀_  : ⟨ X ⟩ β†’ ⟨ X ⟩ β†’ 𝓦 Μ‡ )
                      β†’ is-preorder _≀_
                      β†’ 𝓀 βŠ” 𝓦 βŠ” 𝓦' Μ‡
 approx-order-relates X _≀ⁿ_ _ _≀_ _
  = _≀ⁿ_ relates-toβ†’ _≀_
  Γ— _≀ⁿ_ relates-to← _≀_
\end{code}

## Predicates from approximate orders

\begin{code}
approx-order-ucontinuous-l
 : (X : ClosenessSpace 𝓀)
 β†’ {_≀ⁿ_ : ⟨ X ⟩ β†’ ⟨ X ⟩ β†’ β„• β†’ 𝓦' Μ‡ }
 β†’ (a : is-approx-order X _≀ⁿ_)
 β†’ (Ξ΅ : β„•) (y : ⟨ X ⟩)
 β†’ p-ucontinuous X (Ξ» x β†’ (x ≀ⁿ y) Ξ΅ , ≀ⁿ-prop X a Ξ΅ x y)
approx-order-ucontinuous-l X a Ξ΅ y
 = Ξ΅ , (Ξ» x₁ xβ‚‚ Cx₁xβ‚‚ x₁≀ⁿy
        β†’ ≀ⁿ-trans X a Ξ΅ xβ‚‚ x₁ y
            (≀ⁿ-close X a Ξ΅ xβ‚‚ x₁ (C-sym X Ξ΅ x₁ xβ‚‚ Cx₁xβ‚‚))
            x₁≀ⁿy)

approx-order-ucontinuous-r
 : (X : ClosenessSpace 𝓀)
 β†’ {_≀ⁿ_ : ⟨ X ⟩ β†’ ⟨ X ⟩ β†’ β„• β†’ 𝓦' Μ‡ }
 β†’ (a : is-approx-order X _≀ⁿ_)
 β†’ (Ξ΅ : β„•) (y : ⟨ X ⟩)
 β†’ p-ucontinuous X (Ξ» x β†’ (y ≀ⁿ x) Ξ΅ , ≀ⁿ-prop X a Ξ΅ y x)
approx-order-ucontinuous-r X a Ξ΅ y
 = Ξ΅ , (Ξ» x₁ xβ‚‚ Cx₁xβ‚‚ x₁≀ⁿy
        β†’ ≀ⁿ-trans X a Ξ΅ y x₁ xβ‚‚
            x₁≀ⁿy
            (≀ⁿ-close X a Ξ΅ x₁ xβ‚‚ Cx₁xβ‚‚))

approx-order-uc-predicate-l : (X : ClosenessSpace 𝓀)
                            β†’ (_≀ⁿ_ : ⟨ X ⟩ β†’ ⟨ X ⟩ β†’ β„• β†’ 𝓦 Μ‡ )
                            β†’ is-approx-order X _≀ⁿ_
                            β†’ (Ο΅ : β„•) (y : ⟨ X ⟩)
                            β†’ decidable-uc-predicate 𝓦 X
approx-order-uc-predicate-l X _≀ⁿ_ a Ο΅ y
 = ((Ξ» x β†’ (x ≀ⁿ y) Ο΅ , ≀ⁿ-prop X a Ο΅ x y)
 , Ξ» x β†’ ≀ⁿ-decidable X a Ο΅ x y)
 , approx-order-ucontinuous-l X a Ο΅ y

approx-order-uc-predicate-r : (X : ClosenessSpace 𝓀)
                            β†’ (_≀ⁿ_ : ⟨ X ⟩ β†’ ⟨ X ⟩ β†’ β„• β†’ 𝓦 Μ‡ )
                            β†’ is-approx-order X _≀ⁿ_
                            β†’ (Ο΅ : β„•) (y : ⟨ X ⟩)
                            β†’ decidable-uc-predicate 𝓦 X
approx-order-uc-predicate-r X _≀ⁿ_ a Ο΅ y
 = ((Ξ» x β†’ (y ≀ⁿ x) Ο΅ , ≀ⁿ-prop X a Ο΅ y x)
 , Ξ» x β†’ ≀ⁿ-decidable X a Ο΅ y x)
 , approx-order-ucontinuous-r X a Ο΅ y

approx-order-f-uc-predicate-l : (X : ClosenessSpace 𝓀)
                              β†’ (Y : ClosenessSpace π“₯)
                              β†’ (f : ⟨ X ⟩ β†’ ⟨ Y ⟩)
                              β†’ f-ucontinuous X Y f
                              β†’ (_≀ⁿ_ : ⟨ Y ⟩ β†’ ⟨ Y ⟩ β†’ β„• β†’ 𝓦 Μ‡ )
                              β†’ is-approx-order Y _≀ⁿ_
                              β†’ (Ο΅ : β„•) (y : ⟨ Y ⟩)
                              β†’ decidable-uc-predicate 𝓦 X
approx-order-f-uc-predicate-l X Y f Ο• _≀ⁿ_ a Ο΅ y
 = ((Ξ» x β†’ (f x ≀ⁿ y) Ο΅ , ≀ⁿ-prop Y a Ο΅ (f x) y)
 , (Ξ» x β†’ ≀ⁿ-decidable Y a Ο΅ (f x) y))
 , p-ucontinuous-comp X Y f Ο•
     (Ξ» x β†’ (x ≀ⁿ y) Ο΅ , ≀ⁿ-prop Y a Ο΅ x y)
     (approx-order-ucontinuous-l Y a Ο΅ y)

approx-order-f-uc-predicate-r : (X : ClosenessSpace 𝓀)
                              β†’ (Y : ClosenessSpace π“₯)
                              β†’ (f : ⟨ X ⟩ β†’ ⟨ Y ⟩)
                              β†’ f-ucontinuous X Y f
                              β†’ (_≀ⁿ_ : ⟨ Y ⟩ β†’ ⟨ Y ⟩ β†’ β„• β†’ 𝓦 Μ‡ )
                              β†’ is-approx-order Y _≀ⁿ_
                              β†’ (Ο΅ : β„•) (y : ⟨ Y ⟩)
                              β†’ decidable-uc-predicate 𝓦 X
approx-order-f-uc-predicate-r X Y f Ο• _≀ⁿ_ a Ο΅ y
 = ((Ξ» x β†’ (y ≀ⁿ f x) Ο΅ , ≀ⁿ-prop Y a Ο΅ y (f x))
 , (Ξ» x β†’ ≀ⁿ-decidable Y a Ο΅ y (f x)))
 , p-ucontinuous-comp X Y f Ο•
     (Ξ» x β†’ (y ≀ⁿ x) Ο΅ , ≀ⁿ-prop Y a Ο΅ y x)
     (approx-order-ucontinuous-r Y a Ο΅ y)
\end{code}