------------------------------------------------------------------------
-- The Agda standard library
--
-- Instantiates indexed binary structures at an index to the equivalent
-- non-indexed structures.
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Relation.Binary.Indexed.Heterogeneous.Construct.At where
 
open import Relation.Binary.Bundles using (Setoid; Preorder)
open import Relation.Binary.Structures using (IsEquivalence; IsPreorder)
open import Relation.Binary.Indexed.Heterogeneous
  using (IRel; IsIndexedEquivalence; IsIndexedPreorder; IndexedSetoid
        ; IndexedPreorder)
 
------------------------------------------------------------------------
-- Structures
 
module _ {a i} {I : Set i} {A : I → Set a} where
 
  isEquivalence : ∀ {ℓ} {_≈_ : IRel A ℓ} → IsIndexedEquivalence A _≈_ →
                  (index : I) → IsEquivalence (_≈_ {index})
  isEquivalence isEq index = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
    where open IsIndexedEquivalence isEq
 
  isPreorder : ∀ {ℓ₁ ℓ₂} {_≈_ : IRel A ℓ₁} {_≲_ : IRel A ℓ₂} →
               IsIndexedPreorder A _≈_ _≲_ →
               (index : I) → IsPreorder (_≈_ {index}) _≲_
  isPreorder isPreorder index = record
    { isEquivalence = isEquivalence O.isEquivalence index
    ; reflexive     = O.reflexive
    ; trans         = O.trans
    }
    where module O = IsIndexedPreorder isPreorder
 
------------------------------------------------------------------------
-- Bundles
 
module _ {a i} {I : Set i} where
 
  setoid : ∀ {ℓ} → IndexedSetoid I a ℓ → I → Setoid a ℓ
  setoid S index = record
    { Carrier       = S.Carrier index
    ; _≈_           = S._≈_
    ; isEquivalence = isEquivalence S.isEquivalence index
    }
    where module S = IndexedSetoid S
 
  preorder : ∀ {ℓ₁ ℓ₂} → IndexedPreorder I a ℓ₁ ℓ₂ → I → Preorder a ℓ₁ ℓ₂
  preorder O index = record
    { Carrier    = O.Carrier index
    ; _≈_        = O._≈_
    ; _≲_        = O._≲_
    ; isPreorder = isPreorder O.isPreorder index
    }
    where module O = IndexedPreorder O
 
------------------------------------------------------------------------
-- Some useful shorthand infix notation
 
module _ {a i} {I : Set i} where
 
  infixr -1 _atₛ_
 
  _atₛ_ : ∀ {ℓ} → IndexedSetoid I a ℓ → I → Setoid a ℓ
  _atₛ_ = setoid