Skip to content

agda-lattices

Lattice theory in Agda, on top of the Agda Universal Algebra Library, after Freese, Ježek and Nation's Free Lattices. Every module is checked by Agda under --without-K --exact-split --safe.

Browse the library Check it yourself GitHub

What it is

agda-lattices is a library of general lattice theory, written in literate Agda. It covers free lattices (lattice terms, Whitman's solution of the word problem, the free lattice and its universal property, canonical forms, Whitman's condition and semidistributivity, substitutions, free generating sets, embeddings and complexity, Whitman's countable family, and the polynomial-time decision of the order), free generation and breadth in lattices satisfying Whitman's condition, Nation's theorem and its proof for finite lattices, bounded homomorphisms, projective lattices and Kostinsky's theorem, quotients, intervals, modular and distributive lattices, central elements and direct decompositions, finite products, lattices given by their operation tables, and worked examples.

The reference throughout is R. Freese, J. Ježek and J. B. Nation, Free Lattices, Mathematical Surveys and Monographs 42, American Mathematical Society, 1995 (Freese, Ježek, and Nation (1995); FJN below), cited by theorem number. The library is built on the algebras, terms, homomorphisms and congruences of the Agda Universal Algebra Library.

Reading the code

Every page is rendered from the literate source that Agda checks, so the proof you read is the proof that compiles. In the code blocks every token is colored by its role and links to its definition: on this site for the library's own names, on the Agda Universal Algebra Library's site for its names, and among the standard library's pages for the rest. Each module's import scaffolding is folded away; the Show all Agda switch in the header shows it.

  •   Free lattices

    Lattice terms, Whitman's solution of the word problem and its decision, the free lattice FL(X) and its universal property, canonical forms.

    Lattices.Free

  •   Nation's theorem

    Nation's argument of FJN Section V.3, on finite lattices given by their operation tables.

    Lattices.Nation

  •   Kostinsky's theorem

    Bounded homomorphisms, projective lattices, and the equivalence for a finitely generated lattice.

    Lattices.Kostinsky

  •   The sibling library

    The Agda Universal Algebra Library: signatures, algebras, homomorphisms, terms, varieties, and Birkhoff's HSP theorem.

    agda-algebras

The modules

Every module is under Lattices; the names below drop that prefix. The navigation lists the same modules as a tree.

What is checked

Every module carries the pragma {-# OPTIONS --without-K --exact-split --safe #-}. Under --safe Agda refuses postulates, unsafe primitives and non-terminating definitions, so every theorem is proved from the type theory alone. A worked example may add --lossy-unification, which --safe accepts; Examples.Central uses it, and says why.

A statement proved by induction is checked when its proof term has the stated type. A statement about explicit terms or finite lattices is checked by computation: Whitman's procedure is a decision s ≤ʷ? t, the properties of a lattice given by its tables are decided, and Agda evaluates the decision while it checks the module.

Checking it

The toolchain is a Nix flake, so a machine with Nix 2.28 or later, with flakes enabled, needs nothing else:

git clone https://github.com/ualib/agda-lattices.git
cd agda-lattices
nix develop --command make check

make check checks every module's pragma, then type-checks every module under src/. It exits 0 when every module checks; there is no separate test step, since type-checking is the test. The Agda is a pre-release of Agda 2.9.0, which Nix builds from source in about an hour unless it can fetch it from the public binary cache formalverification on Cachix; the README says how to use it, and which commits of Agda, the standard library and the Agda Universal Algebra Library the flake pins.

Citing it

The repository's CITATION.cff gives the metadata for citing the library, and GitHub's "Cite this repository" button formats it. The library is licensed under the Apache License 2.0; its NOTICE records the attribution it carries from the Agda Universal Algebra Library, where its first modules were first written.