Order

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, 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.

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

module Order where

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