    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Indexed binary relations
    ------------------------------------------------------------------------

    -- The contents of this module should be accessed via
    -- `Relation.Binary.Indexed.Heterogeneous`.

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

    module Relation.Binary.Indexed.Heterogeneous.Core where

    open import Level using (Level)
    import Relation.Binary.Core as B using (Rel; REL; _⇒_)

    ------------------------------------------------------------------------
    -- Indexed binary relations

    -- Heterogeneous types

    IREL : ∀ {i₁ i₂ a₁ a₂} {I₁ : Set i₁} {I₂ : Set i₂} →
          (I₁ → Set a₁) → (I₂ → Set a₂) → (ℓ : Level) → Set _
    IREL A₁ A₂ ℓ = ∀ {i₁ i₂} → A₁ i₁ → A₂ i₂ → Set ℓ

    -- Homogeneous types

    IRel : ∀ {i a} {I : Set i} → (I → Set a) → (ℓ : Level) → Set _
    IRel A ℓ = IREL A A ℓ

    ------------------------------------------------------------------------
    -- Generalised implication.

    infixr 4 _=[_]⇒_

    _=[_]⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : A → Set b} →
              B.Rel A ℓ₁ → ((x : A) → B x) → IRel B ℓ₂ → Set _
    P =[ f ]⇒ Q = ∀ {i j} → P i j → Q (f i) (f j)