---
layout: default
file: "src/Classical/Structures/Lattice.lagda.md"
title: "Classical.Structures.Lattice module"
date: "2026-07-25"
author: "the agda-algebras development team"
---

### Lattices {#classical-structures-lattices}

This is the [Classical.Structures.Lattice][] module of the [Agda Universal Algebra Library][].

```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Classical.Structures.Lattice where

open import Classical.Structures.Lattice.Basic                public
open import Classical.Structures.Lattice.DistributiveLattice  public
open import Classical.Structures.Lattice.Dual                 public
open import Classical.Structures.Lattice.OrdinalSum           public
open import Classical.Structures.Lattice.Parachute            public
open import Classical.Structures.Lattice.Partitions           public
open import Classical.Structures.Lattice.Product              public

```