---
layout: default
title : "Order module (Agda Universal Algebra Library)"
date : "2026-06-02"
author: "agda-algebras development team"
---

### Order-theoretic structures

This is the [Order][] module of the [Agda Universal Algebra Library][].

This top-level `Order/` tree collects the *order-theoretic* structures used across
the universal-algebra development.  Currently this includes a complete lattice module
(`Order.CompleteLattice`{.AgdaModule}, which the standard library lacks), and
a module codifying intervals in lattices (`Order.Interval`).  It is deliberately
separate from `Classical/`: here a lattice is an *ordered* structure (a poset with
meets and joins), whereas the `Classical.*.Lattice` modules formalize lattices *as
equational algebras* over `Sig-Lattice`.  The congruence lattice
([Setoid.Congruences.CompleteLattice][]) and the subalgebra lattice
([Setoid.Subalgebras.CompleteLattice][]) are the motivating instances.

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

module Order where

open import Order.CompleteLattice  public
open import Order.Interval         public
open import Order.Iso              public
```