    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Creates trivially indexed records from their non-indexed counterpart.
    ------------------------------------------------------------------------

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

    module Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
      {i} {I : Set i} where

    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Bundles using (Setoid; Preorder)
    open import Relation.Binary.Structures using (IsEquivalence; IsPreorder)
    open import Relation.Binary.Indexed.Heterogeneous
      using (IndexedSetoid; IndexedPreorder
            ; IsIndexedEquivalence; IsIndexedPreorder)

    ------------------------------------------------------------------------
    -- Structures

    module _ {a} {A : Set a} where

      private
        Aᵢ : I → Set a
        Aᵢ i = A

      isIndexedEquivalence : ∀ {ℓ} {_≈_ : Rel A ℓ} → IsEquivalence _≈_ →
                             IsIndexedEquivalence Aᵢ _≈_
      isIndexedEquivalence isEq = record
        { refl  = refl
        ; sym   = sym
        ; trans = trans
        }
        where open IsEquivalence isEq

      isIndexedPreorder : ∀ {ℓ₁ ℓ₂} {_≈_ : Rel A ℓ₁} {_∼_ : Rel A ℓ₂} →
                          IsPreorder _≈_ _∼_ →
                          IsIndexedPreorder Aᵢ _≈_ _∼_
      isIndexedPreorder isPreorder = record
        { isEquivalence = isIndexedEquivalence isEquivalence
        ; reflexive     = reflexive
        ; trans         = trans
        }
        where open IsPreorder isPreorder

    ------------------------------------------------------------------------
    -- Bundles

    indexedSetoid : ∀ {a ℓ} → Setoid a ℓ → IndexedSetoid I a ℓ
    indexedSetoid S = record
      { isEquivalence = isIndexedEquivalence isEquivalence
      }
      where open Setoid S

    indexedPreorder : ∀ {a ℓ₁ ℓ₂} → Preorder a ℓ₁ ℓ₂ →
                      IndexedPreorder I a ℓ₁ ℓ₂
    indexedPreorder O = record
      { isPreorder = isIndexedPreorder isPreorder
      }
      where open Preorder O