------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed binary relations
------------------------------------------------------------------------
 
-- The contents of this module should be accessed via
-- `Relation.Binary.Indexed.Heterogeneous`.
 
{-# OPTIONS --cubical-compatible --safe #-}
 
open import Relation.Binary.Indexed.Heterogeneous.Core
 
module Relation.Binary.Indexed.Heterogeneous.Structures
  {i a ℓ} {I : Set i} (A : I → Set a) (_≈_ : IRel A ℓ)
  where
 
open import Function.Base using (id; _⟨_⟩_)
open import Level using (suc; _⊔_)
open import Relation.Binary.Core using (_⇒_)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
open import Relation.Binary.Indexed.Heterogeneous.Definitions
  using (Reflexive; Symmetric; Transitive)
 
------------------------------------------------------------------------
-- Equivalences
 
record IsIndexedEquivalence : Set (i ⊔ a ⊔ ℓ) where
  field
    refl  : Reflexive  A _≈_
    sym   : Symmetric  A _≈_
    trans : Transitive A _≈_
 
  reflexive : ∀ {i} → _≡_ ⟨ _⇒_ ⟩ _≈_ {i}
  reflexive ≡.refl = refl
 
 
record IsIndexedPreorder {ℓ₂} (_≲_ : IRel A ℓ₂) : Set (i ⊔ a ⊔ ℓ ⊔ ℓ₂) where
  field
    isEquivalence : IsIndexedEquivalence
    reflexive     : ∀ {i j} → (_≈_ {i} {j}) ⟨ _⇒_ ⟩ _≲_
    trans         : Transitive A _≲_
 
  module Eq = IsIndexedEquivalence isEquivalence
 
  refl : Reflexive A _≲_
  refl = reflexive Eq.refl