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

{-# OPTIONS --without-K --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