------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed binary relations
------------------------------------------------------------------------
 
-- The contents of this module should be accessed via
-- `Relation.Binary.Indexed.Heterogeneous`.
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Relation.Binary.Indexed.Heterogeneous.Definitions where
 
open import Level using (Level)
import Relation.Binary.Definitions as B
  using (Reflexive; Symmetric; Transitive; Sym; Trans)
open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
 
private
  variable
    i a ℓ : Level
    I : Set i
 
------------------------------------------------------------------------
-- Simple properties of indexed binary relations
 
Reflexive : (A : I → Set a) → IRel A ℓ → Set _
Reflexive _ _∼_ = ∀ {i} → B.Reflexive (_∼_ {i})
 
Symmetric : (A : I → Set a) → IRel A ℓ → Set _
Symmetric _ _∼_ = ∀ {i j} → B.Sym (_∼_ {i} {j}) _∼_
 
Transitive : (A : I → Set a) → IRel A ℓ → Set _
Transitive _ _∼_ = ∀ {i j k} → B.Trans _∼_ (_∼_ {j}) (_∼_ {i} {k})