    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties of homogeneous binary relations
    ------------------------------------------------------------------------

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

    module Relation.Binary where

    ------------------------------------------------------------------------
    -- Re-export various components of the binary relation hierarchy

    open import Relation.Binary.Core public
    open import Relation.Binary.Definitions public
    open import Relation.Binary.Structures public
    open import Relation.Binary.Structures.Biased public
    open import Relation.Binary.Bundles public