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 the complete lattice (Order.CompleteLattice), which the standard library lacks. 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 --cubical-compatible --exact-split --safe #-}

module Order where

open import Order.CompleteLattice public