    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Homogeneously-indexed binary relations
    ------------------------------------------------------------------------

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

    module Relation.Binary.Indexed.Homogeneous where

    ------------------------------------------------------------------------
    -- Publicly export core definitions

    open import Relation.Binary.Indexed.Homogeneous.Core public
    open import Relation.Binary.Indexed.Homogeneous.Definitions public
    open import Relation.Binary.Indexed.Homogeneous.Structures public
    open import Relation.Binary.Indexed.Homogeneous.Bundles public