Martin Escardo 31st December 2021

Type-class for notation for strict orders.

\begin{code}

{-# OPTIONS --safe --without-K --exact-split #-}

module Notation.Order where

open import MLTT.Spartan

record Strict-Order {ð“Ī} {ð“Ĩ} {ð“Ķ} (X : ð“Ī Ė‡ ) (Y : ð“Ĩ Ė‡ ) : (ð“Ī ⊔ ð“Ĩ ⊔ ð“Ķ)⁚ Ė‡  where
 field
   _<_ : X → Y → ð“Ķ  Ė‡

 _â‰Ū_ : X → Y → ð“Ķ Ė‡
 _>_ _â‰Ŋ_ : Y → X → ð“Ķ Ė‡

 x â‰Ū y = ÂŽ(x < y)
 y > x = x < y
 y â‰Ŋ x = ÂŽ (y > x)

 infix 30 _<_
 infix 30 _>_
 infix 30 _â‰Ū_
 infix 30 _â‰Ŋ_

open Strict-Order {{...}} public

record Order {ð“Ī} {ð“Ĩ} {ð“Ķ} (X : ð“Ī Ė‡ ) (Y : ð“Ĩ Ė‡ ) : (ð“Ī ⊔ ð“Ĩ ⊔ ð“Ķ)⁚ Ė‡  where
 field
   _â‰Ī_ : X → Y → ð“Ķ  Ė‡

 _≰_ : X → Y → ð“Ķ Ė‡
 _â‰Ĩ_ _≱_ : Y → X → ð“Ķ Ė‡

 x ≰ y = ÂŽ(x â‰Ī y)
 y â‰Ĩ x = x â‰Ī y
 y ≱ x = ÂŽ(y â‰Ĩ x)

 infix 30 _â‰Ī_
 infix 30 _â‰Ĩ_
 infix 30 _≰_
 infix 30 _≱_


open Order {{...}} public

record Strict-Square-Order {ð“Ī} {ð“Ĩ} {ð“Ķ} (X : ð“Ī Ė‡ ) (Y : ð“Ĩ Ė‡ ) : (ð“Ī ⊔ ð“Ĩ ⊔ ð“Ķ)⁚ Ė‡  where
 field
   _⊏_ : X → Y → ð“Ķ  Ė‡

 _⊐_ : Y → X → ð“Ķ Ė‡
 x ⊐ y = y ⊏ x

 infix 30 _⊏_
 infix 30 _⊐_

open Strict-Square-Order {{...}} public

record Square-Order {ð“Ī} {ð“Ĩ} {ð“Ķ} (X : ð“Ī Ė‡ ) (Y : ð“Ĩ Ė‡ ) : (ð“Ī ⊔ ð“Ĩ ⊔ ð“Ķ)⁚ Ė‡  where
 field
   _⊑_ : X → Y → ð“Ķ  Ė‡

 _⊒_ : Y → X → ð“Ķ Ė‡
 x ⊒ y = y ⊑ x

 infix 30 _⊑_
 infix 30 _⊒_

open Square-Order {{...}} public

record Strict-Curly-Order {ð“Ī} {ð“Ĩ} {ð“Ķ} (X : ð“Ī Ė‡ ) (Y : ð“Ĩ Ė‡ ) : (ð“Ī ⊔ ð“Ĩ ⊔ ð“Ķ)⁚ Ė‡  where
 field
   _≹_ : X → Y → ð“Ķ  Ė‡

 _â‰ŧ_ : Y → X → ð“Ķ Ė‡
 x â‰ŧ y = y ≹ x

 infix 30 _≹_
 infix 30 _â‰ŧ_

open Strict-Curly-Order {{...}} public

record Curly-Order {ð“Ī} {ð“Ĩ} {ð“Ķ} (X : ð“Ī Ė‡ ) (Y : ð“Ĩ Ė‡ ) : (ð“Ī ⊔ ð“Ĩ ⊔ ð“Ķ)⁚ Ė‡  where
 field
   _≾_ : X → Y → ð“Ķ  Ė‡

 _â‰―_ : Y → X → ð“Ķ Ė‡
 x â‰― y = y ≾ x

 infix 30 _≾_
 infix 30 _â‰―_

open Curly-Order {{...}} public

record Strict-Order-Chain {ð“Ī} {ð“Ĩ} {ð“Ķ} {ð“Ģ} {𝓧 : Universe}
 (X : ð“Ī Ė‡) (Y : ð“Ĩ Ė‡) (Z : ð“Ķ Ė‡)
 (_<₁_ : X → Y → ð“Ģ Ė‡)
 (_<₂_ : Y → Z → 𝓧 Ė‡) :  (ð“Ī ⊔ ð“Ĩ ⊔ ð“Ķ ⊔ ð“Ģ ⊔ 𝓧)⁚ Ė‡ where
 field
  _<_<_ : X → Y → Z → ð“Ģ ⊔ 𝓧 Ė‡

 infix 30 _<_<_

open Strict-Order-Chain {{...}} public

record Order-Chain {ð“Ī} {ð“Ĩ} {ð“Ķ} {ð“Ģ} {𝓧 : Universe}
 (X : ð“Ī Ė‡) (Y : ð“Ĩ Ė‡) (Z : ð“Ķ Ė‡)
 (_â‰Ī₁_ : X → Y → ð“Ģ Ė‡)
 (_â‰Ī₂_ : Y → Z → 𝓧 Ė‡) :  (ð“Ī ⊔ ð“Ĩ ⊔ ð“Ķ ⊔ ð“Ģ ⊔ 𝓧)⁚ Ė‡ where
 field
  _â‰Ī_â‰Ī_ : X → Y → Z → ð“Ģ ⊔ 𝓧 Ė‡

 infix 30 _â‰Ī_â‰Ī_

open Order-Chain {{...}} public

\end{code}