    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Homogeneously-indexed binary relations
    ------------------------------------------------------------------------

    -- The contents of this module should be accessed via
    -- `Relation.Binary.Indexed.Homogeneous`.

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

    module Relation.Binary.Indexed.Homogeneous.Definitions where

    open import Data.Product.Base using (_×_)
    open import Level using (Level)
    open import Relation.Binary.Core using (_⇒_)
    import Relation.Binary.Definitions as B
      using (Reflexive; Symmetric; Transitive; Antisymmetric; Decidable)
    open import Relation.Binary.Indexed.Homogeneous.Core using (IRel)
    open import Relation.Unary.Indexed using (IPred)

    private
      variable
        i a ℓ ℓ₁ ℓ₂ : Level
        I : Set i

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

    module _ (A : I → Set a) where

      syntax Implies A _∼₁_ _∼₂_ = _∼₁_ ⇒[ A ] _∼₂_

      Implies : IRel A ℓ₁ → IRel A ℓ₂ → Set _
      Implies _∼₁_ _∼₂_ = ∀ {i} → _∼₁_ ⇒ (_∼₂_ {i})

      Reflexive : IRel A ℓ → Set _
      Reflexive _∼_ = ∀ {i} → B.Reflexive (_∼_ {i})

      Symmetric : IRel A ℓ → Set _
      Symmetric _∼_ = ∀ {i} → B.Symmetric (_∼_ {i})

      Transitive : IRel A ℓ → Set _
      Transitive _∼_ = ∀ {i} → B.Transitive (_∼_ {i})

      Antisymmetric : IRel A ℓ₁ → IRel A ℓ₂ → Set _
      Antisymmetric _≈_ _∼_ = ∀ {i} → B.Antisymmetric _≈_ (_∼_ {i})

      Decidable : IRel A ℓ → Set _
      Decidable _∼_ = ∀ {i} → B.Decidable (_∼_ {i})

      Respects : IPred A ℓ₁ → IRel A ℓ₂ → Set _
      Respects P _∼_ = ∀ {i} {x y : A i} → x ∼ y → P x → P y

      Respectsˡ : IRel A ℓ₁ → IRel A ℓ₂ → Set _
      Respectsˡ P _∼_  = ∀ {i} {x y z : A i} → x ∼ y → P x z → P y z

      Respectsʳ : IRel A ℓ₁ → IRel A ℓ₂ → Set _
      Respectsʳ P _∼_ = ∀ {i} {x y z : A i} → x ∼ y → P z x → P z y

      Respects₂ : IRel A ℓ₁ → IRel A ℓ₂ → Set _
      Respects₂ P _∼_ = (Respectsʳ P _∼_) × (Respectsˡ P _∼_)