    ------------------------------------------------------------------------
    -- 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.Bundles where

    open import Level using (suc; _⊔_)
    open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
    open import Relation.Binary.Indexed.Heterogeneous.Structures
      using (IsIndexedEquivalence; IsIndexedPreorder)

    ------------------------------------------------------------------------
    -- Definitions

    record IndexedSetoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where
      infix 4 _≈_
      field
        Carrier       : I → Set c
        _≈_           : IRel Carrier ℓ
        isEquivalence : IsIndexedEquivalence Carrier _≈_

      open IsIndexedEquivalence isEquivalence public

    record IndexedPreorder {i} (I : Set i) c ℓ₁ ℓ₂ :
                           Set (suc (i ⊔ c ⊔ ℓ₁ ⊔ ℓ₂)) where
      infix 4 _≈_ _≲_
      field
        Carrier    : I → Set c
        _≈_        : IRel Carrier ℓ₁  -- The underlying equality.
        _≲_        : IRel Carrier ℓ₂  -- The relation.
        isPreorder : IsIndexedPreorder Carrier _≈_ _≲_

      open IsIndexedPreorder isPreorder public

      infix 4 _∼_
      _∼_ = _≲_

    ------------------------------------------------------------------------
    -- DEPRECATED
    ------------------------------------------------------------------------
    -- Please use the new names as continuing support for the old names is
    -- not guaranteed.

    -- Version 2.0

    {-# WARNING_ON_USAGE IndexedPreorder._∼_
    "Warning: IndexedPreorder._∼_ was deprecated in v2.0. Please use IndexedPreorder._≲_ instead. "
    #-}