    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Order-theoretic lattices
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Relation.Binary.Lattice where

    ------------------------------------------------------------------------
    -- Re-export various components of the lattice hierarchy

    open import Relation.Binary.Lattice.Definitions public
    open import Relation.Binary.Lattice.Structures public
    open import Relation.Binary.Lattice.Bundles public