Cartesian Coordinate Pairs in the 2-Space of Naturals is a Partial Order, but not a Total Order

Point.agda

module Point where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; trans)
open import Relation.Nullary using (¬_)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Function using (_∘_)
open import Data.Nat.Properties using (+-comm; +-identityʳ)
open import Data.Product using (∃-syntax; _,_; _×_; -,_)

data _ℕ≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n : ℕ} → zero ℕ≤ n
  s≤s : ∀ {m n : ℕ} → m ℕ≤ n → suc m ℕ≤ suc n

ℕ≤-refl : ∀ {n : ℕ} → n ℕ≤ n
ℕ≤-refl {zero} = z≤n
ℕ≤-refl {suc _} = s≤s ℕ≤-refl

ℕ≤-trans : ∀ {m n p : ℕ} → m ℕ≤ n → n ℕ≤ p → m ℕ≤ p
ℕ≤-trans z≤n       _          =  z≤n
ℕ≤-trans (s≤s m≤n) (s≤s n≤p)  =  s≤s (ℕ≤-trans m≤n n≤p)

ℕ≤-antisym : ∀ {m n : ℕ} → m ℕ≤ n → n ℕ≤ m → m ≡ n
ℕ≤-antisym z≤n       z≤n        =  refl
ℕ≤-antisym (s≤s m≤n) (s≤s n≤m)  =  cong suc (ℕ≤-antisym m≤n n≤m)

¬sucn≤n : ∀{n : ℕ} → ¬ suc n ℕ≤ n
¬sucn≤n {zero} ()
¬sucn≤n {suc n} (s≤s prf) = ¬sucn≤n {n} prf

record ℕ² : Set where
  constructor [_,_]
  field x y : ℕ

[,]-monoʳ-≡ : ∀ {n p q : ℕ} → p ≡ q → [ n , p ] ≡ [ n , q ]
[,]-monoʳ-≡ {n} = cong [ n ,_]

[,]-monoˡ-≡ : ∀ {n p q : ℕ} → p ≡ q → [ p , n ] ≡ [ q , n ]
[,]-monoˡ-≡ {n} = cong [_, n ]

[,]-mono-≡ : ∀{m n p q : ℕ} → m ≡ n → p ≡ q → [ m , p ] ≡ [ n , q ]
[,]-mono-≡ m≡n p≡q = trans ([,]-monoʳ-≡ p≡q) ([,]-monoˡ-≡ m≡n)

origin : ℕ²
origin = [ zero , zero ]

sucx : ℕ² → ℕ²
sucx [ x , y ] = [ suc x , y ]

sucy : ℕ² → ℕ²
sucy [ x , y ] = [ x , suc y ]

sucxy : ℕ² → ℕ²
sucxy = sucx ∘ sucy

data _ℕ²≤_ : ℕ² → ℕ² → Set where
  p≤q : ∀ {p₁ p₂ q₁ q₂ : ℕ} → p₁ ℕ≤ q₁ → p₂ ℕ≤ q₂ → [ p₁ , p₂ ] ℕ²≤ [ q₁ , q₂ ]

ℕ²≤-refl : ∀ {p : ℕ²} → p ℕ²≤ p
ℕ²≤-refl = p≤q ℕ≤-refl ℕ≤-refl

ℕ²≤-trans : ∀ {p q r : ℕ²} → p ℕ²≤ q → q ℕ²≤ r → p ℕ²≤ r
ℕ²≤-trans (p≤q p₁≤q₁ p₂≤q₂) (p≤q q₁≤r₁ q₂≤r₂) =
  p≤q (ℕ≤-trans p₁≤q₁ q₁≤r₁) (ℕ≤-trans p₂≤q₂ q₂≤r₂)

ℕ²≤-antisym : ∀ {p q : ℕ²} → p ℕ²≤ q → q ℕ²≤ p → p ≡ q
ℕ²≤-antisym {[ p₁ , p₂ ]} {[ q₁ , q₂ ]} (p≤q p₁≤q₁ p₂≤q₂) (p≤q q₁≤p₁ q₂≤p₂) =
  [,]-mono-≡ (ℕ≤-antisym p₁≤q₁ q₁≤p₁) (ℕ≤-antisym p₂≤q₂ q₂≤p₂)

axes-diverge¹ : (p : ℕ²) → ¬ sucx p ℕ²≤ sucy p
axes-diverge¹ [ zero , _ ] (p≤q () _)
axes-diverge¹ [ suc _ , _ ] (p≤q sucn≤n _) = ¬sucn≤n sucn≤n

axes-diverge² : (p : ℕ²) → ¬ sucy p ℕ²≤ sucx p
axes-diverge² [ _ , zero ] (p≤q _ ())
axes-diverge² [ _ , suc _ ] (p≤q _ sucn≤n) = ¬sucn≤n sucn≤n

ℕ²≤-partial : ∃[ p ](∃[ q ](¬ p ℕ²≤ q × ¬ q ℕ²≤ p))
ℕ²≤-partial = -, -, axes-diverge² origin , axes-diverge¹ origin