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

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

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

    module Relation.Binary.Indexed.Homogeneous.Core where

    open import Level using (Level; _⊔_)
    open import Data.Product.Base using (_×_)
    open import Relation.Binary.Core as B using (REL; Rel)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
    import Relation.Binary.Indexed.Heterogeneous as I using (IREL)
    open import Relation.Unary.Indexed using (IPred)

    private
      variable
        a b c ℓ : Level
        I : Set c

    ------------------------------------------------------------------------
    -- Homegeneously indexed binary relations

    -- Heterogeneous types

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

    -- Homogeneous types

    IRel : (I → Set a) → (ℓ : Level) → Set _
    IRel A = IREL A A

    ------------------------------------------------------------------------
    -- Lifting to non-indexed binary relations

    -- Ideally this should be in: `Construct.Lift` but we want this relation
    -- to be exported by the various structures & bundles.

    Lift : (A : I → Set a) → IRel A ℓ → Rel (∀ i → A i) _
    Lift _ _∼_ x y = ∀ i → x i ∼ y i

    ------------------------------------------------------------------------
    -- Conversion between homogeneous and heterogeneously indexed relations

    module _ {i a b} {I : Set i} {A : I → Set a} {B : I → Set b} where

      OverPath : ∀ {ℓ} → IREL A B ℓ → ∀ {i j} → i ≡ j → REL (A i) (B j) ℓ
      OverPath _∼_ refl = _∼_

      toHetIndexed : ∀ {ℓ} → IREL A B ℓ → I.IREL A B (i ⊔ ℓ)
      toHetIndexed _∼_ {i} {j} x y = (p : i ≡ j) → OverPath _∼_ p x y

      fromHetIndexed : ∀ {ℓ} → I.IREL A B ℓ → IREL A B ℓ
      fromHetIndexed _∼_ = _∼_