Contents Previous Next


Introduction

open import Agda.Primitive using (Level; __; lsuc; lzero)

open import Types.relations
open import Types.equality
open import Types.product using (Σ; _,_; __)

module Algebra.order {a ℓ} {A : Set a} (_==_ : Rel A ℓ) where

The equivalence relation remains the most basic relation to be built on objects of all kinds. Higher relations which tend to impose further structural constraints on objects thus creating richer objects and their APIs capable of modeling more complex phenomenon (not much unlike how a programming language’s expressiveness enables one to build more complex programs).

Order is one such higher relation and is fundamental in building a class of structures. There are different kinds of ordered relations each with progressively stricter laws.

Relation Reflexivity Transitivity Antisymmetry Total
Pre-order
Partial-order
Total order

Preorder

Preorders are binary relations (~ : A → A) on a set where:

  1. ~ is reflexive, i.e. x ∼ x
  2. ~ is transitive, i.e. x ∼ y and y ∼ z ⇒ x ∼ z

Preorders are relations which are reflexive and transitive.

We first define an object that encapsulates all the rules into one record:

  record IsPreorder (__ : Rel A ℓ) : Set (a ⊔ ℓ) where
    field
      reflexive     : Reflexive __
      trans         : Transitive __

Partial Order or Poset

Partial orders are a subtype of pre-orders where ≤ : A → A:

  1. is reflexive, i.e. x ≤ x
  2. is transitive, i.e. x ≤ y and y ≤ z ⇒ x ≤ z
  3. is antisymmetric, i.e. x ≤ y and y ≤ x ⇒ x = y

A partial order, or partially ordered set or Poset, is an antisymmetric preorder. In plain words, we require the relation _≤_ to be antisymmetric with respect to the underlying equality .

A relation _≤_ is anti-symmetric over the underlying equality _==_, if for every x, y,

\[ x ≤ y , y ≤ x ⟹ x == y \]

  Antisymmetric : Rel A ℓ  Rel A ℓ  Set _
  Antisymmetric _==_ __ =  {x y}  x ≤ y  y ≤ x  x == y

We can now define partially ordered sets:

  record IsPartialOrder (__ : Rel A ℓ) : Set (a ⊔ ℓ) where
    field
      isPreorder : IsPreorder __
      antisym    : Antisymmetric _==_ __

Total Order

Total orders are binary relations ≤ : A → A where:

  1. is reflexive, i.e. x ≤ x
  2. is transitive, i.e. x ≤ y and y ≤ z ⇒ x ≤ z
  3. is antisymmetric, i.e. x ≤ y and y ≤ x ⇒ x = y
  4. is a total relation, i.e. ∀ x and y : x ≤ y or y ≤ x

Total orders are a further constrained subtype of posets. All pairs of elements contained in a poset need not be comparable. This is exactly what total orders represent. A total order is a total preorder, or the preorder’s relation _≤_ to be a total function.

A relation _≤_ is total if x ≤ y or y ≤ x. This relation has to exist between any pair of elements of A:

  Total : {A : Set a}  Rel A ℓ  Set _
  Total __ =  x y  (x ∼ y)(y ∼ x)

We can now define total orders:

  record IsTotalOrder (__ : Rel A ℓ) : Set (a ⊔ ℓ) where
    field
      isPartialOrder : IsPartialOrder __
      total          : Total __

    open IsPartialOrder isPartialOrder public

Groups and family