Contents Previous Next


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

open import Types.equality using (IsEquivalence; Reflexive; Symmetric; Transitive; Rel; __)
open import Types.product using (Σ; _,_; __)

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

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 objects each with progressively stricter laws.


Preorders are relations which are reflexive and transitive. The property of symmetry is left out, and in such a way, preorders are even more general (less strict) than equivalences. We define a pre-order set of objects with an underlying notion of equality _==_.

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

  record IsPreorder (__ : Rel A ℓ) : Set (a ⊔ ℓ) where
      isEquivalence : IsEquivalence _==_
      -- Reflexivity is expressed in terms of an underlying equality,
      -- reflexivity of the underlying equality implies reflexivity of the relation:
      reflexive     : _==___
      trans         : Transitive __

    module Eq = IsEquivalence isEquivalence

    refl : Reflexive __
    refl = reflexive Eq.rfl

    -- we ensure the relation _∼_ respects the underlying equality:
    -- we cannot use commutativity, hence we use the _Respects₂_ version here.
    ∼-respˡ-== : __ Respectsˡ _==_
    ∼-respˡ-== x==y x∼z = trans (reflexive (Eq.sym x==y)) x∼z

    ∼-respʳ-== : __ Respectsʳ _==_
    ∼-respʳ-== x==y z∼x = trans z∼x (reflexive x==y)

    ∼-resp-== : __ Respects₂ _==_
    ∼-resp-== = ∼-respʳ-== , ∼-respˡ-==

Partial Order or Poset

A partial order, or partially ordered set or Poset, is an antisymmetric preorder. In plain words, we require the relation $ $ to be antisymmetric.

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
      isPreorder : IsPreorder __
      antisym    : Antisymmetric _==_ __

    open IsPreorder isPreorder public
      ( ∼-respˡ-== to ≤-respˡ-==
      ; ∼-respʳ-== to ≤-respʳ-==
      ; ∼-resp-==  to ≤-resp-==

Total Order

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 $. There is no third possibility.

  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
      isPartialOrder : IsPartialOrder __
      total          : Total __

    open IsPartialOrder isPartialOrder public

Groups and family