------------------------------------------------------------------------
-- 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

------------------------------------------------------------------------
-- 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