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

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

    module Relation.Binary.Indexed.Heterogeneous where

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

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