Notation.Order

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}